Questionnaire-2024/sat_solvers_dpll/4005_sol_second_part.tex

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