You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
171 lines
7.8 KiB
171 lines
7.8 KiB
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.
|