(The following text has been copypasted to the SAT/SMT by example book.)
For his chapter 184.108.40.206 about SAT solvers, D.Knuth wrote several SAT solvers:
SAT0 My implementation of Algorithm 220.127.116.11A (very basic SAT solver) SAT0W My implementation of Algorithm 18.104.22.168B (teeny tiny SAT solver) SAT8 My implementation of Algorithm 22.214.171.124W (WalkSAT) SAT9 My implementation of Algorithm 126.96.36.199S (survey propagation SAT solver) SAT10 My implementation of Algorithm 188.8.131.52D (Davis-Putnam SAT solver) SAT11 My implementation of Algorithm 184.108.40.206L (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 220.127.116.11C (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.