<p>An excellent beginner overview is given by the following article from 2009.</p>

<ul>
<li><a href="http://cacm.acm.org/magazines/2009/8/34498-boolean-satisfiability-from-theoretical-hardness-to-practical-success/fulltext">Boolean Satisfiability: From Theoretical Hardness to Practical Success</a>, Sharad Malik, Lintao Zhang,  Communications of the ACM, 2009</li>
</ul>

<p>There are several ways to get into the technical aspects. You can even start with the original Davis-Putnam paper. It is extremely clear and has detailed examples. When discussing SAT optimizations in a course, we discovered that a few one  may imagine are already there. The Davis-Logeman-Loveland paper is (I feel) less instructive, but it is so short you may as well read it. </p>

<ul>
<li><a href="http://dl.acm.org/citation.cfm?id=321034">A Computing Procedure for Quantification Theory</a>, Martin Davis, Hilary Putnam, Journal of the ACM, 1960.</li>
<li><a href="http://portal.acm.org/citation.cfm?id=368557">A machine program for theorem-proving</a>, Martin Davis, George Logemann, Donald Loveland, Communications of the ACM, 1962.</li>
</ul>

<p>There are may ways to catch up on the developments of the next 50 years. I would recommend lecture slides. Just searching for 'DPLL' will throw up many many tutorials. If you browse through them, I'm sure the mist will clear -- to some extent. There are also many useful surveys. The Zhang-Malik paper is a good place to start. There are several articles in the Handbook of Satisfiability you may find useful. </p>

<ul>
<li><a href="http://www.princeton.edu/~chaff/publication/cade_cav_2002.pdf">The Quest for Efficient Boolean Satisfiability Solvers</a>, Lintao Zhang, Sharad Malik, Joint invited paper for CAV and CADE 2002.</li>
<li><a href="http://www.informatik.uni-trier.de/~ley/db/series/faia/faia185.html">Handbook of Satisfiability</a>, Edited by Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, 2009</li>
<li><a href="http://eatcs.org/beatcs/index.php/beatcs/article/view/138">Anatomy and Empirical Evaluation of Modern SAT Solvers</a>, Karem  Sakallah, Joao Marques-Silva, Bulletin of the EATCS, 2011.</li>
</ul>

<p>I second the suggestion of Mikolaos. The MiniSAT code is clean and of manageable size. You can play with it. There are several other solvers you can try. CryptoMiniSat is also quite clean. You should also consult the work of <a href="http://fmv.jku.at/biere/papers/index.html">Armin Biere</a>, who writes SAT solvers and writes about writing SAT solvers.</p>

CC BY-SA 3.0
2011-08-04T01:51:27.933Z
2013-11-09T16:02:52.683Z
2013-11-09T16:02:52.683Z
Vijay D
<p>I suggest first understanding which techniques really advanced the solvers, for which I would suggest the following <a href="http://dx.doi.org/10.1007/978-3-642-21581-0_27">overview and analysis</a>.</p>

<p>Then I would recommend downloading the source code of <a href="http://minisat.se/MiniSat.html">minisat</a> and read its <a href="http://dx.doi.org/10.1007/978-3-540-24605-3_37">description</a>.</p>

<p>It might of course be individual but I found looking at the source code most valuable.</p>

CC BY-SA 3.0
2011-08-03T21:25:34.097Z
2011-08-03T21:25:34.097Z
Mikolas
<p>If you're overwhelmed by all of the work that's out there, why don't you start out pretending that nobody's worked on the problem before?  If your goal is to eventually build a competitive SAT solver, it's going to be a fairly long journey.  By starting out just playing around without 'checking the solutions', so to speak, you have more to gain than to lose. </p>

<p>First build the simplest solver you can and make sure it works.  This will probably be a brute force algorithm whose running time depends more or less only on the $n$, the number of variables, and $m$, the number of clauses.  Then implement something a little bit smarter like branch-and-bound.  Write (or find) a generator that will give you random instances for given values of $n$ and $m$.</p>

<p>Do some benchmarking tests for your branch-and-bound solver.  See how it does for varying values of $n$ and $m$.  Then improve your solver to make it faster.  See how far you can get without reading about other work.  When you run out of ideas, do some of the reading suggested in the other answers.</p>

CC BY-SA 3.0
2011-08-04T12:34:03.827Z
2011-08-04T12:34:03.827Z
James King
<p>Start with a good survey paper.  It's easy to attack the subject piecemeal and get confused by different names in the literature for the same techniques and the same name used for different techniques.  It's also easy to re-enact old algorithmic battles (occur lists vs. head-tail lists vs. two watched literals for DPLL implementations for instance) if you don't know what the state of the art is.</p>

<p><a href="http://www.cs.cornell.edu/gomes/papers/SATSolvers-KR-Handbook.pdf">Satisfiability Solvers</a> by Gomes, et. al. will give you the rough lay of the land.</p>

<p><a href="http://www.emcl-study.eu/fileadmin/master_theses/thesis_manthey.pdf">Improving SAT Solvers Using State-of-the-Art Techniques</a> by Manthey will bring you closer to the present.</p>

CC BY-SA 3.0
2011-12-28T23:25:50.607Z
2011-12-28T23:25:50.607Z
Kyle Jones
<p>I want to make a first SAT solver. I know the SAT competition and the SAT conference, and there are just so many papers on this subject. I'm a starter, an overwhelmed starter. Where should I begin? Eventually I want to push the state-of-the-art. I want some expert advice on how to start, so that I won't be wasting my time on the non-essentials too early. Many thanks.</p>

CC BY-SA 3.0
2011-08-03T08:10:04.973Z
Have you already implemented the DPLL algorithm? Have you fine-tuned and polished your implementation so that it runs extremely fast?
Jukka Suomela
CC BY-SA 3.0
2011-08-03T14:23:42.730Z
The Handbook of Satisfiability - http://www.amazon.co.uk/Satisfiability-Frontiers-Artificial-Intelligence-Applications/dp/1586039296/ref=sr_1_1?ie=UTF8&qid=1312381353&sr=8-1 (perhaps check a library, the cost is pretty high).
MGwynne
CC BY-SA 3.0
2011-08-03T14:25:26.910Z
One lecture series is 
http://cs.swan.ac.uk/~csoliver/SAT200809/index.html . I'm sure there are many others.
MGwynne
CC BY-SA 3.0
2011-08-03T16:26:08.210Z
@Jukka: comment -> answer ?
Suresh Venkat
CC BY-SA 3.0
2011-08-04T05:14:27.570Z
I disagree with Jukka. Why reinvent the wheel? There's no reason to redo what MiniSAT already provides open source. If you're interested in adding to the CDCL framework your addition will show in boosted MiniSAT performance. Also, DPLL by itself is not enough; a lot of improvements have been made. Basically, follow Mikolas' answer!
Huck Bennett
CC BY-SA 3.0
2011-08-06T16:05:17.720Z
See also related question http://cstheory.stackexchange.com/q/1988
András Salamon
<ds.algorithms><reference-request><lo.logic><sat>
Starting SAT solver papers
Zirui Wang
# Starting SAT solver papers

(Asked by: username_0 on 2011-08-03)

I want to make a first SAT solver. I know the SAT competition and the SAT conference, and there are just so many papers on this subject. I'm a starter, an overwhelmed starter. Where should I begin? Eventually I want to push the state-of-the-art. I want some expert advice on how to start, so that I won't be wasting my time on the non-essentials too early. Many thanks.

**Tags:** ds.algorithms, reference-request, lo.logic, sat
> **Comments:**
> **username_1**: Have you already implemented the DPLL algorithm? Have you fine-tuned and polished your implementation so that it runs extremely fast?  
> **username_2**: The Handbook of Satisfiability - http://www.amazon.co.uk/Satisfiability-Frontiers-Artificial-Intelligence-Applications/dp/1586039296/ref=sr_1_1?ie=UTF8&qid=1312381353&sr=8-1 (perhaps check a library, the cost is pretty high).  
> **username_2**: One lecture series is  http://cs.swan.ac.uk/~csoliver/SAT200809/index.html . I'm sure there are many others.  
> **username_3**: @Jukka: comment -> answer ?  
> **username_4**: I disagree with Jukka. Why reinvent the wheel? There's no reason to redo what MiniSAT already provides open source. If you're interested in adding to the CDCL framework your addition will show in boosted MiniSAT performance. Also, DPLL by itself is not enough; a lot of improvements have been made. Basically, follow Mikolas' answer!  
> **username_5**: See also related question http://cstheory.stackexchange.com/q/1988  

---

## 4 answers

### Answer by username_6 on 2011-08-04. Score: 18

An excellent beginner overview is given by the following article from 2009.

* [Boolean Satisfiability: From Theoretical Hardness to Practical Success](http://cacm.acm.org/magazines/2009/8/34498-boolean-satisfiability-from-theoretical-hardness-to-practical-success/fulltext), Sharad Malik, Lintao Zhang, Communications of the ACM, 2009

There are several ways to get into the technical aspects. You can even start with the original Davis-Putnam paper. It is extremely clear and has detailed examples. When discussing SAT optimizations in a course, we discovered that a few one may imagine are already there. The Davis-Logeman-Loveland paper is (I feel) less instructive, but it is so short you may as well read it.

* [A Computing Procedure for Quantification Theory](http://dl.acm.org/citation.cfm?id=321034), Martin Davis, Hilary Putnam, Journal of the ACM, 1960.
* [A machine program for theorem-proving](http://portal.acm.org/citation.cfm?id=368557), Martin Davis, George Logemann, Donald Loveland, Communications of the ACM, 1962.

There are may ways to catch up on the developments of the next 50 years. I would recommend lecture slides. Just searching for 'DPLL' will throw up many many tutorials. If you browse through them, I'm sure the mist will clear -- to some extent. There are also many useful surveys. The Zhang-Malik paper is a good place to start. There are several articles in the Handbook of Satisfiability you may find useful.

* [The Quest for Efficient Boolean Satisfiability Solvers](http://www.princeton.edu/~chaff/publication/cade_cav_2002.pdf), Lintao Zhang, Sharad Malik, Joint invited paper for CAV and CADE 2002.
* [Handbook of Satisfiability](http://www.informatik.uni-trier.de/~ley/db/series/faia/faia185.html), Edited by Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, 2009
* [Anatomy and Empirical Evaluation of Modern SAT Solvers](http://eatcs.org/beatcs/index.php/beatcs/article/view/138), Karem Sakallah, Joao Marques-Silva, Bulletin of the EATCS, 2011.

I second the suggestion of Mikolaos. The MiniSAT code is clean and of manageable size. You can play with it. There are several other solvers you can try. CryptoMiniSat is also quite clean. You should also consult the work of [Armin Biere](http://fmv.jku.at/biere/papers/index.html), who writes SAT solvers and writes about writing SAT solvers.


---

### Answer by username_7 on 2011-08-03. Score: 17

I suggest first understanding which techniques really advanced the solvers, for which I would suggest the following [overview and analysis](http://dx.doi.org/10.1007/978-3-642-21581-0_27).

Then I would recommend downloading the source code of [minisat](http://minisat.se/MiniSat.html) and read its [description](http://dx.doi.org/10.1007/978-3-540-24605-3_37).

It might of course be individual but I found looking at the source code most valuable.


---

### Answer by username_8 on 2011-08-04. Score: 9

If you're overwhelmed by all of the work that's out there, why don't you start out pretending that nobody's worked on the problem before? If your goal is to eventually build a competitive SAT solver, it's going to be a fairly long journey. By starting out just playing around without 'checking the solutions', so to speak, you have more to gain than to lose.

First build the simplest solver you can and make sure it works. This will probably be a brute force algorithm whose running time depends more or less only on the $n$, the number of variables, and $m$, the number of clauses. Then implement something a little bit smarter like branch-and-bound. Write (or find) a generator that will give you random instances for given values of $n$ and $m$.

Do some benchmarking tests for your branch-and-bound solver. See how it does for varying values of $n$ and $m$. Then improve your solver to make it faster. See how far you can get without reading about other work. When you run out of ideas, do some of the reading suggested in the other answers.


---

### Answer by username_9 on 2011-12-28. Score: 9

Start with a good survey paper. It's easy to attack the subject piecemeal and get confused by different names in the literature for the same techniques and the same name used for different techniques. It's also easy to re-enact old algorithmic battles (occur lists vs. head-tail lists vs. two watched literals for DPLL implementations for instance) if you don't know what the state of the art is.

[Satisfiability Solvers](http://www.cs.cornell.edu/gomes/papers/SATSolvers-KR-Handbook.pdf) by Gomes, et. al. will give you the rough lay of the land.

[Improving SAT Solvers Using State-of-the-Art Techniques](http://www.emcl-study.eu/fileadmin/master_theses/thesis_manthey.pdf) by Manthey will bring you closer to the present.


---

