Questionnaire-2024/sat_solvers_dpll/0011_sol.tex

\hspace{-0.09cm}\scalebox{0.87}{
  \begin{dplltabular}{7}
    \dpllStep{1|2|3|4|5|6|7}

    \dpllDecL{0|1|2|2|2|2|1}

    \dpllAssi{-|
              $\lnot a$|
              $\lnot a, \lnot b$|
              $\lnot a, \lnot b, c$|
              $\lnot a, \lnot b, c, \lnot e$|
              $\lnot a, \lnot b, c, \lnot e, \lnot d$|
              $\lnot a$}

    \dpllClause{1}{$\lnot a,\lnot c$}
               {$\lnot a,\lnot c$|\done|\done|\done|\done|\done|\done}
    \dpllClause{2}{$b,c$}
               {$b,c$|$b,c$|$c$|\done|\done|\done|$b,c$}
    \dpllClause{3}{$\lnot b, \lnot d$}
               {$\lnot b,\lnot d$|$\lnot b,\lnot d$|\done|\done|\done|\done|$\lnot b,\lnot d$}
    \dpllClause{4}{$\lnot d, e$}
               {$\lnot d,e$|$\lnot d,e$|$\lnot d,e$|$\lnot d,e$|$\lnot d$|\done|$\lnot d,e$}
    \dpllClause{5}{$d, e$}
               {$d.e$|$d.e$|$d.e$|$d.e$|$d$|\conflict|$d,e$}
    \dpllClause{6}{$a, \lnot c, \lnot e$}
               {$a, \lnot c, \lnot e$|$\lnot c,\lnot e$|$\lnot c, \lnot e$|$\lnot e$|\done|\done|$\lnot c, \lnot e$}
    \dpllClause{7}{$\lnot b, c, d$}
               {$\lnot b,c,d$|$\lnot b,c,d$|\done|\done|\done|\done|$\lnot b,c,d$}
    \dpllClause{8}{\textcolor{gray}{$a.b$}}
               {-|-|-|-|-|$a,b$|$b$}
    \dpllClause{9}{\textcolor{gray}{$a$}}
               {-|-|-|-|-|-|-}

    \dpllBCP{-|-|$c$|$\lnot e$|\lnot d|-|$b$}
    \dpllPL{-|-|-|-|-|-|-}
    \dpllDeci{$\lnot a$|$\lnot b$|-|-|-|-|-}
  \end{dplltabular}
}

First Conflict in Step 6: \\
\begin{conflictgraph}
  \node[base node] (notA)                       {$\lnot a$};
  \node[base node] (notB) [below of=notA]       {$\lnot b$};
  \node[base node] (C)    [right of=notB]       {$c$};
  \node[base node] (notE) [above right of=C]    {$\lnot e$};
  \node[base node] (D)    [above right of=notE] {$d$};
  \node[base node] (notD) [below right of=notE] {$\lnot d$};
  \node[base node] (bot)  [below right of=D] {$\bot$};
  \path[]
      (notA) edge [] node {$6$} (notE)
      (notB) edge [] node {$2$} (C)
      (C)    edge [] node {$6$} (notE)
      (notE) edge [] node {$4$} (D)
      (notE) edge [] node {$5$} (notD)
      (notD) edge [] node {}    (bot)
      (D)    edge [] node {}    (bot);
\end{conflictgraph}
\begin{prooftree}
\AxiomC{$4. \; \lnot d \lor e$}
\AxiomC{$5. \; d \lor e$}
	\BinaryInfC{$e$}
	\AxiomC{$6. \; a \lor \lnot c \lor \lnot e$}
		\BinaryInfC{$a \lor \lnot c$}
		\AxiomC{$2. \; b \lor c$}
			\BinaryInfC{$ a \lor b$}
\end{prooftree}
\vspace{1cm}

\scalebox{0.87}{
  \begin{dplltabular}{8}
    \dpllStep{8|9|10|11|12|13|14}
    \dpllDecL{1|1|1|1|0|0|0}
    \dpllAssi{ $\lnot a, b$|
              $\lnot a, b, \lnot d$|
              $\lnot a, b, \lnot d, c$|
              $\lnot a, b, \lnot d, c, \lnot e$|
              -|
              $a$|
              $a, \lnot c$}

    \dpllClause{1}{$\lnot a,\lnot c$}
               {\done|\done|\done|\done|$\lnot a,\lnot c$|$\lnot c$|\done}
    \dpllClause{2}{$b,c$}
               {\done|\done|\done|\done|$b,c$|$b,c$|$b$}
    \dpllClause{3}{$\lnot b, \lnot d$}
               {$\lnot d$|\done|\done|\done|$\lnot b,\lnot d$|$\lnot b,\lnot d$|$\lnot b,\lnot d$}
    \dpllClause{4}{$\lnot d, e$}
               {$\lnot d,e$|\done|\done|\done|$\lnot d,e$|$\lnot d,e$|$\lnot d,e$}
    \dpllClause{5}{$d, e$}
               {$d,e$|$e$|$e$|\conflict|$d,e$|$d,e$|$d,e$}
    \dpllClause{6}{$a, \lnot c, \lnot e$}
               {$\lnot c,\lnot e$|$\lnot c,\lnot e$|$\lnot e$|\done|$a, \lnot c, \lnot e$|\done|\done}
    \dpllClause{7}{$\lnot b, c, d$}
               {$d,c$|$c$|\done|\done|$\lnot b, c, d$|$\lnot b, c, d$|$\lnot b, d$}
    \dpllClause{8}{\textcolor{gray}{$a.b$}}
               {\done|\done|\done|\done|$a,b$|\done|\done}
    \dpllClause{9}{\textcolor{gray}{$a$}}
               {-|-|-|$a$|$a$|\done|\done}

    \dpllBCP{$\lnot d$|$c$|$\lnot e$|-|$a$|$\lnot c$|$b$}
    \dpllPL{-|-|-|-|-|-|-}
    \dpllDeci{-|-|-|-|-|-|-}
  \end{dplltabular}
}


Second Conflict in Step 11: \\
\begin{conflictgraph}
  \node[base node] (notA)                       {$\lnot a$};
  \node[base node] (B)    [right of=notA]       {$b$};
  \node[base node] (notD) [right of=B]          {$\lnot d$};
  \node[base node] (E)    [right of=notD]       {$e$};
  \node[base node] (C)    [below of=E]          {$c$};
  \node[base node] (notE) [right of=C]          {$\lnot e$};
  \node[base node] (bot)  [above right of=notE] {$\bot$};
  \path[]
      (notA) edge [] node {$8$} (B)
      (B)    edge [] node {$3$} (notD)
      (notD) edge [] node {$5$} (E)
      (notD) edge [] node {$7$} (C)
      (C)    edge [] node {$6$} (notE)
      (notE) edge [] node {}    (bot)
      (E)    edge [] node {}    (bot);
\end{conflictgraph}


\begin{prooftree}
\AxiomC{$6. \; a \lor \lnot c \lor \lnot e$}
\AxiomC{$7. \; \lnot b \lor c \lor d$}
	\BinaryInfC{$a \lor \lnot b \lor d \lor \lnot e$}
	\AxiomC{$5. \; d \lor e$}
	  \BinaryInfC{$a \lor \lnot b \lor d$}
		\AxiomC{$3. \; \lnot b \lor \lnot d$}
			\BinaryInfC{$ a \lor \lnot b$}
		  \AxiomC{$8. \; a \lor b$}
			  \BinaryInfC{$a$}
\end{prooftree}
\vspace{1cm}

\scalebox{0.87}{
  \begin{dplltabular}{2}
    \dpllStep{15|16}
    \dpllDecL{0|0}
    \dpllAssi{$a, \lnot c, b$|
              $a, \lnot c, b, \lnot d$}

    \dpllClause{1}{$\lnot a,\lnot c$}
               {\done|\done}
    \dpllClause{2}{$b,c$}
               {\done|\done}
    \dpllClause{3}{$\lnot b, \lnot d$}
               {$\lnot d$|\done}
    \dpllClause{4}{$\lnot d, e$}
               {$\lnot d,e$|\done}
    \dpllClause{5}{$d, e$}
               {$d,e$|$e$}
    \dpllClause{6}{$a, \lnot c, \lnot e$}
               {\done|\done}
    \dpllClause{7}{$\lnot b, c, d$}
               {$d$|\conflict}
    \dpllClause{8}{\textcolor{gray}{$a.b$}}
               {\done|\done}
    \dpllClause{9}{\textcolor{gray}{$a$}}
               {\done|\done}

    \dpllBCP{$\lnot d$|-}
    \dpllPL{-|-}
    \dpllDeci{-|UNSAT}
  \end{dplltabular}
}


Second Conflict in Step 16: \\
\begin{conflictgraph}
  \node (0) {};
  \node[base node] (A)    [right of=0]       {$a$};
  \node[base node] (notC) [right of=A]       {$\lnot c$};
  \node[base node] (B)    [right of=notC]    {$b$};
  \node[base node] (notD) [right of=B]       {$\lnot d$};
  \node[base node] (D)    [below of=notD]    {$d$};
  \node[base node] (bot)  [above right of=D] {$\bot$};
  \path[]
      (0)    edge [] node {$9$}    (A)
      (A)    edge [] node {$1$}    (notC)
      (notC) edge [] node {$2$}    (B)
      (B)    edge [] node {$3$}    (D)
      (B)    edge [] node {$7$}    (notD)
      (notD) edge [] node {}       (bot)
      (D)    edge [] node {}       (bot);
\end{conflictgraph}

\begin{prooftree}
\AxiomC{$7. \; \lnot b \lor c \lor d$}
\AxiomC{$3. \; \lnot b \lor \lnot d$}
	\BinaryInfC{$\lnot b \lor c$}
	\AxiomC{$2. \; b \lor c$}
	  \BinaryInfC{$c$}
		\AxiomC{$1. \; \lnot a \lor \lnot c$}
			\BinaryInfC{$\lnot a$}
		  \AxiomC{$9. \; a$}
			  \BinaryInfC{$\bot$}
\end{prooftree}