Computer Science Stack Exchange is a question and answer site for students, researchers and practitioners of computer science. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

SAT [5] can be solved with resolution definitively, i.e. if the formula has a true assignment, resolution can find it, and if it cant be satisfied, resolution can show that no assignment exists (at least in exponential time/space.). [4]

Is there a good fully-self contained description somewhere of solving SAT with resolution?

The descriptions on Wikipedia of resolution are focused on a single logical operation, not how to use it in an algorithm to solve SAT, and the Davis Putnam algorithm is described mostly in terms of 1st order logic. I am looking for a description of solving SAT with resolution that does not refer to 1st order logic, just in terms of boolean input variables. Online description is preferred if possible. The connection with DPLL would be helpful also.

[1] Davis Putnam algorithm, Wikipedia

[2] Resolution in logic, Wikipedia

[3] Davis Putnam Logemann Loveland algorithm, Wikipedia

[4] Is resolution complete or only refutation-complete?

[5] The boolean satisfiability problem

share|cite|improve this question
You could have a look at the presentations by Joao Marques-Silva. One of his talks here at least has both an explanation and an example of resolution. Also, IIRC the Russell & Norvig AI book has a self-contained description too. – Juho Jan 28 '13 at 2:04
up vote 4 down vote accepted

What you are looking for is a proof of the completeness of resolution. Here is one example. The relation to DPLL is that a run of DPLL which terminates in failure can be converted to a resolution proof that the formula is unsatisfiable.

share|cite|improve this answer
nice/sufficient & has lots of examples but unfortunately all the examples only have 2 variables ie chosen from 2SAT only... esp interested in 3SAT at least & where clauses have multiple common variables. – vzn Jan 28 '13 at 3:32
well, google for completeness proofs of resolution - you'll find many more examples. – Yuval Filmus Jan 28 '13 at 6:08

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.