Practical Solvers

Five constraint-solving paradigms — CDCL, MILP, SMT, LCG, and MaxSAT — each built from scratch in C99, with a user guide for every solver.

Download book + library Read the book (PDF)

Version 1.1 · about 12,700 lines of C99 · about 80 pages

Practical Solvers picks up where Predictive Algorithms left off. Where that book built a constraint solver and a Dancing Links exact-cover engine from scratch, this one tackles the solver architectures used in industry: CDCL SAT solving, mixed-integer linear programming, satisfiability modulo theories, lazy clause generation, and MaxSAT. Each solver is self-contained, builds independently, and comes with its own user guide focused on modelling patterns and worked examples.

The book closes with a comparison of when to reach for SAT versus SMT versus CSP versus MILP, and what hybrid patterns look like in operational systems.

In the library

CDCL SAT Solver

Conflict-driven clause learning with two-watched-literal propagation, first-UIP conflict analysis, non-chronological backjumping, VSIDS branching, and Luby restarts. About 730 lines of C99. Examples: pigeonhole, N-Queens, graph colouring, Sudoku.

MILP Solver

Two-phase revised simplex with recursive branch-and-bound. Continuous, integer, and binary variables. About 575 lines of C99. Examples: knapsack, assignment, set cover, weapon-target assignment.

SMT Solver

DPLL(T) architecture with congruence closure (EUF), General Simplex with Farkas explanations (LRA), and Nelson–Oppen combination. About 2,400 lines of C99. Examples include UI layout constraint solving.

Lazy Clause Generation

CP-style propagators with CDCL-style learning. Built-in alldifferent and cumulative propagators, user-extensible. About 1,830 lines of C99. Examples: linear constraints, custom propagators, N-Queens, cumulative scheduling, DWTA.

MaxSAT Solver

Partial MaxSAT with hard and soft clauses. Both model-improving (linear) and core-guided (Fu–Malik) algorithms. About 740 lines of C99. Examples: overconstrained WTA, core vs. linear comparison, weighted DWTA.

Building

$ unzip practical-solvers.zip
$ cd practical-solvers/CDCL-Solver
$ ./build.zsh     # compiles, runs sanity tests and examples

Each solver folder is self-contained. The build.zsh script compiles the library, the sanity tests, and the example programs, then runs them automatically. Override flags with CFLAGS="-O0 -g" ./build.zsh.

C99 compiler (clang or gcc)
zsh (build scripts)
No external dependencies — standard library only
macOS, Linux, BSD — anything POSIX

Download book + library Read the book (PDF)