Donald Knuth's SAT solvers

(The following text has been copypasted to the SAT/SMT by example book.)

For his chapter 7.2.2.2 about SAT solvers, D.Knuth wrote several SAT solvers:

SAT0
    My implementation of Algorithm 7.2.2.2A (very basic SAT solver)
SAT0W
    My implementation of Algorithm 7.2.2.2B (teeny tiny SAT solver)
SAT8
    My implementation of Algorithm 7.2.2.2W (WalkSAT)
SAT9
    My implementation of Algorithm 7.2.2.2S (survey propagation SAT solver)
SAT10
    My implementation of Algorithm 7.2.2.2D (Davis-Putnam SAT solver)
SAT11
    My implementation of Algorithm 7.2.2.2L (lookahead 3SAT solver)
SAT11K
    Change file to adapt SAT11 to clauses of arbitrary length
SAT12 and the companion program SAT12-ERP
    My implementation of a simple preprocessor for SAT
SAT13
    My implementation of Algorithm 7.2.2.2C (conflict-driven clause learning SAT solver)

( src )

They all are to be filtered via CWEB programs (CWEAVE and CTANGLE). Then you can compile both C and TeX files.

Here I did this for all these programs.

You can see that these solvers require Stanford Graphbase library, but this is just gb_flip.h module for PRNG. You can safely use srand()/rand().

So far, I rewrote only sat0w solver to down-to-earth C language, available in my book or here.

Also, D.Knuth's solver require slightly different input file format (not DIMACS), but the converters are available at the same Knuth's webpage.


List of my other blog posts.

Yes, I know about these lousy Disqus ads. Please use adblocker. I would consider to subscribe to 'pro' version of Disqus if the signal/noise ratio in comments would be good enough.