Skip to content

Commit

Permalink
move equations from theory to cnf
Browse files Browse the repository at this point in the history
  • Loading branch information
@Anatoly03
Anatoly03 committed Jan 9, 2024
1 parent 691b4f0 commit 1a58b6b
Show file tree
Hide file tree
Showing 4 changed files with 23 additions and 129 deletions.
Binary file modified papers/cnf/Cnf.pdf
View file
Binary file not shown.
32 changes: 23 additions & 9 deletions papers/cnf/Cnf.tex
View file
Original file line number Diff line number Diff line change
Expand Up @@ -51,9 +51,9 @@
If a disjunction consists of one literal, the value of
this literal is fixed.

\[\{X\} \in S \Rightarrow X = \top \]
\[\{X\} \in CNF \Rightarrow X = \top \]

\item[Absorption.]
\item[Absorption (CNF).]

If a disjunction is a superset of another disjunction, it
can be ignored.
Expand All @@ -62,17 +62,21 @@

Proof: $(X \Rightarrow Y) \lor \lnot X$ makes $Y$ irrelevant.

\begin{center}
\begin{tabular}{l|c|p{7pt}|}
\multicolumn{1}{c}{} & \multicolumn{1}{c} X \\ \cline{2-2} \noalign{\vskip\doublerulesep\vskip-\arrayrulewidth} \hhline{~|*{2}{-}}
\multicolumn{1}{c||} Y & \fc & \\ \hhline{~|*{2}{-}}
& \fc & \fc \\ \hhline{~|*{2}{-}}
\end{tabular}
\end{center}
\begin{center}\begin{tabular}{l|c|p{7pt}|}
\multicolumn{1}{c}{} & \multicolumn{1}{c} X \\ \cline{2-2} \noalign{\vskip\doublerulesep\vskip-\arrayrulewidth} \hhline{~|*{2}{-}}
\multicolumn{1}{c||} Y & \fc & \\ \hhline{~|*{2}{-}}
& \fc & \fc \\ \hhline{~|*{2}{-}}
\end{tabular}\end{center}

The Absorption Rule allows to freely create new disjunctions,
as long it's consisting of an already existing disjunction.

\item[Absorption (DNF).]

\[\forall X \subseteq Y : X + Y \equiv_\text{DNF} X \]

Proof: $(X \Rightarrow \top) \land (\lnot X \Rightarrow \lnot Y)$

\item[Common Contradiction.]

\[(A + X)\cdot(B + \overline X)\equiv_\text{CNF}(BX+A\overline X)\]
Expand All @@ -99,6 +103,16 @@
\end{tabular}
\end{center}

\item[Semi-Common Part.]

\[(AX + B)(A + C) \equiv_\text{CNF} A(X + B) + BC\]

Proof: \begin{equation}\nonumber\begin{split}
(AX + B)(A + C) \\
\equiv_\text{CNF} AX + AXC + AB + BC \\
\equiv_\text{CNF}^\text{Absorption} AX + AB + BC
\end{split}\end{equation}

\item[Common and Contradicting Part]

\[ (A + B + C) \cdot (A + \lnot B + D) \equiv_\text{CNF} (A + BD + C \overline B)\]
Expand Down
Binary file modified papers/theory/Theory.pdf
View file
Binary file not shown.
120 changes: 0 additions & 120 deletions papers/theory/Theory.tex
View file
Original file line number Diff line number Diff line change
Expand Up @@ -116,66 +116,6 @@
\section{Optimisation Techniques}

\begin{description}
\item[Zugzwang.] {
\emph{Common Literals.}
If a disjunction consists of one literal, the value of
this literal is fixed.

\[S = X \cdot A(X) \rightarrow \left(f_{SAT}(Y) \Rightarrow X \in Y \right) \]
}
\item[Contradiction.]
{
\emph{Contradictional Disjunctions.}

A formula with contradictional disjunctions
is not satisfiable.

\[\forall A : X \cdot \lnot X \cdot A(X) = \bot \]
}
\item[Common Contradicting Literals.] {
\emph{Disjunction with common contradictional part.}

\[ (A + B) \cdot (\lnot A + C) \cdot X = (AC + B \overline A) \cdot X\]

\begin{center}
\begin{tabular}{lcccc}
& \multicolumn{2}{c} A \\ \cline{2-3} \noalign{\vskip\doublerulesep\vskip-\arrayrulewidth} \hhline{~|*{4}{-}}
\multicolumn{1}{c||} C & \multicolumn{1}{c|} {\cellcolor{blue!15}} & \multicolumn{1}{c|} {\cellcolor{blue!15}} & \multicolumn{1}{c|} {\cellcolor{blue!15}} & \multicolumn{1}{c|} {} \\ \hhline{~|*{4}{-}}
\multicolumn{1}{c|} {} & \multicolumn{1}{c|} {} & \multicolumn{1}{c|} {} & \multicolumn{1}{c|} {\cellcolor{blue!15}} & \multicolumn{1}{c|} {} \\ \cline{2-5} \noalign{\vskip\doublerulesep\vskip-\arrayrulewidth} \cline{3-4}
&& \multicolumn{2}{c} B \\
\end{tabular}
\end{center}
}
\item[Common Literals.] {
\emph{Disjunction with common positive part.}

\[ (A + B) \cdot (A + C) \cdot X = (A + B C) \cdot X\]

\begin{center}
\begin{tabular}{lcccc}
& \multicolumn{2}{c} A \\ \cline{2-3} \noalign{\vskip\doublerulesep\vskip-\arrayrulewidth} \hhline{~|*{4}{-}}
\multicolumn{1}{c||} C & \multicolumn{1}{c|} {\cellcolor{blue!15}} & \multicolumn{1}{c|} {\cellcolor{blue!15}} & \multicolumn{1}{c|} {\cellcolor{blue!15}} & \multicolumn{1}{c|} {} \\ \hhline{~|*{4}{-}}
\multicolumn{1}{c|} {} & \multicolumn{1}{c|} {\cellcolor{blue!15}} & \multicolumn{1}{c|} {\cellcolor{blue!15}} & \multicolumn{1}{c|} {} & \multicolumn{1}{c|} {} \\ \cline{2-5} \noalign{\vskip\doublerulesep\vskip-\arrayrulewidth} \cline{3-4}
&& \multicolumn{2}{c} B \\
\end{tabular}
\end{center}
}
\item[Common Literals and Contradictional Part.] {
\emph{Disjunction with positive and negative common parts.}

\[ (A + B + C) \cdot (A + \lnot B + D) \cdot X = (A + BD + C \overline B) \cdot X\]

\begin{center}
\begin{tabular}{lccccr}
& \multicolumn{2}{c} A \\ \cline{2-3} \noalign{\vskip\doublerulesep\vskip-\arrayrulewidth} \hhline{~|*{4}{-}}
\multicolumn{1}{l||} {\multirow{2}{*}{C}} & \multicolumn{1}{c|} {\cellcolor{blue!15}} & \multicolumn{1}{c|} {\cellcolor{blue!15}} & \multicolumn{1}{c|} {} & \multicolumn{1}{c|} {\cellcolor{blue!15}} \\ \hhline{~|*{4}{-}}
\multicolumn{1}{l||}{} & \multicolumn{1}{c|} {\cellcolor{blue!15}} & \multicolumn{1}{c|} {\cellcolor{blue!15}} & \multicolumn{1}{c|} {\cellcolor{blue!15}} & \multicolumn{1}{c} {\cellcolor{blue!15}} & \multicolumn{1}{||r} {\multirow{2}{*}{D}} \\ \hhline{~|*{4}{-}}
\multicolumn{1}{l|}{} & \multicolumn{1}{c|} {\cellcolor{blue!15}} & \multicolumn{1}{c|} {\cellcolor{blue!15}} & \multicolumn{1}{c|} {\cellcolor{blue!15}} & \multicolumn{1}{c} {} & \multicolumn{1}{||r}{} \\ \hhline{~|*{4}{-}}
\multicolumn{1}{l|}{} & \multicolumn{1}{c|} {\cellcolor{blue!15}} & \multicolumn{1}{c|} {\cellcolor{blue!15}} & \multicolumn{1}{c|} {} & \multicolumn{1}{c|} {} \\ \cline{2-5} \noalign{\vskip\doublerulesep\vskip-\arrayrulewidth} \cline{3-4}
&& \multicolumn{2}{c} B \\
\end{tabular}
\end{center}
}
\item[Connected Component.] {
\emph{Two independent sets of variables.}
If there exists two sets of variables $A$ and $B$, such that
Expand All @@ -199,65 +139,5 @@
}
\end{description}

\section{CNF-SAT Optimisation}

TODO 3-CNF-SAT equations

% https://tex.stackexchange.com/questions/25886/how-to-fix-the-width-of-a-minipage
\begin{multicols}{2}% Two-column layout
\setlength{\parindent}{0pt}% No paragraph indent
\begin{minipage}[t]{\linewidth}%
\begin{minipage}[t]{\linewidth-2\fboxsep-2\fboxrule}
\begin{description}
\item[All equal.] {
$D\cdot D = D$

If two disjunctions are equal, remove
the second one.
}
\item[One off.] {
$(a+b+c)\cdot(a+b+d)$

If two disjunctions differ in only one
letter, the following can be said:
\begin{equation}
\nonumber
\begin{aligned}
(a+b+c)\cdot(a+b+d)\\
= a+b+c\cdot d
\end{aligned}
\end{equation}
}
\end{description}
\end{minipage}

\end{minipage}

\begin{minipage}[t]{\linewidth}%
\begin{minipage}[t]{\linewidth-2\fboxsep-2\fboxrule}% Remove fbox rule/sep width
\begin{description}
% \item[All different.] {
% $(a+b+c)\cdot(d+e+f)$
%
% Do nothing.
% }
\item[Opposing Literal.] {
$(a+D_1)\cdot(\overline a+D_2)$

\begin{center}
\begin{tabular}{lcccc}
& \multicolumn{2}{c} a \\ \cline{2-3} \noalign{\vskip\doublerulesep\vskip-\arrayrulewidth} \hhline{~|*{4}{-}}
\multicolumn{1}{c||}{$D_1$} & \multicolumn{1}{c|}{} & \multicolumn{1}{c|} {\cellcolor{blue!15}} & \multicolumn{1}{c|} {\cellcolor{blue!15}} & \multicolumn{1}{c|}{\cellcolor{blue!15}} \\ \hhline{~|*{4}{-}}
\multicolumn{1}{c|} {} & \multicolumn{1}{c|}{} & \multicolumn{1}{c|} {\cellcolor{blue!15}} & \multicolumn{1}{c|} {} & \multicolumn{1}{c|} {} \\ \cline{2-5} \noalign{\vskip\doublerulesep\vskip-\arrayrulewidth} \cline{3-4}
&& \multicolumn{2}{c}{$D_2$} \\
\end{tabular}
\end{center}

Add the following
}
\end{description}
\end{minipage}
\end{minipage}
\end{multicols}

\end{document}

0 comments on commit 1a58b6b

Please sign in to comment.