3
$\begingroup$

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

$\endgroup$
  • 1
    $\begingroup$ 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. $\endgroup$ – Juho Jan 28 '13 at 2:04
4
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ 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. $\endgroup$ – vzn Jan 28 '13 at 3:32
  • $\begingroup$ well, google for completeness proofs of resolution - you'll find many more examples. $\endgroup$ – Yuval Filmus Jan 28 '13 at 6:08

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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