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$ – Klaus Draeger Nov 6 '14 at 15:10
  • $\begingroup$ Take a look at Skiena's discussion of this. He describes a few options if I recall correctly. $\endgroup$ – Giovanni Botta Nov 6 '14 at 17:22
  • $\begingroup$ @GiovanniBotta: Can you post the link? I googled it, but didn't find. $\endgroup$ – user Nov 6 '14 at 19:15
  • $\begingroup$ I was thinking about his book, The Algorithm Design Manual but he also has a website. $\endgroup$ – Giovanni Botta Nov 6 '14 at 19:24

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$ – Yuval Filmus Nov 6 '14 at 15:37

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.