23 changed files with 990 additions and 5 deletions
-
2smt/2001.tex
-
2smt/2004.tex
-
8smt/3013.tex
-
61smt/3013_sol.tex
-
98smt/3013_sol_second_part.tex
-
9smt/3014.tex
-
37smt/3014_sol.tex
-
9smt/3015.tex
-
36smt/3015_sol.tex
-
8smt/3016.tex
-
126smt/3016_sol.tex
-
133smt/3016_sol_second_part.tex
-
7smt/3017.tex
-
125smt/3017_sol.tex
-
133smt/3017_sol_second_part.tex
-
7smt/3018.tex
-
39smt/3018_sol.tex
-
26smt/3018_sol_second_part.tex
-
7smt/3019.tex
-
41smt/3019_sol.tex
-
26smt/3019_sol_second_part.tex
-
45smt/smt.tex
-
10util/math_macros.tex
@ -1,3 +1,3 @@ |
|||
\item \ifassignmentsheet \points{2} \fi \applyAckermann{ |
|||
$$f(x)=g(x) \lor z=f(y) \imp f(z) \neq g(y) \land x=z$$ |
|||
$$f(x)=g(x) \lor z=f(y) \imp f(z) \neq g(y) \land x=z.$$ |
|||
} |
|||
@ -1,3 +1,3 @@ |
|||
\item \ifassignmentsheet \points{2} \fi \applyAckermann{ |
|||
$$ \varphi_{EUF} := f(a,b)=x \land f(x,y)\neq g(a) \lor f(m,n)=b \lor f(g(a),y) \neq a$$ |
|||
$$ \varphi_{EUF} := f(a,b)=x \land f(x,y)\neq g(a) \lor f(m,n)=b \lor f(g(a),y) \neq a.$$ |
|||
} |
|||
@ -0,0 +1,8 @@ |
|||
\item \ifassignmentsheet \points{5} \fi |
|||
Use the lazy encoding approach to check whether the formula $\varphi$ in $\EUF$ is satisfiable. |
|||
\begin{align*} |
|||
\varphi = &(\clause{(f(a)=b); (f(a)=c); \lnot (b=c)}) \land (\clause{(b=c); (a=b); (f(a)=b)})~\land\\ |
|||
&(\clause{\lnot (f(a)=b); (a=b)}) \land (\clause{(b=c); \lnot (a=b); \lnot (f(a)=b)})~\land\\ |
|||
&(\clause{\lnot (f(a)=c); (b=c)}) \land (\clause{\lnot (f(a)=c); (b=c); \lnot (a=b)})~\land\\ |
|||
&(\clause{(f(a)=b); (f(a)=c)}) |
|||
\end{align*} |
|||
@ -0,0 +1,61 @@ |
|||
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} |
|||
} |
|||
|
|||
@ -0,0 +1,98 @@ |
|||
Conflict in step 8\\ |
|||
\scalebox{0.75}{ |
|||
|
|||
\begin{tikzpicture}[>=latex,line join=bevel,] |
|||
\pgfsetlinewidth{1bp} |
|||
%% |
|||
\pgfsetcolor{black} |
|||
% Edge: 1 -> 4 |
|||
\draw [->] (22.3bp,31.0bp) .. controls (35.47bp,31.0bp) and (58.583bp,31.0bp) .. (85.878bp,31.0bp); |
|||
\definecolor{strokecol}{rgb}{0.0,0.0,0.0}; |
|||
\pgfsetstrokecolor{strokecol} |
|||
\draw (54.0bp,38.5bp) node {$$7$$}; |
|||
% Edge: 3 -> 2 |
|||
\draw [->] (193.67bp,47.438bp) .. controls (201.41bp,44.585bp) and (212.51bp,40.495bp) .. (231.47bp,33.51bp); |
|||
% Edge: 4 -> 3 |
|||
\draw [->] (107.97bp,33.373bp) .. controls (121.23bp,36.53bp) and (144.98bp,42.186bp) .. (172.05bp,48.63bp); |
|||
\draw (140.0bp,50.5bp) node {$$5$$}; |
|||
% Edge: 4 -> 5 |
|||
\draw [->] (107.11bp,26.371bp) .. controls (112.48bp,23.828bp) and (119.48bp,20.828bp) .. (126.0bp,19.0bp) .. controls (137.65bp,15.733bp) and (151.06bp,13.758bp) .. (171.92bp,11.639bp); |
|||
\draw (140.0bp,26.5bp) node {$$8$$}; |
|||
% Edge: 5 -> 2 |
|||
\draw [->] (193.67bp,14.223bp) .. controls (201.24bp,16.746bp) and (212.02bp,20.339bp) .. (231.09bp,26.697bp); |
|||
% Node: 1 |
|||
\begin{scope} |
|||
\definecolor{strokecol}{rgb}{0.0,0.0,0.0}; |
|||
\pgfsetstrokecolor{strokecol} |
|||
\draw (11.0bp,31.0bp) ellipse (11.0bp and 11.0bp); |
|||
\draw (11.0bp,31.0bp) node {$\lnot e_{0}$}; |
|||
\end{scope} |
|||
% Node: 4 |
|||
\begin{scope} |
|||
\definecolor{strokecol}{rgb}{0.0,0.0,0.0}; |
|||
\pgfsetstrokecolor{strokecol} |
|||
\draw (97.0bp,31.0bp) ellipse (11.0bp and 11.0bp); |
|||
\draw (97.0bp,31.0bp) node {$e_{1}$}; |
|||
\end{scope} |
|||
% Node: 2 |
|||
\begin{scope} |
|||
\definecolor{strokecol}{rgb}{0.0,0.0,0.0}; |
|||
\pgfsetstrokecolor{strokecol} |
|||
\draw (242.0bp,30.0bp) ellipse (11.0bp and 11.0bp); |
|||
\draw (242.0bp,30.0bp) node {$\bot$}; |
|||
\end{scope} |
|||
% Node: 3 |
|||
\begin{scope} |
|||
\definecolor{strokecol}{rgb}{0.0,0.0,0.0}; |
|||
\pgfsetstrokecolor{strokecol} |
|||
\draw (183.0bp,51.0bp) ellipse (11.0bp and 11.0bp); |
|||
\draw (183.0bp,51.0bp) node {$e_{2}$}; |
|||
\end{scope} |
|||
% Node: 5 |
|||
\begin{scope} |
|||
\definecolor{strokecol}{rgb}{0.0,0.0,0.0}; |
|||
\pgfsetstrokecolor{strokecol} |
|||
\draw (183.0bp,11.0bp) ellipse (11.0bp and 11.0bp); |
|||
\draw (183.0bp,11.0bp) node {$\lnot e_{2}$}; |
|||
\end{scope} |
|||
% |
|||
\end{tikzpicture} |
|||
|
|||
|
|||
} |
|||
\begin{prooftree} |
|||
\AxiomC{$5. \; \lnot e_{1} \lor e_{2}$} |
|||
\AxiomC{$8. \; e_{0} \lor \lnot e_{1} \lor \lnot e_{2}$} |
|||
\BinaryInfC{$\lnot e_{1} \lor e_{0}$} |
|||
\AxiomC{$7. \; e_{0} \lor e_{1}$} |
|||
\BinaryInfC{$e_{0}$} |
|||
\end{prooftree} |
|||
|
|||
\hspace{-0.09cm}\scalebox{0.85}{ |
|||
\begin{dplltabular}{4} |
|||
\dpllStep{9|10|11|12} |
|||
\dpllDecL{0|0|0|0} |
|||
\dpllAssi{ - |$e_{0}$|$e_{0}, e_{3}$|$e_{0}, e_{3}, e_{2}$} |
|||
\dpllClause{1}{$e_{0}, e_{1}, \lnot e_{2}$}{$e_{0}, e_{1}, \lnot e_{2}$|\done|\done|\done} |
|||
\dpllClause{2}{$e_{2}, e_{3}, e_{0}$}{$e_{2}, e_{3}, e_{0}$|\done|\done|\done} |
|||
\dpllClause{3}{$\lnot e_{0}, e_{3}$}{$\lnot e_{0}, e_{3}$|$e_{3}$|\done|\done} |
|||
\dpllClause{4}{$e_{2}, \lnot e_{3}, \lnot e_{0}$}{$e_{2}, \lnot e_{3}, \lnot e_{0}$|$e_{2}, \lnot e_{3}$|$e_{2}$|\done} |
|||
\dpllClause{5}{$\lnot e_{1}, e_{2}$}{$\lnot e_{1}, e_{2}$|$\lnot e_{1}, e_{2}$|$\lnot e_{1}, 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}$|$\lnot e_{1}, e_{2}$|\done} |
|||
\dpllClause{7}{$e_{0}, e_{1}$}{$e_{0}, e_{1}$|\done|\done|\done} |
|||
\dpllClause{8}{$e_{0}, \lnot e_{1}, \lnot e_{2}$}{$e_{0}, \lnot e_{1}, \lnot e_{2}$|\done|\done|\done} |
|||
\dpllClause{9}{$e_{0}$}{$e_{0}$|\done|\done|\done} |
|||
\dpllBCP{$e_{0}$|$e_{3}$|$e_{2}$| - } |
|||
\dpllPL{ - | - | - | - } |
|||
\dpllDeci{ - | - | - |SAT} |
|||
\end{dplltabular} |
|||
} |
|||
|
|||
$\Model_{\EUF} := (f(a) = b) \land (b = c) \land (a = b) $ \\ |
|||
Check if the assignment is consistent with the theory: |
|||
\begin{align*} |
|||
&\{f(a), b\}, \{b, c\}, \{a, b\}\\ |
|||
&\{a, b, c, f(a)\} |
|||
\end{align*} |
|||
$\Model_{\EUF}$ is consistent with the theory, \\ |
|||
$\Rightarrow$ $\Model_{\EUF}$ is a satisfying assignment and $\varphi$ is SAT. |
|||
@ -0,0 +1,9 @@ |
|||
\item \ifassignmentsheet \points{5} \fi |
|||
Use the lazy encoding approach to check whether the formula $\varphi$ in $\EUF$ is satisfiable. |
|||
\begin{align*} |
|||
\varphi =& (\clause{\lnot (f(a)=f(b)); (f(a)=c); (a=b)}) \land (\clause{\lnot (f(a)=c); (a=b); \lnot (f(c)=a)})~\land\\ |
|||
& (\clause{(f(a)=f(b)); \lnot (f(a)=c)}) \land (\clause{\lnot (f(a)=f(b)); (a=b)})~\land \\ |
|||
& (\clause{\lnot (a=b); \lnot (f(c)=a)}) \land (\clause{(f(a)=f(b)); (a=b)})~\land \\ |
|||
& (\clause{\lnot (a=b); \lnot (f(a)=c)}) |
|||
\end{align*} |
|||
|
|||
@ -0,0 +1,37 @@ |
|||
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)=f(b))$ |
|||
\item $e_{1}\Leftrightarrow(f(a)=c)$ |
|||
\item $e_{2}\Leftrightarrow(a=b)$ |
|||
\item $e_{3}\Leftrightarrow(f(c)=a)$ |
|||
\end{itemize} |
|||
|
|||
$\hat{\varphi} = (\clause{\lnot e_{0}; e_{1}; e_{2}}) \land (\clause{\lnot e_{1}; e_{2}; \lnot e_{3}}) \land (\clause{e_{0}; \lnot e_{1}}) \land (\clause{\lnot e_{0}; e_{2}}) \land (\clause{\lnot e_{2}; \lnot e_{3}}) \land (\clause{e_{0}; e_{2}}) \land (\clause{\lnot e_{2}; \lnot e_{1}}) $ |
|||
|
|||
|
|||
\hspace{-0.09cm}\scalebox{0.85}{ |
|||
\begin{dplltabular}{5} |
|||
\dpllStep{1|2|3|4|5} |
|||
\dpllDecL{0|0|1|1|1} |
|||
\dpllAssi{ - |$\lnot e_{3}$|$\lnot e_{3}, \lnot e_{0}$|$\lnot e_{3}, \lnot e_{0}, \lnot e_{1}$|\makecell{$\lnot e_{3}, \lnot e_{0}, \lnot e_{1}, $ \\ $e_{2}$}} |
|||
\dpllClause{1}{$\lnot e_{0}, e_{1}, e_{2}$}{$\lnot e_{0}, e_{1}, e_{2}$|$\lnot e_{0}, e_{1}, e_{2}$|\done|\done|\done} |
|||
\dpllClause{2}{$\lnot e_{1}, e_{2}, \lnot e_{3}$}{$\lnot e_{1}, e_{2}, \lnot e_{3}$|\done|\done|\done|\done} |
|||
\dpllClause{3}{$e_{0}, \lnot e_{1}$}{$e_{0}, \lnot e_{1}$|$e_{0}, \lnot e_{1}$|$\lnot e_{1}$|\done|\done} |
|||
\dpllClause{4}{$\lnot e_{0}, e_{2}$}{$\lnot e_{0}, e_{2}$|$\lnot e_{0}, e_{2}$|\done|\done|\done} |
|||
\dpllClause{5}{$\lnot e_{2}, \lnot e_{3}$}{$\lnot e_{2}, \lnot e_{3}$|\done|\done|\done|\done} |
|||
\dpllClause{6}{$e_{0}, e_{2}$}{$e_{0}, e_{2}$|$e_{0}, e_{2}$|$e_{2}$|$e_{2}$|\done} |
|||
\dpllClause{7}{$\lnot e_{2}, \lnot e_{1}$}{$\lnot e_{2}, \lnot e_{1}$|$\lnot e_{2}, \lnot e_{1}$|$\lnot e_{2}, \lnot e_{1}$|\done|\done} |
|||
\dpllBCP{ - | - |$\lnot e_{1}$|$e_{2}$| - } |
|||
\dpllPL{$\lnot e_{3}$| - | - | - | - } |
|||
\dpllDeci{ - |$\lnot e_{0}$| - | - |SAT} |
|||
\end{dplltabular} |
|||
} |
|||
|
|||
$\Model_{\EUF} := (f(a) \neq f(b)) \land (f(a) \neq c) \land (a = b) \land (f(c) \neq a) $ \\ |
|||
Check if the assignment is consistent with the theory: |
|||
|
|||
\begin{align*} |
|||
&\{a, b\}, \{f(a)\}, \{f(b)\}, \{c\}, \{f(c)\} |
|||
\end{align*} |
|||
|
|||
$\Model_{\EUF}$ is consistent with the theory, \\$\Rightarrow \Model_{\EUF}$ is a satisfying assignment and $\varphi$ is SAT. |
|||
@ -0,0 +1,9 @@ |
|||
\item \ifassignmentsheet \points{5} \fi |
|||
Use the lazy encoding approach to check whether the formula $\varphi$ in $\EUF$ is satisfiable. |
|||
\begin{align*} |
|||
\varphi =& (\clause{(a=x); (a=y); (x=y)})\land (\clause{\lnot (a=x); (a=y)})~\land \\ |
|||
& (\clause{\lnot (a=y); (x=y)})\land (\clause{(x=y); (z=a)})~\land \\ |
|||
& (\clause{\lnot (x=y); (b=z)})\land (\clause{\lnot (z=a); \lnot (b=z)}) |
|||
\end{align*} |
|||
|
|||
|
|||
@ -0,0 +1,36 @@ |
|||
We start by translating $\varphi$ to $\hat{\varphi} = \skel$ and assign the following variables to the theory literals: |
|||
\begin{itemize} |
|||
\item $e_{0}\Leftrightarrow(a=x)$ |
|||
\item $e_{1}\Leftrightarrow(a=y)$ |
|||
\item $e_{2}\Leftrightarrow(x=y)$ |
|||
\item $e_{3}\Leftrightarrow(z=a)$ |
|||
\item $e_{4}\Leftrightarrow(b=z)$ |
|||
\end{itemize} |
|||
|
|||
$\hat{\varphi} = (\clause{e_{0}; e_{1}; e_{2}})\land (\clause{\lnot e_{0}; e_{1}})\land (\clause{\lnot e_{1}; e_{2}})\land (\clause{e_{2}; e_{3}})\land (\clause{\lnot e_{2}; e_{4}})\land (\clause{\lnot e_{3}; \lnot e_{4}})$ |
|||
|
|||
\hspace{-0.09cm}\scalebox{0.85}{ |
|||
\begin{dplltabular}{6} |
|||
\dpllStep{1|2|3|4|5|6} |
|||
\dpllDecL{0|1|2|2|2|2} |
|||
\dpllAssi{ - |$\lnot e_{0}$|$\lnot e_{0}, \lnot e_{1}$|$\lnot e_{0}, \lnot e_{1}, e_{2}$|\makecell{$\lnot e_{0}, \lnot e_{1}, e_{2}, $ \\ $e_{4}$}|\makecell{$\lnot e_{0}, \lnot e_{1}, e_{2}, $ \\ $e_{4}, \lnot e_{3}$}} |
|||
\dpllClause{1}{$e_{0}, e_{1}, e_{2}$}{$e_{0}, e_{1}, e_{2}$|$e_{1}, e_{2}$|$e_{2}$|\done|\done|\done} |
|||
\dpllClause{2}{$\lnot e_{0}, e_{1}$}{$\lnot e_{0}, e_{1}$|\done|\done|\done|\done|\done} |
|||
\dpllClause{3}{$\lnot e_{1}, e_{2}$}{$\lnot e_{1}, e_{2}$|$\lnot e_{1}, e_{2}$|\done|\done|\done|\done} |
|||
\dpllClause{4}{$e_{2}, e_{3}$}{$e_{2}, e_{3}$|$e_{2}, e_{3}$|$e_{2}, e_{3}$|\done|\done|\done} |
|||
\dpllClause{5}{$\lnot e_{2}, e_{4}$}{$\lnot e_{2}, e_{4}$|$\lnot e_{2}, e_{4}$|$\lnot e_{2}, e_{4}$|$e_{4}$|\done|\done} |
|||
\dpllClause{6}{$\lnot e_{3}, \lnot e_{4}$}{$\lnot e_{3}, \lnot e_{4}$|$\lnot e_{3}, \lnot e_{4}$|$\lnot e_{3}, \lnot e_{4}$|$\lnot e_{3}, \lnot e_{4}$|$\lnot e_{3}$|\done} |
|||
\dpllBCP{ - | - |$e_{2}$|$e_{4}$|$\lnot e_{3}$| - } |
|||
\dpllPL{ - | - | - | - | - | - } |
|||
\dpllDeci{$\lnot e_{0}$|$\lnot e_{1}$| - | - | - |SAT} |
|||
\end{dplltabular} |
|||
} |
|||
|
|||
$\Model_{\EUF} := (a \neq x) \land (a \neq y) \land (x = y) \land (z \neq a) \land (b = z) $ \\ |
|||
Check if the assignment is consistent with the theory: |
|||
|
|||
\begin{align*} |
|||
&\{x, y\}, \{b, z\}, \{a\} |
|||
\end{align*} |
|||
|
|||
$\Model_{\EUF}$ is consistent with the theory, \\$\Rightarrow \Model_{\EUF}$ is a satisfying assignment and $\varphi$ is SAT. |
|||
@ -0,0 +1,8 @@ |
|||
\item \ifassignmentsheet \points{5} \fi |
|||
Use the lazy encoding approach to check whether the formula $\varphi$ in $\EUF$ is satisfiable. |
|||
\begin{align*} |
|||
\varphi =&(\clause{(f(x)=x); (f(x)=y); (x=y)}) \land (\clause{\lnot (f(x)=x); (f(x)=y)})~\land \\ |
|||
&(\clause{\lnot (f(x)=y); (x=y)}) \land (\clause{(x=y); (z=f(x))})~\land \\ |
|||
&(\clause{\lnot (x=y); (f(x)=y)}) \land (\clause{\lnot (z=f(x)); \lnot (f(x)=y)}) |
|||
\end{align*} |
|||
|
|||
@ -0,0 +1,126 @@ |
|||
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(x)=x)$ |
|||
\item $e_{1}\Leftrightarrow(f(x)=y)$ |
|||
\item $e_{2}\Leftrightarrow(x=y)$ |
|||
\item $e_{3}\Leftrightarrow(z=f(x))$ |
|||
\end{itemize} |
|||
|
|||
|
|||
$\hat{\varphi} = (\clause{e_{0}; e_{1}; e_{2}}) \land (\clause{\lnot e_{0}; e_{1}}) \land (\clause{\lnot e_{1}; e_{2}}) \land (\clause{e_{2}; e_{3}}) \land (\clause{\lnot e_{2}; e_{1}}) \land (\clause{\lnot e_{3}; \lnot e_{1}}) $ |
|||
|
|||
|
|||
\hspace{-0.09cm}\scalebox{0.85}{ |
|||
\begin{dplltabular}{4} |
|||
\dpllStep{1|2|3|4} |
|||
\dpllDecL{0|1|2|2} |
|||
\dpllAssi{ - |$\lnot e_{0}$|$\lnot e_{0}, \lnot e_{1}$|$\lnot e_{0}, \lnot e_{1}, \lnot e_{2}$} |
|||
\dpllClause{1}{$e_{0}, e_{1}, e_{2}$}{$e_{0}, e_{1}, e_{2}$|$e_{1}, e_{2}$|$e_{2}$|\conflict} |
|||
\dpllClause{2}{$\lnot e_{0}, e_{1}$}{$\lnot e_{0}, e_{1}$|\done|\done|\done} |
|||
\dpllClause{3}{$\lnot e_{1}, e_{2}$}{$\lnot e_{1}, e_{2}$|$\lnot e_{1}, e_{2}$|\done|\done} |
|||
\dpllClause{4}{$e_{2}, e_{3}$}{$e_{2}, e_{3}$|$e_{2}, e_{3}$|$e_{2}, e_{3}$|$e_{3}$} |
|||
\dpllClause{5}{$\lnot e_{2}, e_{1}$}{$\lnot e_{2}, e_{1}$|$\lnot e_{2}, e_{1}$|$\lnot e_{2}$|\done} |
|||
\dpllClause{6}{$\lnot e_{3}, \lnot e_{1}$}{$\lnot e_{3}, \lnot e_{1}$|$\lnot e_{3}, \lnot e_{1}$|\done|\done} |
|||
\dpllBCP{ - | - |$\lnot e_{2}$| - } |
|||
\dpllPL{ - | - | - | - } |
|||
\dpllDeci{$\lnot e_{0}$|$\lnot e_{1}$| - | - } |
|||
\end{dplltabular} |
|||
} |
|||
|
|||
Conflict in step 4\\ |
|||
\scalebox{0.75}{ |
|||
|
|||
\begin{tikzpicture}[>=latex,line join=bevel,] |
|||
\pgfsetlinewidth{1bp} |
|||
%% |
|||
\pgfsetcolor{black} |
|||
% Edge: 1 -> 4 |
|||
\draw [->] (21.08bp,83.506bp) .. controls (26.44bp,80.758bp) and (33.44bp,77.508bp) .. (40.0bp,75.5bp) .. controls (51.601bp,71.949bp) and (65.006bp,69.732bp) .. (85.898bp,67.281bp); |
|||
\definecolor{strokecol}{rgb}{0.0,0.0,0.0}; |
|||
\pgfsetstrokecolor{strokecol} |
|||
\draw (54.0bp,83.0bp) node {$$1$$}; |
|||
% Edge: 1 -> 5 |
|||
\draw [->] (21.966bp,90.636bp) .. controls (35.227bp,93.477bp) and (58.98bp,98.567bp) .. (86.047bp,104.37bp); |
|||
\draw (54.0bp,107.0bp) node {$$5$$}; |
|||
% Edge: 2 -> 4 |
|||
\draw [->] (21.717bp,33.396bp) .. controls (33.05bp,36.904bp) and (52.243bp,43.253bp) .. (68.0bp,50.5bp) .. controls (71.462bp,52.092bp) and (75.062bp,53.969bp) .. (87.382bp,61.048bp); |
|||
\draw (54.0bp,58.0bp) node {$$1$$}; |
|||
% Edge: 4 -> 3 |
|||
\draw [->] (107.67bp,69.723bp) .. controls (115.24bp,72.246bp) and (126.02bp,75.839bp) .. (145.09bp,82.197bp); |
|||
% Edge: 5 -> 3 |
|||
\draw [->] (107.67bp,102.94bp) .. controls (115.41bp,100.08bp) and (126.51bp,95.995bp) .. (145.47bp,89.01bp); |
|||
% Node: 1 |
|||
\begin{scope} |
|||
\definecolor{strokecol}{rgb}{0.0,0.0,0.0}; |
|||
\pgfsetstrokecolor{strokecol} |
|||
\draw (11.0bp,88.5bp) ellipse (11.0bp and 11.0bp); |
|||
\draw (11.0bp,88.5bp) node {$\lnot e_{1}$}; |
|||
\end{scope} |
|||
% Node: 4 |
|||
\begin{scope} |
|||
\definecolor{strokecol}{rgb}{0.0,0.0,0.0}; |
|||
\pgfsetstrokecolor{strokecol} |
|||
\draw (97.0bp,66.5bp) ellipse (11.0bp and 11.0bp); |
|||
\draw (97.0bp,66.5bp) node {$e_{2}$}; |
|||
\end{scope} |
|||
% Node: 5 |
|||
\begin{scope} |
|||
\definecolor{strokecol}{rgb}{0.0,0.0,0.0}; |
|||
\pgfsetstrokecolor{strokecol} |
|||
\draw (97.0bp,106.5bp) ellipse (11.0bp and 11.0bp); |
|||
\draw (97.0bp,106.5bp) node {$\lnot e_{2}$}; |
|||
\end{scope} |
|||
% Node: 2 |
|||
\begin{scope} |
|||
\definecolor{strokecol}{rgb}{0.0,0.0,0.0}; |
|||
\pgfsetstrokecolor{strokecol} |
|||
\draw (11.0bp,30.5bp) ellipse (11.0bp and 11.0bp); |
|||
\draw (11.0bp,30.5bp) node {$\lnot e_{0}$}; |
|||
\end{scope} |
|||
% Node: 3 |
|||
\begin{scope} |
|||
\definecolor{strokecol}{rgb}{0.0,0.0,0.0}; |
|||
\pgfsetstrokecolor{strokecol} |
|||
\draw (156.0bp,85.5bp) ellipse (11.0bp and 11.0bp); |
|||
\draw (156.0bp,85.5bp) node {$\bot$}; |
|||
\end{scope} |
|||
% |
|||
\end{tikzpicture} |
|||
|
|||
|
|||
} |
|||
\begin{prooftree} |
|||
\AxiomC{$1. \; e_{0} \lor e_{1} \lor e_{2}$} |
|||
\AxiomC{$5. \; \lnot e_{2} \lor e_{1}$} |
|||
\BinaryInfC{$e_{0} \lor e_{1}$} |
|||
\end{prooftree} |
|||
|
|||
\hspace{-0.09cm}\scalebox{0.85}{ |
|||
\begin{dplltabular}{4} |
|||
\dpllStep{5|6|7|8} |
|||
\dpllDecL{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_{1}, e_{2}$|\done|\done|\done} |
|||
\dpllClause{2}{$\lnot e_{0}, e_{1}$}{\done|\done|\done|\done} |
|||
\dpllClause{3}{$\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}$|\done|\done} |
|||
\dpllClause{5}{$\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_{3}$|\done} |
|||
\dpllClause{7}{$e_{0}, e_{1}$}{$e_{1}$|\done|\done|\done} |
|||
\dpllBCP{$e_{1}$|$e_{2}$|$\lnot e_{3}$| - } |
|||
\dpllPL{ - | - | - | - } |
|||
\dpllDeci{ - | - | - | - } |
|||
\end{dplltabular} |
|||
} |
|||
|
|||
$\Model_{\EUF} := (f(x) \neq 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), y\}, \{x, y\}, \{z\}\\ |
|||
&\{z\}, \{f(x), x, y\} |
|||
\end{align*} |
|||
|
|||
$\Model_{\EUF}$ is not consistent with the theory, because of: $(f(x) \neq x) $\\ |
|||
$\Rightarrow$ We need to add a blocking clause from $\Model_{\EUF}: \\ $ |
|||
$BC :=e_{0} \lor \neg e_{1} \lor \neg e_{2} \lor e_{3}$\\ |
|||
@ -0,0 +1,133 @@ |
|||
\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. |
|||
@ -0,0 +1,7 @@ |
|||
\item \ifassignmentsheet \points{5} \fi |
|||
Use the lazy encoding approach to check whether the formula $\varphi$ in $\EUF$ is satisfiable. |
|||
\begin{align*} |
|||
\varphi= & (\clause{(a=b); (a=f(a)); (b=f(a))}) \land (\clause{\lnot (a=b); (a=f(a))})~\land \\ |
|||
& (\clause{\lnot (a=f(a)); (b=f(a))}) \land (\clause{(b=f(a)); (d=a)})~\land \\ |
|||
& (\clause{\lnot (b=f(a)); (a=f(a))}) \land (\clause{\lnot (d=a); \lnot (a=f(a))}) |
|||
\end{align*} |
|||
@ -0,0 +1,125 @@ |
|||
We start by translating $\varphi$ to $\hat{\varphi} = \skel$ and assign the following variables to the theory literals: |
|||
\begin{itemize} |
|||
\item $e_{0}\Leftrightarrow(a=b)$ |
|||
\item $e_{1}\Leftrightarrow(a=f(a))$ |
|||
\item $e_{2}\Leftrightarrow(b=f(a))$ |
|||
\item $e_{3}\Leftrightarrow(d=a)$ |
|||
\end{itemize} |
|||
|
|||
$ \hat{\varphi} = (\clause{e_{0}; e_{1}; e_{2}}) \land (\clause{\lnot e_{0}; e_{1}}) \land (\clause{\lnot e_{1}; e_{2}}) \land (\clause{e_{2}; e_{3}}) \land (\clause{\lnot e_{2}; e_{1}}) \land (\clause{\lnot e_{3}; \lnot e_{1}}) $ |
|||
|
|||
\hspace{-0.09cm}\scalebox{0.85}{ |
|||
\begin{dplltabular}{4} |
|||
\dpllStep{1|2|3|4} |
|||
\dpllDecL{0|1|2|2} |
|||
\dpllAssi{ - |$\lnot e_{0}$|$\lnot e_{0}, \lnot e_{1}$|$\lnot e_{0}, \lnot e_{1}, \lnot e_{2}$} |
|||
\dpllClause{1}{$e_{0}, e_{1}, e_{2}$}{$e_{0}, e_{1}, e_{2}$|$e_{1}, e_{2}$|$e_{2}$|\conflict} |
|||
\dpllClause{2}{$\lnot e_{0}, e_{1}$}{$\lnot e_{0}, e_{1}$|\done|\done|\done} |
|||
\dpllClause{3}{$\lnot e_{1}, e_{2}$}{$\lnot e_{1}, e_{2}$|$\lnot e_{1}, e_{2}$|\done|\done} |
|||
\dpllClause{4}{$e_{2}, e_{3}$}{$e_{2}, e_{3}$|$e_{2}, e_{3}$|$e_{2}, e_{3}$|$e_{3}$} |
|||
\dpllClause{5}{$\lnot e_{2}, e_{1}$}{$\lnot e_{2}, e_{1}$|$\lnot e_{2}, e_{1}$|$\lnot e_{2}$|\done} |
|||
\dpllClause{6}{$\lnot e_{3}, \lnot e_{1}$}{$\lnot e_{3}, \lnot e_{1}$|$\lnot e_{3}, \lnot e_{1}$|\done|\done} |
|||
\dpllBCP{ - | - |$\lnot e_{2}$| - } |
|||
\dpllPL{ - | - | - | - } |
|||
\dpllDeci{$\lnot e_{0}$|$\lnot e_{1}$| - | - } |
|||
\end{dplltabular} |
|||
} |
|||
|
|||
Conflict in step 4\\ |
|||
\scalebox{0.75}{ |
|||
|
|||
\begin{tikzpicture}[>=latex,line join=bevel,] |
|||
\pgfsetlinewidth{1bp} |
|||
%% |
|||
\pgfsetcolor{black} |
|||
% Edge: 1 -> 4 |
|||
\draw [->] (21.08bp,83.506bp) .. controls (26.44bp,80.758bp) and (33.44bp,77.508bp) .. (40.0bp,75.5bp) .. controls (51.601bp,71.949bp) and (65.006bp,69.732bp) .. (85.898bp,67.281bp); |
|||
\definecolor{strokecol}{rgb}{0.0,0.0,0.0}; |
|||
\pgfsetstrokecolor{strokecol} |
|||
\draw (54.0bp,83.0bp) node {$$1$$}; |
|||
% Edge: 1 -> 5 |
|||
\draw [->] (21.966bp,90.636bp) .. controls (35.227bp,93.477bp) and (58.98bp,98.567bp) .. (86.047bp,104.37bp); |
|||
\draw (54.0bp,107.0bp) node {$$5$$}; |
|||
% Edge: 2 -> 4 |
|||
\draw [->] (21.717bp,33.396bp) .. controls (33.05bp,36.904bp) and (52.243bp,43.253bp) .. (68.0bp,50.5bp) .. controls (71.462bp,52.092bp) and (75.062bp,53.969bp) .. (87.382bp,61.048bp); |
|||
\draw (54.0bp,58.0bp) node {$$1$$}; |
|||
% Edge: 4 -> 3 |
|||
\draw [->] (107.67bp,69.723bp) .. controls (115.24bp,72.246bp) and (126.02bp,75.839bp) .. (145.09bp,82.197bp); |
|||
% Edge: 5 -> 3 |
|||
\draw [->] (107.67bp,102.94bp) .. controls (115.41bp,100.08bp) and (126.51bp,95.995bp) .. (145.47bp,89.01bp); |
|||
% Node: 1 |
|||
\begin{scope} |
|||
\definecolor{strokecol}{rgb}{0.0,0.0,0.0}; |
|||
\pgfsetstrokecolor{strokecol} |
|||
\draw (11.0bp,88.5bp) ellipse (11.0bp and 11.0bp); |
|||
\draw (11.0bp,88.5bp) node {$\lnot e_{1}$}; |
|||
\end{scope} |
|||
% Node: 4 |
|||
\begin{scope} |
|||
\definecolor{strokecol}{rgb}{0.0,0.0,0.0}; |
|||
\pgfsetstrokecolor{strokecol} |
|||
\draw (97.0bp,66.5bp) ellipse (11.0bp and 11.0bp); |
|||
\draw (97.0bp,66.5bp) node {$e_{2}$}; |
|||
\end{scope} |
|||
% Node: 5 |
|||
\begin{scope} |
|||
\definecolor{strokecol}{rgb}{0.0,0.0,0.0}; |
|||
\pgfsetstrokecolor{strokecol} |
|||
\draw (97.0bp,106.5bp) ellipse (11.0bp and 11.0bp); |
|||
\draw (97.0bp,106.5bp) node {$\lnot e_{2}$}; |
|||
\end{scope} |
|||
% Node: 2 |
|||
\begin{scope} |
|||
\definecolor{strokecol}{rgb}{0.0,0.0,0.0}; |
|||
\pgfsetstrokecolor{strokecol} |
|||
\draw (11.0bp,30.5bp) ellipse (11.0bp and 11.0bp); |
|||
\draw (11.0bp,30.5bp) node {$\lnot e_{0}$}; |
|||
\end{scope} |
|||
% Node: 3 |
|||
\begin{scope} |
|||
\definecolor{strokecol}{rgb}{0.0,0.0,0.0}; |
|||
\pgfsetstrokecolor{strokecol} |
|||
\draw (156.0bp,85.5bp) ellipse (11.0bp and 11.0bp); |
|||
\draw (156.0bp,85.5bp) node {$\bot$}; |
|||
\end{scope} |
|||
% |
|||
\end{tikzpicture} |
|||
|
|||
|
|||
} |
|||
\begin{prooftree} |
|||
\AxiomC{$1. \; e_{0} \lor e_{1} \lor e_{2}$} |
|||
\AxiomC{$5. \; \lnot e_{2} \lor e_{1}$} |
|||
\BinaryInfC{$e_{0} \lor e_{1}$} |
|||
\end{prooftree} |
|||
|
|||
\hspace{-0.09cm}\scalebox{0.85}{ |
|||
\begin{dplltabular}{4} |
|||
\dpllStep{5|6|7|8} |
|||
\dpllDecL{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_{1}, e_{2}$|\done|\done|\done} |
|||
\dpllClause{2}{$\lnot e_{0}, e_{1}$}{\done|\done|\done|\done} |
|||
\dpllClause{3}{$\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}$|\done|\done} |
|||
\dpllClause{5}{$\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_{3}$|\done} |
|||
\dpllClause{7}{$e_{0}, e_{1}$}{$e_{1}$|\done|\done|\done} |
|||
\dpllBCP{$e_{1}$|$e_{2}$|$\lnot e_{3}$| - } |
|||
\dpllPL{ - | - | - | - } |
|||
\dpllDeci{ - | - | - | - } |
|||
\end{dplltabular} |
|||
} |
|||
|
|||
$\Model_{\EUF} := (a \neq b) \land (a = f(a)) \land (b = f(a)) \land (d \neq a) $ \\ |
|||
Check if the assignment is consistent with the theory: |
|||
|
|||
\begin{align*} |
|||
&\{a, f(a)\}, \{b, f(a)\}, \{d\}\\ |
|||
&\{d\}, \{a, b, f(a)\} |
|||
\end{align*} |
|||
|
|||
$\Model_{\EUF}$ is not consistent with the theory, because of: $(a \neq b) $\\ |
|||
$\Rightarrow$ We need to add a blocking clause from $\Model_{\EUF}: \\ $ |
|||
$BC :=e_{0} \lor \neg e_{1} \lor \neg e_{2} \lor e_{3}$\\ |
|||
|
|||
@ -0,0 +1,133 @@ |
|||
\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} := (a = b) \land (a = f(a)) \land (b = f(a)) \land (d \neq a) $ \\ |
|||
Check if the assignment is consistent with the theory: |
|||
|
|||
\begin{align*} |
|||
&\{a, b\}, \{a, f(a)\}, \{b, f(a)\}, \{d\}\\ |
|||
&\{d\}, \{a, b, f(a)\} |
|||
\end{align*} |
|||
|
|||
$\Model_{\EUF}$ is consistent with the theory, \\$\Rightarrow \Model_{\EUF}$ is a satisfying assignment and $\varphi$ is SAT. |
|||
@ -0,0 +1,7 @@ |
|||
\item \ifassignmentsheet \points{5} \fi |
|||
Use the lazy encoding approach to check whether the formula $\varphi$ in $\EUF$ is satisfiable. |
|||
\begin{align*} |
|||
\varphi = & (\clause{(a=b); (a=f(a))}) \land (\clause{(f(a)=b); (c=b); (f(a)=c)})~\land \\ |
|||
& (\clause{(f(b)=c); \lnot (f(a)=b); \lnot (f(a)=c)}) \land (\clause{\lnot (a=b); \lnot (a=f(a))})~\land \\ |
|||
& (\clause{(a=f(a)); \lnot (c=b)}) |
|||
\end{align*} |
|||
@ -0,0 +1,39 @@ |
|||
We start by translating $\varphi$ to $\hat{\varphi} = \skel$ and assign the following variables to the theory literals: |
|||
\begin{itemize} |
|||
\item $e_{0}\Leftrightarrow(a=b)$ |
|||
\item $e_{1}\Leftrightarrow(a=f(a))$ |
|||
\item $e_{2}\Leftrightarrow(f(a)=b)$ |
|||
\item $e_{3}\Leftrightarrow(c=b)$ |
|||
\item $e_{4}\Leftrightarrow(f(a)=c)$ |
|||
\item $e_{5}\Leftrightarrow(f(b)=c)$ |
|||
\end{itemize} |
|||
|
|||
$\hat{\varphi} = (\clause{e_{0}; e_{1}}) \land (\clause{e_{2}; e_{3}; e_{4}}) \land (\clause{e_{5}; \lnot e_{2}; \lnot e_{4}}) \land (\clause{\lnot e_{0}; \lnot e_{1}}) \land (\clause{e_{1}; \lnot e_{3}}) $ |
|||
|
|||
\hspace{-0.09cm}\scalebox{0.85}{ |
|||
\begin{dplltabular}{6} |
|||
\dpllStep{1|2|3|4|5|6} |
|||
\dpllDecL{0|0|0|0|1|1} |
|||
\dpllAssi{ - |$e_{5}$|$e_{5}, e_{2}$|$e_{5}, e_{2}, \lnot e_{3}$|\makecell{$e_{5}, e_{2}, \lnot e_{3}, $ \\ $\lnot e_{0}$}|\makecell{$e_{5}, e_{2}, \lnot e_{3}, $ \\ $\lnot e_{0}, e_{1}$}} |
|||
\dpllClause{1}{$e_{0}, e_{1}$}{$e_{0}, e_{1}$|$e_{0}, e_{1}$|$e_{0}, e_{1}$|$e_{0}, e_{1}$|$e_{1}$|\done} |
|||
\dpllClause{2}{$e_{2}, e_{3}, e_{4}$}{$e_{2}, e_{3}, e_{4}$|$e_{2}, e_{3}, e_{4}$|\done|\done|\done|\done} |
|||
\dpllClause{3}{$e_{5}, \lnot e_{2}, \lnot e_{4}$}{$e_{5}, \lnot e_{2}, \lnot e_{4}$|\done|\done|\done|\done|\done} |
|||
\dpllClause{4}{$\lnot e_{0}, \lnot e_{1}$}{$\lnot e_{0}, \lnot e_{1}$|$\lnot e_{0}, \lnot e_{1}$|$\lnot e_{0}, \lnot e_{1}$|$\lnot e_{0}, \lnot e_{1}$|\done|\done} |
|||
\dpllClause{5}{$e_{1}, \lnot e_{3}$}{$e_{1}, \lnot e_{3}$|$e_{1}, \lnot e_{3}$|$e_{1}, \lnot e_{3}$|\done|\done|\done} |
|||
\dpllBCP{ - | - | - | - |$e_{1}$| - } |
|||
\dpllPL{$e_{5}$|$e_{2}$|$\lnot e_{3}$| - | - | - } |
|||
\dpllDeci{ - | - | - |$\lnot e_{0}$| - | - } |
|||
\end{dplltabular} |
|||
} |
|||
|
|||
$\Model_{\EUF} := (a \neq b) \land (a = f(a)) \land (f(a) = b) \land (c \neq b) \land (f(b) = c) $ \\ |
|||
Check if the assignment is consistent with the theory: |
|||
|
|||
\begin{align*} |
|||
&\{a, f(a)\}, \{f(a), b\}, \{f(b), c\}\\ |
|||
&\{f(b), c\}, \{a, b, f(a)\} |
|||
\end{align*} |
|||
|
|||
$\Model_{\EUF}$ is not consistent with the theory, because of: $(a \neq b) $\\ |
|||
$\Rightarrow$ We need to add a blocking clause from $\Model_{\EUF}: \\ $ |
|||
$BC :=\neg e_{5} \lor \neg e_{2} \lor e_{3} \lor e_{0} \lor \neg e_{1}$\\ |
|||
@ -0,0 +1,26 @@ |
|||
|
|||
\hspace{-0.09cm}\scalebox{0.85}{ |
|||
\begin{dplltabular}{5} |
|||
\dpllStep{7|8|9|10|11} |
|||
\dpllDecL{0|1|1|1|1} |
|||
\dpllAssi{ - |$\lnot e_{0}$|$\lnot e_{0}, e_{1}$|$\lnot e_{0}, e_{1}, e_{3}$|\makecell{$\lnot e_{0}, e_{1}, e_{3}, $ \\ $\lnot e_{2}$}} |
|||
\dpllClause{1}{$e_{0}, e_{1}$}{$e_{0}, e_{1}$|$e_{1}$|\done|\done|\done} |
|||
\dpllClause{2}{$e_{2}, e_{3}, e_{4}$}{$e_{2}, e_{3}, e_{4}$|$e_{2}, e_{3}, e_{4}$|$e_{2}, e_{3}, e_{4}$|\done|\done} |
|||
\dpllClause{3}{$e_{5}, \lnot e_{2}, \lnot e_{4}$}{$e_{5}, \lnot e_{2}, \lnot e_{4}$|$e_{5}, \lnot e_{2}, \lnot e_{4}$|$e_{5}, \lnot e_{2}, \lnot e_{4}$|$e_{5}, \lnot e_{2}, \lnot e_{4}$|\done} |
|||
\dpllClause{4}{$\lnot e_{0}, \lnot e_{1}$}{$\lnot e_{0}, \lnot e_{1}$|\done|\done|\done|\done} |
|||
\dpllClause{5}{$e_{1}, \lnot e_{3}$}{$e_{1}, \lnot e_{3}$|$e_{1}, \lnot e_{3}$|\done|\done|\done} |
|||
\dpllClause{6}{$\lnot e_{5}, \lnot e_{2}, e_{3}, e_{0}, \lnot e_{1}$}{\makecell{$\lnot e_{5}, \lnot e_{2}, e_{3}, $ \\ $e_{0}, \lnot e_{1}$}|\makecell{$\lnot e_{5}, \lnot e_{2}, e_{3}, $ \\ $\lnot e_{1}$}|$\lnot e_{5}, \lnot e_{2}, e_{3}$|\done|\done} |
|||
\dpllBCP{ - |$e_{1}$| - | - | - } |
|||
\dpllPL{ - | - |$e_{3}$|$\lnot e_{2}$| - } |
|||
\dpllDeci{$\lnot e_{0}$| - | - | - |SAT} |
|||
\end{dplltabular} |
|||
} |
|||
|
|||
$\Model_{\EUF} := (a \neq b) \land (a = f(a)) \land (f(a) \neq b) \land (c = b) $ \\ |
|||
Check if the assignment is consistent with the theory: |
|||
|
|||
\begin{align*} |
|||
&\{a, f(a)\}, \{c, b\} |
|||
\end{align*} |
|||
|
|||
$\Model_{\EUF}$ is consistent with the theory, \\$\Rightarrow \Model_{\EUF}$ is a satisfying assignment and $\varphi$ is SAT. |
|||
@ -0,0 +1,7 @@ |
|||
\item \ifassignmentsheet \points{5} \fi |
|||
Use the lazy encoding approach to check whether the formula $\varphi$ in $\EUF$ is satisfiable. |
|||
\begin{align*} |
|||
\varphi = &(\clause{\lnot (y=f(x)); \lnot (y=f(y))}) \land (\clause{(y=f(x)); (y=f(y))})~\land\\ |
|||
&(\clause{(f(x)=z); (f(y)=x); \lnot (f(y)=z)}) \land (\clause{(y=f(y)); \lnot (z=x)})~\land\\ |
|||
&(\clause{(f(y)=x); (z=x); (f(y)=z)}) \land (\clause{(y=f(x)); (z=x)}) |
|||
\end{align*} |
|||
@ -0,0 +1,41 @@ |
|||
|
|||
We start by translating $\varphi$ to $\hat{\varphi} = \skel$ and assign the following variables to the theory literals: |
|||
\begin{itemize} |
|||
\item $e_{0}\Leftrightarrow(y=f(x))$ |
|||
\item $e_{1}\Leftrightarrow(y=f(y))$ |
|||
\item $e_{2}\Leftrightarrow(f(x)=z)$ |
|||
\item $e_{3}\Leftrightarrow(f(y)=x)$ |
|||
\item $e_{4}\Leftrightarrow(f(y)=z)$ |
|||
\item $e_{5}\Leftrightarrow(z=x)$ |
|||
\end{itemize} |
|||
|
|||
$\hat{\varphi} = (\clause{\lnot e_{0}; \lnot e_{1}}) \land (\clause{e_{0}; e_{1}}) \land (\clause{e_{2}; e_{3}; \lnot e_{4}}) \land (\clause{e_{1}; \lnot e_{5}}) \land (\clause{e_{3}; e_{5}; e_{4}}) \land (\clause{e_{0}; e_{5}})$ |
|||
|
|||
\hspace{-0.09cm}\scalebox{0.85}{ |
|||
\begin{dplltabular}{6} |
|||
\dpllStep{1|2|3|4|5|6} |
|||
\dpllDecL{0|0|0|1|1|1} |
|||
\dpllAssi{ - |$e_{2}$|$e_{2}, e_{3}$|$e_{2}, e_{3}, \lnot e_{0}$|\makecell{$e_{2}, e_{3}, \lnot e_{0}, $ \\ $e_{1}$}|\makecell{$e_{2}, e_{3}, \lnot e_{0}, $ \\ $e_{1}, e_{5}$}} |
|||
\dpllClause{1}{$\lnot e_{0}, \lnot e_{1}$}{$\lnot e_{0}, \lnot e_{1}$|$\lnot e_{0}, \lnot e_{1}$|$\lnot e_{0}, \lnot e_{1}$|\done|\done|\done} |
|||
\dpllClause{2}{$e_{0}, e_{1}$}{$e_{0}, e_{1}$|$e_{0}, e_{1}$|$e_{0}, e_{1}$|$e_{1}$|\done|\done} |
|||
\dpllClause{3}{$e_{2}, e_{3}, \lnot e_{4}$}{$e_{2}, e_{3}, \lnot e_{4}$|\done|\done|\done|\done|\done} |
|||
\dpllClause{4}{$e_{1}, \lnot e_{5}$}{$e_{1}, \lnot e_{5}$|$e_{1}, \lnot e_{5}$|$e_{1}, \lnot e_{5}$|$e_{1}, \lnot e_{5}$|\done|\done} |
|||
\dpllClause{5}{$e_{3}, e_{5}, e_{4}$}{$e_{3}, e_{5}, e_{4}$|$e_{3}, e_{5}, e_{4}$|\done|\done|\done|\done} |
|||
\dpllClause{6}{$e_{0}, e_{5}$}{$e_{0}, e_{5}$|$e_{0}, e_{5}$|$e_{0}, e_{5}$|$e_{5}$|$e_{5}$|\done} |
|||
\dpllBCP{ - | - | - |$e_{1}$|$e_{5}$| - } |
|||
\dpllPL{$e_{2}$|$e_{3}$| - | - | - | - } |
|||
\dpllDeci{ - | - |$\lnot e_{0}$| - | - | - } |
|||
\end{dplltabular} |
|||
} |
|||
|
|||
$\Model_{\EUF} := (y \neq f(x)) \land (y = f(y)) \land (f(x) = z) \land (f(y) = x) \land (z = x) $ \\ |
|||
Check if the assignment is consistent with the theory: |
|||
|
|||
\begin{align*} |
|||
&\{y, f(y)\}, \{f(x), z\}, \{f(y), x\}, \{z, x\}\\ |
|||
&\{f(x), f(y), x, y, z\} |
|||
\end{align*} |
|||
|
|||
$\Model_{\EUF}$ is not consistent with the theory, because of: $(y \neq f(x)) $\\ |
|||
$\Rightarrow$ We need to add a blocking clause from $\Model_{\EUF}: \\ $ |
|||
$BC :=\neg e_{2} \lor \neg e_{3} \lor e_{0} \lor \neg e_{1} \lor \neg e_{5}$\\ |
|||
@ -0,0 +1,26 @@ |
|||
\hspace{-0.09cm}\scalebox{0.85}{ |
|||
\begin{dplltabular}{6} |
|||
\dpllStep{7|8|9|10|11|12} |
|||
\dpllDecL{0|1|1|1|1|1} |
|||
\dpllAssi{ - |$\lnot e_{0}$|$\lnot e_{0}, e_{1}$|$\lnot e_{0}, e_{1}, e_{5}$|\makecell{$\lnot e_{0}, e_{1}, e_{5}, $ \\ $\lnot e_{4}$}|\makecell{$\lnot e_{0}, e_{1}, e_{5}, $ \\ $\lnot e_{4}, \lnot e_{2}$}} |
|||
\dpllClause{1}{$\lnot e_{0}, \lnot e_{1}$}{$\lnot e_{0}, \lnot e_{1}$|\done|\done|\done|\done|\done} |
|||
\dpllClause{2}{$e_{0}, e_{1}$}{$e_{0}, e_{1}$|$e_{1}$|\done|\done|\done|\done} |
|||
\dpllClause{3}{$e_{2}, e_{3}, \lnot e_{4}$}{$e_{2}, e_{3}, \lnot e_{4}$|$e_{2}, e_{3}, \lnot e_{4}$|$e_{2}, e_{3}, \lnot e_{4}$|$e_{2}, e_{3}, \lnot e_{4}$|\done|\done} |
|||
\dpllClause{4}{$e_{1}, \lnot e_{5}$}{$e_{1}, \lnot e_{5}$|$e_{1}, \lnot e_{5}$|\done|\done|\done|\done} |
|||
\dpllClause{5}{$e_{3}, e_{5}, e_{4}$}{$e_{3}, e_{5}, e_{4}$|$e_{3}, e_{5}, e_{4}$|$e_{3}, e_{5}, e_{4}$|\done|\done|\done} |
|||
\dpllClause{6}{$e_{0}, e_{5}$}{$e_{0}, e_{5}$|$e_{5}$|$e_{5}$|\done|\done|\done} |
|||
\dpllClause{7}{$\lnot e_{2}, \lnot e_{3}, e_{0}, \lnot e_{1}, \lnot e_{5}$}{\makecell{$\lnot e_{2}, \lnot e_{3}, e_{0}, $ \\ $\lnot e_{1}, \lnot e_{5}$}|\makecell{$\lnot e_{2}, \lnot e_{3}, \lnot e_{1}, $ \\ $\lnot e_{5}$}|$\lnot e_{2}, \lnot e_{3}, \lnot e_{5}$|$\lnot e_{2}, \lnot e_{3}$|$\lnot e_{2}, \lnot e_{3}$|\done} |
|||
\dpllBCP{ - |$e_{1}$|$e_{5}$| - | - | - } |
|||
\dpllPL{ - | - | - |$\lnot e_{4}$|$\lnot e_{2}$| - } |
|||
\dpllDeci{$\lnot e_{0}$| - | - | - | - |SAT} |
|||
\end{dplltabular} |
|||
} |
|||
|
|||
$\Model_{\EUF} := (y \neq f(x)) \land (y = f(y)) \land (f(x) \neq z) \land (f(y) \neq z) \land (z = x) $ \\ |
|||
Check if the assignment is consistent with the theory: |
|||
|
|||
\begin{align*} |
|||
&\{y, f(y)\}, \{z, x\}, \{f(x)\} |
|||
\end{align*} |
|||
|
|||
$\Model_{\EUF}$ is consistent with the theory, \\$\Rightarrow \Model_{\EUF}$ is a satisfying assignment and $\varphi$ is SAT. |
|||
Write
Preview
Loading…
Cancel
Save
Reference in new issue