# sat — CDCL SAT solver

A small C99 CDCL SAT solver demonstrating conflict learning, watched literals,
VSIDS, and Luby restarts. Originally the second annex to *Predictive
Algorithms*; now the codebase backing Chapter 2 of *Practical Solvers*.

About 650 lines for the solver, four worked examples, no dependencies beyond
the standard library.

## Build

    ./build.zsh

Produces:

- `build/sanity` — seven smoke tests, runs automatically
- `build/ex1_pigeonhole` — PHP(7, 6) UNSAT (classical hard case)
- `build/ex2_queens` — 8-Queens as SAT
- `build/ex3_coloring` — Petersen graph k-colouring (k=2 UNSAT, k=3 SAT)
- `build/ex4_sudoku` — "AI Escargot" sudoku (a famously hard puzzle)

The build script runs the sanity tests and each example after compiling it.

## Layout

    src/sat.h               public API (~75 lines)
    src/sat.c               CDCL implementation (~650 lines)
    examples/ex*.c          four worked examples
    sanity.c                smoke tests
    build.zsh               build script

## Reading

For the canonical write-up, read **Chapter 2 of *Practical Solvers***
(`../books/practical-solvers/practical-solvers.pdf`) — the consolidated
treatise covers this solver in detail, with the full annotated source
reproduced as Appendix A.

The original standalone annex is preserved at
`../books/background/cdcl-annex.{pdf,tex}` for historical reference.

The four examples are arranged in order of increasing payoff: pigeonhole
(UNSAT proof from learning), queens (generic encoding beating
problem-specific propagation), graph coloring (NP-complete decision
problem), sudoku (a real puzzle in ten conflicts).
