Questionnaire-2024/smt/3013_sol.tex

We start by translating $\varphi$ to $\hat{\varphi} = \skel$ and assign the following variables to the theory literals:
\begin{itemize}
	\item $e_{0}\Leftrightarrow(f(a)=b)$
	\item $e_{1}\Leftrightarrow(f(a)=c)$
	\item $e_{2}\Leftrightarrow(b=c)$
	\item $e_{3}\Leftrightarrow(a=b)$
\end{itemize}

$\hat{\varphi} = (\clause{e_{0}; e_{1}; \lnot e_{2}}) \land (\clause{e_{2}; e_{3}; e_{0}}) \land (\clause{\lnot e_{0}; e_{3}}) \land (\clause{e_{2}; \lnot e_{3}; \lnot e_{0}}) \land (\clause{\lnot e_{1}; e_{2}}) \land (\clause{\lnot e_{1}; e_{2}; \lnot e_{3}}) \land (\clause{e_{0}; e_{1}}) $


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

$\Model_{\EUF} := \{(f(a) \neq b), (f(a) = c), (b = c)\} $ \\
Check if the assignment is consistent with the theory:

\begin{align*}
	&\{f(a), c\}, \{b, c\}\\
	&\{b, c, f(a)\}
\end{align*}

$\Model_{\EUF}$ is not consistent with the theory, because of: $(f(a) \neq b) $\\
$\Rightarrow$ We need to add a blocking clause from $\Model_{\EUF}$:

$BC_8 := e_0 \lor \neg e_1 \lor \neg e_2 $ \\

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