To my best knowledge, these are the sound and complete algorithms for boolean satisfiability

  • Variations of DPLL algorithm (e.g. CDCL, Look-ahead solvers)
  • Stalmarks method
  • Binary Decision Diagram (BDD)

I am looking for other sound and complete algorithms for boolean satisfiability?

  • $\begingroup$ If you don't care about efficiency, then simple algorithms like brute force enumeration also fit the bill. $\endgroup$ Nov 6, 2014 at 15:10
  • $\begingroup$ Take a look at Skiena's discussion of this. He describes a few options if I recall correctly. $\endgroup$ Nov 6, 2014 at 17:22
  • $\begingroup$ @GiovanniBotta: Can you post the link? I googled it, but didn't find. $\endgroup$
    – user
    Nov 6, 2014 at 19:15
  • $\begingroup$ I was thinking about his book, The Algorithm Design Manual but he also has a website. $\endgroup$ Nov 6, 2014 at 19:24

1 Answer 1


Resolution is sound and complete. In recursive learning, you recursively evaluate the clause satisfiability requirements for identifying common assignments. Look at say page 29 and onwards in these slides.

  • 2
    $\begingroup$ Resolution is the non-deterministic version of DPLL. $\endgroup$ Nov 6, 2014 at 15:37

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

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