1
$\begingroup$


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 $?$

$\endgroup$
1
$\begingroup$

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)$

| cite | improve this answer | |
$\endgroup$
  • 1
    $\begingroup$ I see $\dots$ In the end it become: $$(a ∨ b ∨ c) ∧ (b ∨ ¬c ∨ ¬f) ∧ (¬b ∨ e)$$$$\equiv(a ∨ b ∨ c) ∧ (b ∨ ¬c ∨ ¬f) ∧ (¬b ∨ e) ∧ (a ∨ c ∨ e) ∧ (¬c ∨ e ∨ ¬f) ∧ (a ∨ e ∨ ¬f)$$ which is SAT, make sense, thanks $\endgroup$ – Manx Nov 20 '19 at 3:38
  • 1
    $\begingroup$ @Manx Yes, that's exactly right! :) $\endgroup$ – Bram28 Nov 20 '19 at 3:41

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.