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.
 
 

133 lines
3.8 KiB

\begin{dplltabular}{9}
\dpllStep{1|2|3|4|5}
\dpllDecL{0|1|1|1|1}
\dpllAssi{-|
$\lnot a$|
$\lnot a, \lnot b$|
$\lnot a, \lnot b, \lnot c$|
$\lnot a,\lnot b, \lnot c, \lnot d$}
\dpllClause{1}{$\lnot a,c$}
{$\lnot a,c$|\done|\done|\done|\done}
\dpllClause{2}{$\lnot a, b, \lnot c$}
{$\lnot a, b, \lnot c$|\done|\done|\done|\done}
\dpllClause{3}{$\lnot b, e$}
{$\lnot b, e$|$\lnot b, e$|\done|\done|\done}
\dpllClause{4}{$a, d$}
{$a, d$|$d$|$d$|$d$|\conflict}
\dpllClause{5}{$a, \lnot c$}
{$a, \lnot c$|$\lnot c$|$\lnot c$|\done|\done}
\dpllClause{6}{$\lnot a, \lnot e$}
{$\lnot a, \lnot e$|\done|\done|\done|\done}
\dpllClause{7}{$a, \lnot b$}
{$a, \lnot b$|$\lnot b$|\done|\done|\done}
\dpllClause{8}{$b, \lnot d$}
{$b, \lnot d$|$b, \lnot d$|$\lnot d$|$\lnot d$|\done}
\dpllBCP{-|$\lnot b$|$\lnot c$|$\lnot d$|-}
\dpllPL{-|-|-|-|-}
\dpllDeci{$\lnot a$|-|-|-|-}
\end{dplltabular}
\begin{conflictgraph}
\node[base node] (notA) {$\lnot a$};
\node[base node] (notB) [right of=notA] {$\lnot b$};
\node[base node] (notD) [right of=notB] {$\lnot d$};
\node[base node] (D) [above of=notD] {$d$};
\node[base node] (bot) [below right of=D] {$\bot$};
\path[]
(notA) edge [] node {$7$} (notB)
(notA) edge [] node {$4$} (D)
(notB) edge [] node {$8$} (notD)
(notD) edge [] node {} (bot)
(D) edge [] node {} (bot);
\end{conflictgraph}
\begin{prooftree}
\AxiomC{$8. \; b \lor \lnot d$}
\AxiomC{$4. \; a \lor d$}
\BinaryInfC{$a \lor b$}
\AxiomC{$7. \; a \lor \lnot b $}
\BinaryInfC{$a$}
\end{prooftree}
\begin{dplltabular}{9}
\dpllStep{(1)|6|7|8|9}
\dpllDecL{0 |0|0|0|0}
\dpllAssi{-|
$a$|
$a,c$|
$a,c,b$|
$a,c,b,\lnot e$}
\dpllClause{1}{$\lnot a,c$}
{$\lnot a,c$|$c$|\done|\done|\done}
\dpllClause{2}{$\lnot a, b, \lnot c$}
{$\lnot a, b, \lnot c$|$b,\lnot c$|$b$|\done|\done}
\dpllClause{3}{$\lnot b, e$}
{$\lnot b, e$|$\lnot b, e$|$\lnot b,e$|$e$|\conflict}
\dpllClause{4}{$a, d$}
{$a, d$|\done|\done|\done|\done}
\dpllClause{5}{$a, \lnot c$}
{$a, \lnot c$|\done|\done|\done|\done}
\dpllClause{6}{$\lnot a, \lnot e$}
{$\lnot a, \lnot e$|$\lnot e$|$\lnot e$|$\lnot e$|\done}
\dpllClause{7}{$a, \lnot b$}
{$a, \lnot b$|\done|\done|\done|\done}
\dpllClause{8}{$b, \lnot d$}
{$b, \lnot d$|$b,\lnot d$|$b,\lnot d$|\done|\done}
\dpllClause{9}{$a$}
{$a$|\done|\done|\done|\done}
\dpllBCP{$a$|$c$|$b$|$\lnot e$|-}
\dpllPL{-|-|-|-|-}
\dpllDeci{-|-|-|-|UNSAT}
\end{dplltabular}
\begin{conflictgraph}
\node (0) {};
\node[base node] (A) [right of=0] {$a$};
\node[base node] (C) [right of=A] {$c$};
\node[base node] (B) [right of=C] {$b$};
\node[base node] (E) [right of=B] {$e$};
\node[base node] (notE) [below right of=A] {$\lnot e$};
\node[base node] (bot) [below of=E] {$\bot$};
\path[]
(0) edge [] node {$9$} (A)
(A) edge [] node {$1$} (C)
(A) edge [bend left] node {$2$} (B)
(C) edge [] node {$2$} (B)
(B) edge [] node {$3$} (E)
(A) edge [] node {$6$} (notE)
(E) edge [] node {} (bot)
(notE) edge [] node {} (bot);
\end{conflictgraph}
\begin{prooftree}
\AxiomC{$3. \; \clause{\lnot b;e}$}
\AxiomC{$6. \; \clause{\lnot a;\lnot e}$}
\BinaryInfC{$\clause{\lnot a;\lnot b}$}
\AxiomC{$2. \; \clause{\lnot a;b;\lnot c}$}
\BinaryInfC{$\clause{\lnot a;\lnot c}$}
\AxiomC{$1. \; \clause{\lnot a;c}$}
\BinaryInfC{$\clause{\lnot a}$}
\AxiomC{$9. \; \clause{a}$}
\BinaryInfC{$\bot$}
\end{prooftree}