# If a statement implies a SAT statement, then itself is SAT $?$

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

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)$$
• 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 – Manx Nov 20 '19 at 3:38