You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
89 lines
4.8 KiB
89 lines
4.8 KiB
DPLL algorithm:
|
|
|
|
\scalebox{1}{
|
|
\setlength\tabcolsep{3pt}
|
|
\begin{tabular}{|l|c|c|c|c|c|c|c|c|c|c|}
|
|
\hline
|
|
Step & 1 & 2 & 3 & 4 & 5 & 6 & 7 & 8 & 9 & 10 \\ \hline \hline
|
|
Decision Level & 0 & 1 & 1 & 1 & 1 & 0 & 0 & 0 & 0 & 0 \\ \hline
|
|
Assignment & - & $\lnot a$& $\lnot a,c$ & $\lnot a,b,c$ & $\lnot a,b,c,\lnot d$& - & $a$ &$a,\lnot b$ &$a,\lnot b,\lnot c$& $a,\lnot b,\lnot c,\lnot e$ \\ \hline
|
|
Cl. 1: $\lnot a,\lnot b$ & 1 & \cmark & \cmark & \cmark & \cmark & 1 & $\lnot b$ & \cmark & \cmark & \cmark \\ \hline
|
|
Cl. 2: $ a,c$ & 2 & $c$ & \cmark & \cmark & \cmark & 2 & \cmark & \cmark & \cmark & \cmark \\ \hline
|
|
Cl. 3: $b,\lnot c$ & 3 & 3 & $b$ & \cmark & \cmark & 3 & 3 & $\lnot c$ & \cmark & \cmark \\ \hline
|
|
Cl. 4: $\lnot b,d$ & 4 & 4 & 4 & $d$ & $\{\}$ \xmark & 4 & 4 & \cmark & \cmark & \cmark \\ \hline
|
|
Cl. 5: $\lnot c,\lnot d$ & 5 & 5 & $\lnot d$ & $\lnot d$ & \cmark & 5 & 5 & 5 & \cmark & \cmark \\ \hline
|
|
Cl. 6: $c,e$ & 6 & 6 & \cmark & \cmark & \cmark & 6 & 6 & 6 & $e$ & $\{\}$ \xmark \\ \hline
|
|
Cl. 7: $c,\lnot e$ & 7 & 7 & \cmark & \cmark & \cmark & 7 & 7 & 7 & $\lnot e$ & \cmark \\ \hline
|
|
\textcolor{gray}{Cl. 8: $a$}& - & - & - & - & learned $a$ & 8 & \cmark & \cmark & \cmark & \cmark \\ \hline \hline
|
|
BCP & - & $c$ & $b$ & $\lnot d$ & - & $a$ & $\lnot b$ & $\lnot c$ & $\lnot e$ & - \\ \hline
|
|
PL & - & - & - & - & - & - & - & - & - & - \\ \hline
|
|
Decision & $\lnot a$& - & - & - & - & - & - & - & - & UNSAT \\ \hline
|
|
\end{tabular}}
|
|
|
|
Ad 5:
|
|
|
|
\begin{center}
|
|
\begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,node distance=1.5cm,
|
|
thick,base node/.style={circle,draw,minimum size=20pt}, real node/.style={double,circle,draw,minimum size=20pt}]
|
|
|
|
\node[base node] (1) {$\lnot a$};
|
|
\node[base node] (2) [right of=1]{$c$};
|
|
\node[base node] (3) [below right of=2] {$\lnot d$};
|
|
\node[base node] (4) [above right of=2] {$b$};
|
|
\node[base node] (5) [right of=4] {$d$};
|
|
\node[base node] (6) [below right of=5] {$\bot$};
|
|
\path[]
|
|
(1) edge [] node {$2$} (2)
|
|
(2) edge [] node {$5$} (3)
|
|
edge [] node {$3$} (4)
|
|
(4) edge [] node {$4$} (5)
|
|
(5) edge [] node {} (6)
|
|
(3) edge [] node {} (6);
|
|
\end{tikzpicture}
|
|
\end{center}
|
|
|
|
\begin{prooftree}
|
|
\AxiomC{$4. \; \lnot b \lor d$}
|
|
\AxiomC{$5. \; \lnot c \lor \lnot d$}
|
|
\BinaryInfC{$\lnot b \lor \lnot c$}
|
|
\AxiomC{$3. \; b \lor \lnot c$}
|
|
\BinaryInfC{$\lnot c$}
|
|
\AxiomC{$2. \; a \lor c$}
|
|
\BinaryInfC{$a$}
|
|
\end{prooftree}
|
|
|
|
Ad 10:
|
|
|
|
\begin{center}
|
|
\begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,node distance=1.5cm,
|
|
thick,base node/.style={circle,draw,minimum size=20pt}, real node/.style={double,circle,draw,minimum size=20pt}]
|
|
|
|
\node (0) {};
|
|
\node[base node] (1) [right of=0]{$a$};
|
|
\node[base node] (2) [right of=1]{$\lnot b$};
|
|
\node[base node] (3) [right of=2] {$\lnot c$};
|
|
\node[base node] (4) [above right of=3] {$\lnot e$};
|
|
\node[base node] (5) [below right of=3] {$e$};
|
|
\node[base node] (6) [above right of=5] {$\bot$};
|
|
\path[]
|
|
(0) edge [] node {$8$} (1)
|
|
(1) edge [] node {$1$} (2)
|
|
(2) edge [] node {$3$} (3)
|
|
(3) edge [] node {$7$} (4)
|
|
edge [] node {$6$} (5)
|
|
(4) edge [] node {} (6)
|
|
(5) edge [] node {} (6);
|
|
\end{tikzpicture}
|
|
\end{center}
|
|
|
|
\begin{prooftree}
|
|
\AxiomC{$6. \; c \lor e$}
|
|
\AxiomC{$7. \; c \lor \lnot e$}
|
|
\BinaryInfC{$c$}
|
|
\AxiomC{$3. \; b \lor \lnot c$}
|
|
\BinaryInfC{$b$}
|
|
\AxiomC{$1. \; \lnot a \lor \lnot b$}
|
|
\BinaryInfC{$\lnot a$}
|
|
\AxiomC{$8. \; a$}
|
|
\BinaryInfC{$\bot$}
|
|
\end{prooftree}
|