2
$\begingroup$

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?

Improve this question
$\endgroup$
4
  • $\begingroup$ If you don't care about efficiency, then simple algorithms like brute force enumeration also fit the bill. $\endgroup$
    – Klaus Draeger
    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$
    – Giovanni Botta
    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$
    – Giovanni Botta
    Nov 6, 2014 at 19:24

1 Answer 1

Reset to default
2
$\begingroup$

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.

Improve this answer
$\endgroup$
1
  • 2
    $\begingroup$ Resolution is the non-deterministic version of DPLL. $\endgroup$
    – Yuval Filmus
    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.