# Proving unsatisfiability with propositional resolution

I'm having trouble understanding how to use the resolution rule to prove if a statement is satisfiable or unsatisfiable.

I watched this course lecture on propositional resolution and unsatisfiability (linked with a time stamp to skip to the part in question):
"5.4 - Resolution Method - Propositional Resolution - [Introduction To Logic] By Michael Genesereth" https://www.youtube.com/watch?v=IpixwNupBIs#t=2m21s

For those that don't want to watch the video, my understanding is that he is saying that for a statement in conjunctive normal form (CNF) we can test whether the statement is satisfiable by repeatedly applying the simplifying resolution rule:
If there is a pair of clauses of the form $$(a \vee X)$$ $$(\neg a \vee Y)$$ this can be replaced by a single clause $$(X \vee Y)$$

The claim is that a statement is unsatisfiable if and only if repeated application of this rule leads to an empty clause.

But this doesn't make sense to me. I think there are some important details that are left out. For instance in the example given in the video, consider the statement with the clauses

1. $(p \vee q)$
2. $(p \vee \neg q)$
3. $(\neg p \vee q)$
4. $(\neg p \vee \neg q)$

By inspection, this is unsatisfiable. But let's find this using the resolution rule, following along with the video...

Applying the resolution rule on pair 1,2 gives: $p$

Then applying the resolution rule on pair 3,4 gives $\neg p$

So now we just have the clauses $p, \neg p$, which after applying the resolution rule one more time gives the empty clause.

That is how the example goes in the video. But look what happens if we apply the rule in another order:

Applying the resolution rule on pair 1,4 gives: $q \vee \neg q$

Then applying the resolution rule on pair 2,3 gives $\neg q \vee q$

So now we are just left with two clauses which are tautologies. So we simplified the statement to just $\top$. So by this order, it claims the statement is satisfiable.

Clearly something is wrong. What am I misunderstanding? Or is the course lecture leaving out something crucial?

• Whoever downvoted my question, can you at least give me a hint of what I should do better? Is this question considered too basic? Is it not clear what I'm asking? – SweetPickles Aug 17 '15 at 6:50
• See Resolution : The resolution rule is applied to all possible pairs of clauses that contain complementary literals. After each application of the resolution rule, the resulting sentence is simplified by removing repeated literals. If the sentence contains complementary literals, it is discarded (as a tautology). If not, and if it is not yet present in the clause set S, it is added to S, and is considered for further resolution inferences. – Mauro ALLEGRANZA Aug 17 '15 at 14:46

You can see :

for a complete treatment of the proof system based on the Resolution Rule.

The proof system "expands" the set of cluases, applying the Resoultion Rule in order to add e new clause (a disjunction) to the original set of clauses. The rule has the property that "preserves stisfiability", i.e. the new set of clauses is satisfiable iff the original one is.

Thus, if after iterated applications of the rule the empty clause is produced, being it unsatisfiable (it is another way of writing $\bot$, i.e. a contradiction) this is enough to conclude that also the original set of clauses is unsatisfiable.

• Oh, okay. Maybe because how people draw it when working it out, I thought the original rules could be removed. – SweetPickles Aug 18 '15 at 2:47
• However, there appear to be cases where it IS okay to discard the original clauses after using the resolution rule. For instance here: en.wikipedia.org/wiki/Conflict-Driven_Clause_Learning#/media/… en.wikipedia.org/wiki/Davis%E2%80%93Putnam_algorithm How can one know if it is okay to discard the clauses? The book doesn't seem to talk about that. – SweetPickles Aug 18 '15 at 2:49
• @SweetPickles - if you "run" the proof procedure "by hand", you work with insight; this means that you apply a strategy directed to the goal of "producing" the empty clause. But the proof procedure is designed to be "mechanized": this means that you have to produce all possible combinations of disjuncts that "matchs" according to the Resolution rule and you have not to discard anything, otherwise (as in your case) you are in danger to miss the result. – Mauro ALLEGRANZA Aug 18 '15 at 11:39

I think this algorithm should help you . You need to add the resolved clause to your set of clauses everytime you resolve and so your set of clauses grow. Also before adding, you need to make sure that when you resolve you do not end up generating the clause which you might have already generated before in the process of resolution or( which already exists in your set of clauses). Look the algorithm pictures

Unsatisfiability algo pic

Saturation Algo pic
{"extraction_info": {"found_math": true, "script_math_tex": 0, "script_math_asciimath": 0, "math_annotations": 0, "math_alttext": 0, "mathml": 0, "mathjax_tag": 0, "mathjax_inline_tex": 1, "mathjax_display_tex": 1, "mathjax_asciimath": 0, "img_math": 0, "codecogs_latex": 0, "wp_latex": 0, "mimetex.cgi": 0, "/images/math/codecogs": 0, "mathtex.cgi": 0, "katex": 0, "math-container": 0, "wp-katex-eq": 0, "align": 0, "equation": 0, "x-ck12": 0, "texerror": 0, "math_score": 0.7229149341583252, "perplexity": 462.0232707702813}, "config": {"markdown_headings": true, "markdown_code": true, "boilerplate_config": {"ratio_threshold": 0.18, "absolute_threshold": 10, "end_threshold": 15, "enable": true}, "remove_buttons": true, "remove_image_figures": true, "remove_link_clusters": true, "table_config": {"min_rows": 2, "min_cols": 3, "format": "plain"}, "remove_chinese": true, "remove_edit_buttons": true, "extract_latex": true}, "warc_path": "s3://commoncrawl/crawl-data/CC-MAIN-2019-26/segments/1560627999263.6/warc/CC-MAIN-20190620165805-20190620191805-00061.warc.gz"}