For his chapter 18.104.22.168 about SAT solvers, D.Knuth wrote several SAT solvers:
SAT0 My implementation of Algorithm 22.214.171.124A (very basic SAT solver) SAT0W My implementation of Algorithm 126.96.36.199B (teeny tiny SAT solver) SAT8 My implementation of Algorithm 188.8.131.52W (WalkSAT) SAT9 My implementation of Algorithm 184.108.40.206S (survey propagation SAT solver) SAT10 My implementation of Algorithm 220.127.116.11D (Davis-Putnam SAT solver) SAT11 My implementation of Algorithm 18.104.22.168L (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 22.214.171.124C (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.
Please drop me email about bug(s) and/or suggestion(s): firstname.lastname@example.org. List of other blog posts. Follow me in social networks: Twitter, Telegram, GitHub, Discord, Facebook.