4

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?

Jules
  • 6,318
  • 2
  • 29
  • 40
  • 1
    Could you elaborate on what you mean by "solving SAT questions"? SAT questions are specifically designed so that the test taker needs to have creative problem solving skills. A computer does not have this. – Cory Walker Mar 27 '10 at 19:25
  • 1
    Cory, he means satisfaction problems in Boolean logic (see http://en.wikipedia.org/wiki/Boolean_satisfiability_problem), not questions on the SAT (one set of college entrance exams widely used in the US). – Doug McClean Mar 27 '10 at 19:27
  • Yes, sorry, Doug McClean is right: my question is about boolean satisfiability solvers. – Jules Mar 27 '10 at 19:40
  • Check out the documentation on minisat, they have a paper detailing their approach. Very readable and thorough. – Elliot Gorokhovsky Dec 20 '14 at 20:04
  • I've just recently written an article on SAT: [Boolean Satisfiability Problem in 5 mins](http://0a.io/boolean-satisfiability-problem-or-sat-in-5-minutes/) Perhaps anyone who is new to it may find it useful. (it covers the classical DPLL algorithm and improvements that can be made on it [e.g. VSIDS introduced in chaff]) – Archy Will He 何魏奇 Aug 08 '15 at 15:45

2 Answers2

8

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.

Thomas Leonard
  • 7,068
  • 2
  • 36
  • 40
  • Thanks. No PDF reader would open the files on the minisat website, so I gave up on these. But since you suggested them I assume that you *can* open them. And indeed when I open them with Google's online pdf viewer they *do* work! Thanks. Is your Python SAT solver's code available? – Jules Mar 29 '10 at 17:48
  • Good idea - I've added a link to my code. The PDFs opened fine for me (in Evince: http://projects.gnome.org/evince/). – Thomas Leonard Mar 29 '10 at 18:57
0

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

noctua
  • 115
  • 10