Knuth and SAT

Presentation by Knuth about SAT problems and solvers (and also a little bit about Integer Programming). Not new but still interesting..

Section 7.2.2.2 is about SAT. Ran out of extra space for more sub-numbering:

Looks like Donald Knuth got a bit sidetracked by this subject (his program SAT13 seems to indicate he implemented at least 13 SAT solvers). He had the same thing when starting on the book TAOCP. He did not like any of the available typesetting software. So he implemented TeX. Then he did not like the fonts, so he implemented MetaFont. There is a similar story about about Bill Orchard-Hays: he needed to implement an LP solver on a different machine. In those times everything was coded in assembly. Well, he did not like the assembler, so he started with implementing a proper macro-assembler. Then he did not like the linker, so he implemented a new linker. After that it just took a few weeks to implement the LP solver. (I am not sure this story is 100% true, but it could well be).

Knuth mentions integer programming and Cplex when discussing pictures like:

References

1. Donald E. Knuth, The Art of Computer Programming, Volume 4, Fascicle 6, Satisfiability, 2015
2. William Orchard-Hays, Advanced Linear Programming Computing Techniques, 1968.