Learning material on SAT (Boolean Satisfiability Problem) [closed]

Closed. This question does not meet Stack Overflow guidelines. It is not currently accepting answers.

---

We don’t allow questions seeking recommendations for books, tools开发者_如何学Go, software libraries, and more. You can edit the question so it can be answered with facts and citations.

Closed 7 years ago.

Improve this question

What are good documents to read on SAT (Boolean satisfiability problem) solvers. I have not been able to find good material via Google. The documents I found were either birds eye view, too advanced or corrupted PDF files...

Which papers/documents do you recommend to learn about the algorithms in modern practical SAT solvers?

---

The Davis-Putnam-Logemann-Loveland page on Wikipedia has a good overview.

Then you should be able to follow the minisat paper "An Extensible SAT-solver".

You should also read "GRASP - A New Search Algorithm for Satisfiability" to understand the conflict-driven learning algorithm used in minisat.

I was able to write a SAT solver in Python quite easily using those resources. My sat.py code is available (LGPL 2.1 currently), but it's quite recent so may still contain bugs. It lacks a few optimisations from the minisat design; if you want raw speed use the minisat code ;-)

Update: I've also made an OCaml version, sat.ml, which might make it easier to see the types.

---

A good Book is: Uwe Schöning; Jacobo Torán - The Satisfiability Problem