optional · interactive figures
20
Explore: SAT and CDCL
A CDCL solver run event by event: decisions, unit propagation through watched literals, conflicts, learning and backjumps.
optional: nothing in the lab depends on it back to the slides
These figures support the slides; they don't replace them, and the unit is complete
without them. Each one is computed from the unit's own data or reference solution, so
what you see agrees with the numbers on the slides.
Inside a figure, the arrow keys and drags belong to the figure; click outside it (or
press Esc) to use them for the slides again.
20 · explore
CDCL, event by event
Try: step to the conflict, then the analysis: the learned clause and the first UIP light up. Then switch to the pigeonhole run, which ends unsatisfiable. Static versions: watched literals , the implication graph , the learned clause .
What it shows. A CDCL run as its implication graph (one column per decision level,
filled nodes are decisions, arrows come from reason clauses) and its clause list (watched
literals underlined, true in green, false struck through).
The deck's four clauses : decide x1, propagate x3, decide x2, propagate x4 and x5,
conflict in (¬x4 ∨ ¬x5), learn (¬x2 ∨ ¬x3) with backjump to level 1, propagate ¬x2 from the learned clause, decide x4, propagate ¬x5: a model.Three pigeons, two holes : one decision, a conflict, a learned unit clause at level 0, and a
second conflict at level 0: unsatisfiable.
Data. slides/viz/traces/u20.py subclasses the reference Solver
only to take snapshots; the first two decisions of the deck's run are scripted, the rest are the
reference's own. Its satisfiability answer is checked against a plain reference run.