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 Answer 1

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

$\endgroup$
2
  • 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$
    – Ethan
    Commented Nov 20, 2019 at 3:38
  • 1
    $\begingroup$ @Manx Yes, that's exactly right! :) $\endgroup$
    – Bram28
    Commented Nov 20, 2019 at 3:41

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .