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.
87 lines
2.5 KiB
87 lines
2.5 KiB
\begin{prooftree}
|
|
\AxiomC{$1. \; \clause{a;\lnot c;\lnot e$}}
|
|
\AxiomC{$4. \; \clause{\lnot b;d;\lor e$}}
|
|
\BinaryInfC{$\clause{a;\lnot b;\lnot c;d}$}
|
|
\AxiomC{$7. \; \clause{c;d}$}
|
|
\BinaryInfC{$\clause{a;\lnot b;d}$}
|
|
\AxiomC{$5. \; \clause{\lnot b;\lnot d}$}
|
|
\BinaryInfC{$\clause{a;\lnot b}$}
|
|
\AxiomC{$8. \; \clause{a;b}$}
|
|
\BinaryInfC{$\clause{a}$}
|
|
\end{prooftree}
|
|
|
|
\begin{dplltabular}{6}
|
|
\dpllStep{(1)|11|12|13|14}
|
|
\dpllDecL{0 |0 |0 |0 |0 }
|
|
|
|
\dpllAssi{-|
|
|
$a$|
|
|
$a, \lnot e$|
|
|
$a, \lnot e, b$|
|
|
\makecell{$a, \lnot e$,\\ $ b, \lnot d$}}
|
|
|
|
|
|
\dpllClause{1}{$a, \lnot c, \lnot e$}
|
|
{$a, \lnot c, \lnot e$|\done|\done|\done|\done}
|
|
|
|
\dpllClause{2}{$\lnot a, \lnot e$}
|
|
{$\lnot a, \lnot e$|$\lnot e$|\done|\done|\done}
|
|
|
|
\dpllClause{3}{$b,e$}
|
|
{$b,e$|$b,e$|$b$|\done|\done}
|
|
|
|
\dpllClause{4}{$\lnot b,d,e$}
|
|
{$\lnot b,d,e$|$\lnot b,d,e$|$\lnot b,d$|$d$|\conflict}
|
|
|
|
\dpllClause{5}{$\lnot b,\lnot d$}
|
|
{$\lnot b,\lnot d$|$\lnot b,\lnot d$|$\lnot b,\lnot d$|$\lnot d$|\done}
|
|
|
|
\dpllClause{6}{$c,\lnot d$}
|
|
{$c,\lnot d$|$c,\lnot d$|$c,\lnot d$|$c,\lnot d$|\done}
|
|
|
|
\dpllClause{7}{$c,d$}
|
|
{$c,d$|$c,d$|$c,d$|$c,d$|$c$}
|
|
|
|
\dpllClause{8}{$a,b$}
|
|
{$a,b$|\done|\done|\done|\done}
|
|
|
|
\dpllClause{9}{$a$}
|
|
{$a$|\done|\done|\done|\done}
|
|
|
|
\dpllBCP {$a$|$\lnot e$|$b$|$\lnot d$|-}
|
|
\dpllPL {-|-|-|-|-}
|
|
\dpllDeci{-|-|-|-|UNSAT}
|
|
\end{dplltabular}
|
|
|
|
|
|
\begin{conflictgraph}
|
|
\node (0){};
|
|
\node[base node] (A) [right of=0] {$a$};
|
|
\node[base node] (notE) [right of=A] {$\lnot e$};
|
|
\node[base node] (B) [right of=notE] {$b$};
|
|
\node[base node] (D) [above right of=B] {$d$};
|
|
\node[base node] (notD) [below right of=B] {$\lnot d$};
|
|
\node[base node] (bot) [above right of=notD] {$\bot$};
|
|
\path[]
|
|
(0) edge [] node {9} (A)
|
|
(A) edge [] node {2} (notE)
|
|
(notE) edge [] node {3} (B)
|
|
(B) edge [] node {4} (D)
|
|
(notE) edge [bend left] node {4} (D)
|
|
(B) edge [] node {5} (notD)
|
|
(notD) edge [] node {} (bot)
|
|
(D) edge [] node {} (bot);
|
|
\end{conflictgraph}
|
|
|
|
|
|
\begin{prooftree}
|
|
\AxiomC{$5. \; \clause{\lnot b;\lnot d$}}
|
|
\AxiomC{$4. \; \clause{\lnot b;d;\lor e$}}
|
|
\BinaryInfC{$\clause{\lnot b;e}$}
|
|
\AxiomC{$3. \; \clause{b;e}$}
|
|
\BinaryInfC{$\clause{e}$}
|
|
\AxiomC{$2. \; \clause{\lnot a;\lnot e}$}
|
|
\BinaryInfC{$\clause{\lnot a}$}
|
|
\AxiomC{$8. \; \clause{a}$}
|
|
\BinaryInfC{$\clause{\bot}$}
|
|
\end{prooftree}
|