[Solved]: Description of resolution algorithm as it applies to SAT

ignougroup
Problem Detail: 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

Asked By : vzn

Answered By : Yuval Filmus

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.
Best Answer from StackOverflow

Question Source : http://cs.stackexchange.com/questions/9233