Donald Knuth's SAT solvers

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

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

    My implementation of Algorithm (very basic SAT solver)
    My implementation of Algorithm (teeny tiny SAT solver)
    My implementation of Algorithm (WalkSAT)
    My implementation of Algorithm (survey propagation SAT solver)
    My implementation of Algorithm (Davis-Putnam SAT solver)
    My implementation of Algorithm (lookahead 3SAT solver)
    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
    My implementation of Algorithm (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. My company.

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.