SAT: Getting started

I recently participated in Al Zimmerman's Programming Contest. Tomas Rokicki, the runner up of this contest, published a writeup of his solution, which was a very interesting read. Specifically, it made me interested in learning more about SAT solvers.

My excitement was amplified by having heard Donald Knuth say "Satisfiability is something that turned out to be extremely important the more I looked at it".

By Rokicki's recommendation, I started reading Knuth's preprint about satisfiability. After working with pen and paper for a while, I felt that the material would open itself up more naturally if I had the chance to implement SAT problems and scale.

I installed python-sat. It comes with some good solvers. The documentation looks solid too. Installation procedure:

$ pip install six

$ pip install python-sat

Pysat works with integers as variable names, as far as I can see. Below a naive way to work around that, to increase model readability:

.