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
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}
|