Questionnaire-2024/sat_solvers_dpll/4002_sol.tex

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