Questionnaire-2024/smt/3016_sol_second_part.tex

\hspace{-0.09cm}\scalebox{0.85}{
	\begin{dplltabular}{5}
		\dpllStep{9|10|11|12|13}
		\dpllDecL{0|1|1|1|1}
		\dpllAssi{ - |$\lnot e_{0}$|$\lnot e_{0}, e_{1}$|$\lnot e_{0}, e_{1}, e_{2}$|\makecell{$\lnot e_{0}, e_{1}, e_{2}, $ \\ $\lnot e_{3}$}}
		\dpllClause{1}{$e_{0}, e_{1}, e_{2}$}{$e_{0}, e_{1}, e_{2}$|$e_{1}, e_{2}$|\done|\done|\done}
		\dpllClause{2}{$\lnot e_{0}, e_{1}$}{$\lnot e_{0}, e_{1}$|\done|\done|\done|\done}
		\dpllClause{3}{$\lnot e_{1}, e_{2}$}{$\lnot e_{1}, e_{2}$|$\lnot e_{1}, e_{2}$|$e_{2}$|\done|\done}
		\dpllClause{4}{$e_{2}, e_{3}$}{$e_{2}, e_{3}$|$e_{2}, e_{3}$|$e_{2}, e_{3}$|\done|\done}
		\dpllClause{5}{$\lnot e_{2}, e_{1}$}{$\lnot e_{2}, e_{1}$|$\lnot e_{2}, e_{1}$|\done|\done|\done}
		\dpllClause{6}{$\lnot e_{3}, \lnot e_{1}$}{$\lnot e_{3}, \lnot e_{1}$|$\lnot e_{3}, \lnot e_{1}$|$\lnot e_{3}$|$\lnot e_{3}$|\done}
		\dpllClause{7}{$e_{0}, e_{1}$}{$e_{0}, e_{1}$|$e_{1}$|\done|\done|\done}
		\dpllClause{8}{$e_{0}, \lnot e_{1}, \lnot e_{2}, e_{3}$}{\makecell{$e_{0}, \lnot e_{1}, \lnot e_{2}, $ \\ $e_{3}$}|$\lnot e_{1}, \lnot e_{2}, e_{3}$|$\lnot e_{2}, e_{3}$|$e_{3}$|\conflict}
		\dpllBCP{ - |$e_{1}$|$e_{2}$|$\lnot e_{3}$| - }
		\dpllPL{ - | - | - | - | - }
		\dpllDeci{$\lnot e_{0}$| - | - | - | - }
	\end{dplltabular}
}

Conflict in step 13\\
\scalebox{0.75}{

\begin{tikzpicture}[>=latex,line join=bevel,]
  \pgfsetlinewidth{1bp}
%%
\pgfsetcolor{black}
  % Edge: 1 -> 5
  \draw [->] (22.3bp,50.0bp) .. controls (35.47bp,50.0bp) and (58.583bp,50.0bp)  .. (85.878bp,50.0bp);
  \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
  \pgfsetstrokecolor{strokecol}
  \draw (54.0bp,57.5bp) node {$$7$$};
  % Edge: 3 -> 6
  \draw [->] (197.32bp,50.0bp) .. controls (211.2bp,50.0bp) and (236.16bp,50.0bp)  .. (263.96bp,50.0bp);
  \draw (232.0bp,57.5bp) node {$$8$$};
  % Edge: 4 -> 2
  \draw [->] (242.95bp,12.194bp) .. controls (259.12bp,14.134bp) and (291.4bp,18.008bp)  .. (322.79bp,21.775bp);
  % Edge: 5 -> 3
  \draw [->] (108.32bp,50.0bp) .. controls (122.2bp,50.0bp) and (147.16bp,50.0bp)  .. (174.96bp,50.0bp);
  \draw (140.0bp,57.5bp) node {$$3$$};
  % Edge: 5 -> 4
  \draw [->] (105.82bp,43.402bp) .. controls (111.18bp,39.225bp) and (118.62bp,34.054bp)  .. (126.0bp,31.0bp) .. controls (154.04bp,19.403bp) and (189.09bp,14.461bp)  .. (220.77bp,11.572bp);
  \draw (140.0bp,38.5bp) node {$$6$$};
  % Edge: 5 -> 6
  \draw [->] (105.67bp,57.009bp) .. controls (110.96bp,61.36bp) and (118.39bp,66.571bp)  .. (126.0bp,69.0bp) .. controls (176.81bp,85.217bp) and (195.19bp,85.217bp)  .. (246.0bp,69.0bp) .. controls (250.16bp,67.671bp) and (254.27bp,65.511bp)  .. (266.33bp,57.009bp);
  \draw (186.0bp,89.5bp) node {$$8$$};
  % Edge: 6 -> 2
  \draw [->] (285.16bp,45.662bp) .. controls (293.01bp,41.945bp) and (304.56bp,36.472bp)  .. (323.68bp,27.417bp);
  % Node: 1
\begin{scope}
  \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
  \pgfsetstrokecolor{strokecol}
  \draw (11.0bp,50.0bp) ellipse (11.0bp and 11.0bp);
  \draw (11.0bp,50.0bp) node {$\lnot e_{0}$};
\end{scope}
  % Node: 5
\begin{scope}
  \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
  \pgfsetstrokecolor{strokecol}
  \draw (97.0bp,50.0bp) ellipse (11.0bp and 11.0bp);
  \draw (97.0bp,50.0bp) node {$e_{1}$};
\end{scope}
  % Node: 2
\begin{scope}
  \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
  \pgfsetstrokecolor{strokecol}
  \draw (334.0bp,23.0bp) ellipse (11.0bp and 11.0bp);
  \draw (334.0bp,23.0bp) node {$\bot$};
\end{scope}
  % Node: 3
\begin{scope}
  \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
  \pgfsetstrokecolor{strokecol}
  \draw (186.0bp,50.0bp) ellipse (11.0bp and 11.0bp);
  \draw (186.0bp,50.0bp) node {$e_{2}$};
\end{scope}
  % Node: 6
\begin{scope}
  \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
  \pgfsetstrokecolor{strokecol}
  \draw (275.0bp,50.0bp) ellipse (11.0bp and 11.0bp);
  \draw (275.0bp,50.0bp) node {$e_{3}$};
\end{scope}
  % Node: 4
\begin{scope}
  \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
  \pgfsetstrokecolor{strokecol}
  \draw (232.0bp,11.0bp) ellipse (11.0bp and 11.0bp);
  \draw (232.0bp,11.0bp) node {$\lnot e_{3}$};
\end{scope}
%
\end{tikzpicture}


}
\begin{prooftree}
	\AxiomC{$8. \; e_{0} \lor \lnot e_{1} \lor \lnot e_{2} \lor e_{3}$}
	\AxiomC{$3. \; \lnot e_{1} \lor e_{2}$}
	\BinaryInfC{$e_{0} \lor \lnot e_{1} \lor e_{3}$}
	\AxiomC{$6. \; \lnot e_{3} \lor \lnot e_{1}$}
	\BinaryInfC{$e_{0} \lor \lnot e_{1}$}
	\AxiomC{$7. \; e_{0} \lor e_{1}$}
	\BinaryInfC{$e_{0}$}
\end{prooftree}

\hspace{-0.09cm}\scalebox{0.85}{
	\begin{dplltabular}{5}
		\dpllStep{14|15|16|17|18}
		\dpllDecL{0|0|0|0|0}
		\dpllAssi{ - |$e_{0}$|$e_{0}, e_{1}$|$e_{0}, e_{1}, e_{2}$|\makecell{$e_{0}, e_{1}, e_{2}, $ \\ $\lnot e_{3}$}}
		\dpllClause{1}{$e_{0}, e_{1}, e_{2}$}{$e_{0}, e_{1}, e_{2}$|\done|\done|\done|\done}
		\dpllClause{2}{$\lnot e_{0}, e_{1}$}{$\lnot e_{0}, e_{1}$|$e_{1}$|\done|\done|\done}
		\dpllClause{3}{$\lnot e_{1}, e_{2}$}{$\lnot e_{1}, e_{2}$|$\lnot e_{1}, e_{2}$|$e_{2}$|\done|\done}
		\dpllClause{4}{$e_{2}, e_{3}$}{$e_{2}, e_{3}$|$e_{2}, e_{3}$|$e_{2}, e_{3}$|\done|\done}
		\dpllClause{5}{$\lnot e_{2}, e_{1}$}{$\lnot e_{2}, e_{1}$|$\lnot e_{2}, e_{1}$|\done|\done|\done}
		\dpllClause{6}{$\lnot e_{3}, \lnot e_{1}$}{$\lnot e_{3}, \lnot e_{1}$|$\lnot e_{3}, \lnot e_{1}$|$\lnot e_{3}$|$\lnot e_{3}$|\done}
		\dpllClause{7}{$e_{0}, e_{1}$}{$e_{0}, e_{1}$|\done|\done|\done|\done}
		\dpllClause{8}{$e_{0}, \lnot e_{1}, \lnot e_{2}, e_{3}$}{\makecell{$e_{0}, \lnot e_{1}, \lnot e_{2}, $ \\ $e_{3}$}|\done|\done|\done|\done}
		\dpllClause{9}{$e_{0}$}{$e_{0}$|\done|\done|\done|\done}
		\dpllBCP{$e_{0}$|$e_{1}$|$e_{2}$|$\lnot e_{3}$| - }
		\dpllPL{ - | - | - | - | - }
		\dpllDeci{ - | - | - | - |SAT}
	\end{dplltabular}
}

$\Model_{\EUF} := (f(x) = x) \land (f(x) = y) \land (x = y) \land (z \neq f(x)) $ \\
Check if the assignment is consistent with the theory:

\begin{align*}
	&\{f(x), x\}, \{f(x), y\}, \{x, y\}, \{z\}\\
	&\{z\}, \{f(x), x, y\}
\end{align*}

$\Model_{\EUF}$ is consistent with the theory, \\$\Rightarrow \Model_{\EUF}$ is a satisfying assignment and $\varphi$ is SAT.