|
|
We start by computing $\skel$: \begin{compactItemize} \item $e_{0}\Leftrightarrow(g(a)=c)$ \item $e_{1}\Leftrightarrow(f(g(a))=f(c))$ \item $e_{2}\Leftrightarrow(g(a)=d)$ \item $e_{3}\Leftrightarrow(c=d)$ \end{compactItemize} $$ \skel = e_{0} \land \neg e_{1} \land e_{2} \land \neg e_{3} $$
\hspace{-0.09cm}\scalebox{0.85}{ \begin{dplltabular}{4} \dpllStep{1|2|3|4} \dpllDecL{0|0|0|0} \dpllAssi{ - |$e_{0}$|$e_{0}, \lnot e_{3}$|$e_{0}, \lnot e_{3}, \lnot e_{1}$} \dpllClause{1}{$e_{0}$}{$e_{0}$|\done|\done|\done} \dpllClause{2}{$\lnot e_{1}, e_{2}$}{$\lnot e_{1}, e_{2}$|$\lnot e_{1}, e_{2}$|$\lnot e_{1}, e_{2}$|\done} \dpllClause{3}{$\lnot e_{3}$}{$\lnot e_{3}$|$\lnot e_{3}$|\done|\done} \dpllBCP{$e_{0}$|$\lnot e_{3}$| - | - } \dpllPL{ - | - |$\lnot e_{1}$| - } \dpllDeci{ - | - | - | - } \end{dplltabular} }
A satisfying assignment $e_0 \land \neg e_1 \land \neg e_3$ has been found and we have to check consistency of $(g(a) = c) \land (f(g(a)) \neq f(c)) \land (c \neq d) $:
\begin{align*} &\{g(a), c\}, \{f(g(a))\}, \{f(c)\}, \{d\}\\ &\{g(a), c\}, \{d\}, \{f(c), f(g(a))\} \end{align*}
Congruence Closure returns UNSAT because of: $(f(g(a)) \neq f(c)) $. We therefore add $\neg e_0 \lor e_1 \lor e_3$ as a blocking clause and continue. \hspace{-0.09cm}\scalebox{0.85}{ \begin{dplltabular}{5} \dpllStep{5|6|7|8|9} \dpllDecL{0|0|0|0|0} \dpllAssi{ - |$e_{0}$|$e_{0}, \lnot e_{3}$|$e_{0}, \lnot e_{3}, e_{1}$|\makecell{$e_{0}, \lnot e_{3}, e_{1}, $ \\ $e_{2}$}} \dpllClause{1}{$e_{0}$}{$e_{0}$|\done|\done|\done|\done} \dpllClause{2}{$\lnot e_{1}, e_{2}$}{$\lnot e_{1}, e_{2}$|$\lnot e_{1}, e_{2}$|$\lnot e_{1}, e_{2}$|$e_{2}$|\done} \dpllClause{3}{$\lnot e_{3}$}{$\lnot e_{3}$|$\lnot e_{3}$|\done|\done|\done} \dpllClause{4}{$\lnot e_{0}, e_{3}, e_{1}$}{$\lnot e_{0}, e_{3}, e_{1}$|$e_{3}, e_{1}$|$e_{1}$|\done|\done} \dpllBCP{$e_{0}$|$\lnot e_{3}$|$e_{1}$|$e_{2}$| - } \dpllPL{ - | - | - | - | - } \dpllDeci{ - | - | - | - | - } \end{dplltabular} }
We have to check consistency for $(g(a) = c) \land (f(g(a)) = f(c)) \land (g(a) = d) \land (c \neq d) $:
\begin{align*} &\{g(a), c\}, \{f(g(a)), f(c)\}, \{g(a), d\}\\ &\{f(g(a)), f(c)\}, \{c, d, g(a)\} \end{align*}
Congruence Closure returns UNSAT because of: $(c \neq d) $\\ We therefore add $\neg e_0 \lor e_3 \lor \neg e_1 \lor \neg e_2$ as a blocking clause and continue. \hspace{-0.09cm}\scalebox{0.80}{ \begin{dplltabular}{5} \dpllStep{10|11|12|13|14} \dpllDecL{0|0|0|0|0} \dpllAssi{ - |$e_{0}$|$e_{0}, \lnot e_{3}$|$e_{0}, \lnot e_{3}, e_{1}$|\makecell{$e_{0}, \lnot e_{3}, e_{1}, $ \\ $\lnot e_{2}$}} \dpllClause{1}{$e_{0}$}{$e_{0}$|\done|\done|\done|\done} \dpllClause{2}{$\lnot e_{1}, e_{2}$}{$\lnot e_{1}, e_{2}$|$\lnot e_{1}, e_{2}$|$\lnot e_{1}, e_{2}$|$e_{2}$|\conflict} \dpllClause{3}{$\lnot e_{3}$}{$\lnot e_{3}$|$\lnot e_{3}$|\done|\done|\done} \dpllClause{4}{$\lnot e_{0}, e_{3}, e_{1}$}{$\lnot e_{0}, e_{3}, e_{1}$|$e_{3}, e_{1}$|$e_{1}$|\done|\done} \dpllClause{5}{$\lnot e_{0}, e_{3}, \lnot e_{1}, \lnot e_{2}$}{\makecell{$\lnot e_{0}, e_{3}, \lnot e_{1}, $ \\ $\lnot e_{2}$}|$e_{3}, \lnot e_{1}, \lnot e_{2}$|$\lnot e_{1}, \lnot e_{2}$|$\lnot e_{2}$|\done} \dpllBCP{$e_{0}$|$\lnot e_{3}$|$e_{1}$|$\lnot e_{2}$| - } \dpllPL{ - | - | - | - | - } \dpllDeci{ - | - | - | - |UNSAT} \end{dplltabular} }
Conflict in step 14\\ \scalebox{0.75}{
\begin{tikzpicture}[>=latex,line join=bevel,] \pgfsetlinewidth{1bp} %%
\pgfsetcolor{black} % Edge: 0 -> 2
\draw [->] (1.0882bp,62.277bp) .. controls (1.964bp,62.779bp) and (9.2748bp,62.662bp) .. (19.0bp,62.429bp) .. controls (30.239bp,62.537bp) and (43.981bp,61.976bp) .. (65.01bp,63.663bp); \definecolor{strokecol}{rgb}{0.0,0.0,0.0}; \pgfsetstrokecolor{strokecol} \draw (33.0bp,70.929bp) node {$$1$$}; % Edge: 0 -> 4
\draw [->] (1.0536bp,100.444bp) .. controls (2.5288bp,100.842bp) and (34.108bp,100.377bp) .. (65.302bp,102.81bp); \draw (33.0bp,107.93bp) node {$$3$$}; % Edge: 2 -> 5
\draw [->] (84.139bp,57.437bp) .. controls (89.42bp,51.96bp) and (97.049bp,44.903bp) .. (105.0bp,40.429bp) .. controls (117.15bp,33.594bp) and (132.19bp,29.057bp) .. (153.87bp,24.136bp); \draw (119.0bp,47.929bp) node {$$4$$}; % Edge: 2 -> 6
\draw [->] (87.223bp,65.255bp) .. controls (115.41bp,64.774bp) and (194.66bp,63.424bp) .. (242.75bp,62.604bp); \draw (165.0bp,70.929bp) node {$$5$$}; % Edge: 3 -> 1
\draw [->] (264.67bp,18.652bp) .. controls (272.24bp,21.175bp) and (283.02bp,24.768bp) .. (302.09bp,31.126bp); % Edge: 4 -> 5
\draw [->] (85.379bp,99.325bp) .. controls (96.698bp,90.91bp) and (117.27bp,75.011bp) .. (133.0bp,59.429bp) .. controls (139.39bp,53.105bp) and (145.86bp,45.585bp) .. (157.76bp,30.745bp); \draw (119.0bp,89.929bp) node {$$4$$}; % Edge: 4 -> 6
\draw [->] (87.393bp,105.29bp) .. controls (98.691bp,105.0bp) and (117.24bp,104.11bp) .. (133.0bp,101.43bp) .. controls (174.77bp,94.331bp) and (185.41bp,91.533bp) .. (225.0bp,76.429bp) .. controls (228.25bp,75.189bp) and (231.62bp,73.694bp) .. (243.87bp,67.569bp); \draw (165.0bp,104.93bp) node {$$5$$}; % Edge: 5 -> 3
\draw [->] (173.78bp,15.592bp) .. controls (179.69bp,10.872bp) and (188.28bp,4.9991bp) .. (197.0bp,2.4291bp) .. controls (208.94bp,-1.0874bp) and (212.85bp,-0.25425bp) .. (225.0bp,2.4291bp) .. controls (228.24bp,3.1456bp) and (231.56bp,4.2776bp) .. (244.02bp,10.039bp); \draw (211.0bp,9.9291bp) node {$$2$$}; % Edge: 5 -> 6
\draw [->] (176.04bp,24.306bp) .. controls (188.14bp,26.832bp) and (208.86bp,32.005bp) .. (225.0bp,40.429bp) .. controls (229.31bp,42.678bp) and (233.61bp,45.621bp) .. (245.22bp,55.023bp); \draw (211.0bp,47.929bp) node {$$5$$}; % Edge: 6 -> 1
\draw [->] (264.16bp,57.93bp) .. controls (272.09bp,54.035bp) and (283.8bp,48.281bp) .. (302.68bp,39.01bp); % Node: 2
\begin{scope} \definecolor{strokecol}{rgb}{0.0,0.0,0.0}; \pgfsetstrokecolor{strokecol} \draw (76.0bp,65.43bp) ellipse (11.0bp and 11.0bp); \draw (76.0bp,65.429bp) node {$e_{0}$}; \end{scope} % Node: 4
\begin{scope} \definecolor{strokecol}{rgb}{0.0,0.0,0.0}; \pgfsetstrokecolor{strokecol} \draw (76.0bp,105.43bp) ellipse (11.0bp and 11.0bp); \draw (76.0bp,105.43bp) node {$\lnot e_{3}$}; \end{scope} % Node: 1
\begin{scope} \definecolor{strokecol}{rgb}{0.0,0.0,0.0}; \pgfsetstrokecolor{strokecol} \draw (313.0bp,34.43bp) ellipse (11.0bp and 11.0bp); \draw (313.0bp,34.429bp) node {$\bot$}; \end{scope} % Node: 5
\begin{scope} \definecolor{strokecol}{rgb}{0.0,0.0,0.0}; \pgfsetstrokecolor{strokecol} \draw (165.0bp,22.43bp) ellipse (11.0bp and 11.0bp); \draw (165.0bp,22.429bp) node {$e_{1}$}; \end{scope} % Node: 6
\begin{scope} \definecolor{strokecol}{rgb}{0.0,0.0,0.0}; \pgfsetstrokecolor{strokecol} \draw (254.0bp,62.43bp) ellipse (11.0bp and 11.0bp); \draw (254.0bp,62.429bp) node {$\lnot e_{2}$}; \end{scope} % Node: 3
\begin{scope} \definecolor{strokecol}{rgb}{0.0,0.0,0.0}; \pgfsetstrokecolor{strokecol} \draw (254.0bp,15.43bp) ellipse (11.0bp and 11.0bp); \draw (254.0bp,15.429bp) node {$e_{2}$}; \end{scope} %
\end{tikzpicture}
} \begin{prooftree} \AxiomC{$2. \; \lnot e_{1} \lor e_{2}$} \AxiomC{$5. \; \lnot e_{0} \lor e_{3} \lor \lnot e_{1} \lor \lnot e_{2}$} \BinaryInfC{$\lnot e_{1} \lor \lnot e_{0} \lor e_{3}$} \AxiomC{$4. \; \lnot e_{0} \lor e_{3} \lor e_{1}$} \BinaryInfC{$\lnot e_{0} \lor e_{3}$} \AxiomC{$1. \; e_{0}$} \BinaryInfC{$e_{3}$} \AxiomC{$3. \; \lnot e_{3}$} \BinaryInfC{$\bot$} \end{prooftree}
Since the SAT solver cannot find a satisfying assignment we are done and conclude that $\varphi$ is UNSAT.
|
