SAT Solvers

The Silent (R)evolution of SAT

Looking at the ACM page of the MIT Computer Science & Artificial Intelligence Laboratory, the first article (at the time of writing) in the Downloads section is

Johannes K. Fichte, Daniel Le Berre, Markus Hecher, and Stefan Szeider. The Silent (R)evolution of SAT. Commun. ACM 66, 6 (June 2023), 64–72.

The corresponding acm page releases its pdf in open access mode; for the sake of clarity, its abstract follows:

Today’s powerful, robust SAT solvers have become primary tools for solving hard computational problems.

Knuth hosts lots of programs, in particular he provides many implementations of SAT solvers, given in the CWEB format:

Algorithm 7.2.2.2A, a very basic SAT solver with the generated c source and pdf;
Algorithm 7.2.2.2B, a teeny tiny SAT solver with the generated c source and pdf;
Algorithm 7.2.2.2W, a walk SAT solver with the generated c source and pdf;
Algorithm 7.2.2.2S, a survey propagation SAT solver with the generated c source and pdf;
Algorithm 7.2.2.2D, a Davis-Putnam SAT solver with the generated c source and pdf;
Algorithm 7.2.2.2L, a lookahead 3SAT solver with the generated c source and pdf. Moreover, a change file that adapts to clauses of arbitrary length, with the generated c source and pdf;
preprocessor, for SAT solver with the generated c source and pdf;
a companion preprocessor, for SAT solver with the generated c source and pdf;
Algorithm 7.2.2.2C, a conflict-driven clause learning SAT solver with the generated c source and pdf;
encoder, a forcing encoding of regular languages into SAT via nondeterministic finite automata with the generated c source and pdf.

We compiled and ship the corresponding executables in the sat.cweb image that can be pulled easily:

docker pull ghcr.io/massimo-nocentini/sat.cweb:master