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.
 
 

92 lines
3.0 KiB

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