0

I am refering to this document.

The relevant part is: enter image description here

My question:

I understand that (a or b) and (not(a) or c) implies b or c but what really confuses me is the statement

"The produced resolvents $S{'} = S_x \circ S_{\overline{x}}$ replace the original clauses $S$ containing $x$ or $\overline{x}$, resulting in a satisfiability equivalent problem"

Given my example $S{'}=\{\{b,c\}\}$ would be satisfiable by $(a,b,c)=(1,1,0)$ but $S=\{\{a,b\}, \{\overline{a},c\}\}$ clearly is not.

What what am I misunderstanding here?

p.s. Prefer ELI5 answer <)

mangolassi
  • 221

1 Answers1

1

Both $S{'}=\{\{b,c\}\}$ and $S=\{\{a,b\}, \{\overline{a},c\}\}$ are satisfiable. That's all that matters.

The fact that $S{'}=\{\{b,c\}\}$ is satisfiable by some specific truth-assignment that does not satisfy $S=\{\{a,b\}, \{\overline{a},c\}\}$ does not change that: $S=\{\{a,b\}, \{\overline{a},c\}\}$ is still satisfiable, just by a different truth-assignment, e.g. $a=b=c=1$ will do nicely

Bram28
  • 100,612
  • 6
  • 70
  • 118
  • Ok, that sounds like the root cause of my confusion. But then I don't understand what the point of this is, but whatever <3 – mangolassi Feb 15 '24 at 20:19
  • @mangolassi By going through this process you are eliminating variables one by one. So at some point you reach an end point, and thus an answer. – Bram28 Feb 15 '24 at 20:58