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?

$\endgroup$
4
  • $\begingroup$ If you don't care about efficiency, then simple algorithms like brute force enumeration also fit the bill. $\endgroup$ Commented 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$ Commented Nov 6, 2014 at 17:22
  • $\begingroup$ @GiovanniBotta: Can you post the link? I googled it, but didn't find. $\endgroup$
    – user
    Commented Nov 6, 2014 at 19:15
  • $\begingroup$ I was thinking about his book, The Algorithm Design Manual but he also has a website. $\endgroup$ Commented Nov 6, 2014 at 19:24

1 Answer 1

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.

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

Your Answer

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

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