I am refering to this document.
The relevant part is:
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 <)
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