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.
11 lines
747 B
11 lines
747 B
\item Use the DPLL algorithm with BCP, PL and CDCL to determine whether or not the set of clauses given is satisfiable. Decide variables in alphabetical order starting with the \textit{negative} phase. For conflicts, draw conflict graphs after the end of the table, and add the learned clause to the table.\\
|
|
If the set of clauses resulted in \texttt{SAT}, give a satisfying model. If the set of clauses resulted in \texttt{UNSAT}, give a resolution proof that shows that the conjunction of the clauses from the table is unsatisfiable.
|
|
|
|
\begin{dpllCNFInput}
|
|
\item (x \lor y \lor w)
|
|
\item (\lnot x \lor z \lor \lnot w)
|
|
\item (\lnot y \lor w)
|
|
\item (\lnot z \lor \lnot w)
|
|
\item (\lnot y \lor z)
|
|
\item (\lnot x \lor w)
|
|
\end{dpllCNFInput}
|