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.
 
 

33 lines
1.2 KiB

\item \self Consider the following conflict graph with the following set of clauses:
\begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,node distance=1.5cm,
thick,base node/.style={circle,draw,minimum size=20pt}, real node/.style={double,circle,draw,minimum size=20pt}]
\node[base node] (1) {$\lnot a$};
\node[base node] (2) [right of=1]{$\lnot b$};
\node[base node] (4) [right of=2] {$\lnot c$};
\node[base node] (5) [right of=4] {$\lnot e$};
\node[base node] (6) [above right of=5] {$d$};
\node[base node] (3) [below right of=5] {$\lnot d$};
\node[base node] (7) [below right of=6] {$\bot$};
\path[]
(1) edge [] node {$3$} (2)
edge [bend right] node {$4$} (3)
(2) edge [] node {$5$} (4)
edge [bend left=35] node {$1$} (6)
(4) edge [] node {$2$} (5)
edge [bend left=20] node {$1$} (6)
(5) edge [] node {$4$} (3)
(3) edge [] node {} (7)
(6) edge [] node {} (7);
\end{tikzpicture}
\begin{dpllCNFInput}
\item $\{b, c, d\}$
\item $\{c, \lnot e\}$
\item $\{a, \lnot b\}$
\item $\{a, \lnot d, e\}$
\item $\{b, \lnot c\}$
\end{dpllCNFInput}
State the learned clause by making a resolution proof according to the given conflict graph and given clauses.