Two runs of the Davis-Putnam procedure on example propositional ground instances.
Top to bottom, Left: Starting from the formula ${\displaystyle (a\lor b\lor c)\land (b\lor \lnot c\lor \lnot f)\land (\lnot b\lor e)}$, the algorithm resolves on ${\displaystyle b}$, and then on ${\displaystyle c}$. Since no further resolution is possible, the algorithm stops; since the empty clause couldn't be derived, the result is "satisfiable". Right: Resolving the given formula on ${\displaystyle b}$, then on ${\displaystyle a}$, then on ${\displaystyle c}$ yields the empty clause; hence the algorithm returns "unsatisfiable".
I'm reading the wiki page of Davis–Putnam algorithm, and have some qeustions:
Second proof of UNSAT is fine, since each level are equivalent.
For the picture on the left, have statement $(a+b+c)(b+c'+f')(b'+e)$,
I think it's saying:
$$\left\{\begin{array}{l}(a+\color{red}{b}+c)(\color{red}{b'}+e)\\(\color{blue}{b}+c'+f')(\color{blue}{b'}+e)\end{array}\right.\Rightarrow
\left\{\begin{array}{l}(a+\color{orange}{c}+e)\\(\color{orange}{c'}+e+f')\end{array}\right.
\Rightarrow(a+e+f')\text{(which is SAT)}$$
From $(a+e+f')$ is SAT, $\underset{?}{\underline{\text{we can conclude original statement is SAT}}}$.
My question is which theorem was used here, since $(a+b+c)(b+c'+f')(b'+e)$ implies $(a+e+f')$ but not equivalent, why this implies original statement is SAT $?$
Best Answer
It is not because $a+e+f'$ is satisfable that the original statement is satisfiable, but rather because there is nothing further to be resolved.
Indeed, note that when you get a new statement through resolution, then that statement does not replace the original statements, but rather it gets added to them. For example, you really go from $(a+b+c)(b+c'+f')(b'+e)$ to $(a+b+c)(b+c'+f')(b'+e)(a+c+e)$ when doing the first resolution. Indeed, these two statements are equivalent because of the basic equivalence of:
$(a+b)(a'+c)\Leftrightarrow (a+b)(a'+c)(b+c)$