Questionnaire-2024/sat_solvers_dpll/4003_sol.tex

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