Lesson 03
How a SAT solver searches
How can a program rule out enormous numbers of Boolean assignments?
A modern Boolean satisfiability (SAT) solver propagates forced values, analyzes conflicts, learns clauses, and returns to the earliest choice responsible for a contradiction.
After this lesson, you should be able to
- Explain the Boolean satisfiability problem and its three common solver outcomes.
- Trace propagation, a decision, a conflict, clause learning, and backtracking.
- State what a DRAT certificate checks and what remains outside that check.
3.1
Propagation uses clauses before guessing
A clause with one undecided literal and all other literals false forces its remaining literal to true. This operation is unit propagation. Repeating it can determine many values without a search decision.
When propagation stops, the solver chooses a value for an undecided variable. The choice opens a branch. More propagation follows until the solver finds a model or makes some clause false.
3.2
A conflict produces reusable information
Conflict-driven clause learning, abbreviated CDCL, records why propagated values were forced. When a conflict occurs, the solver follows those reasons backward and derives a new clause. That clause blocks the failing combination and can force values elsewhere.
The solver can return past several recent choices instead of reversing only the last one. This non-chronological backtracking is useful because the conflict may depend on an older choice and not on the intervening assignments.
3.3
Certificates separate search from checking
Search code uses heuristics to choose variables, remove clauses, restart, and manage memory. An unsat certificate records a derivation that a smaller checker can validate without trusting those heuristics.
DRAT is one common certificate format. Its checker works on the CNF problem. If an earlier AIG or SMT translation changed the problem, the certificate still proves only that the translated clauses are unsat.
3.4
Axeyum's SAT component
Axeyum implements AIG construction, CNF lowering, CDCL search, learned clauses, and certificate support in Rust. The SAT component can be tested on its own and also acts as the final decision layer for some bit-blasted SMT queries.
CaDiCaL and Kissat are external reference points for SAT solving. They are not part of Axeyum's default execution path.
Worked example
Learn from one failed choice
Consider the clauses (not a or b), (not a or not b), and (a or c).
- Decide
Choose a = true.
- Propagate
The first clause forces b = true. The second clause forces b = false.
- Analyze
Both forced values came from choosing a = true. The current branch cannot work.
- Learn
The solver can learn not a and backtrack to a = false.
- Finish
With a = false, the third clause forces c = true. Either value of b now satisfies the first two clauses.
Result. The formula is sat, and the conflict establishes the useful consequence not a.
3.5
Check your understanding
Answer each question before opening the explanation.
1 Why is a learned clause safer than permanently recording a heuristic guess?
The learned clause is derived from existing constraints, while a guess need not follow from them.
2 What does a DRAT proof fail to check in a bit-blasted SMT route?
It does not check that the translation from the original theory terms to CNF preserved their meaning.
Concept wiki
Terms in this lesson
- SAT The problem of deciding whether a Boolean formula has a satisfying assignment.
- Unknown result A report that the solver did not decide the query.
- AIG A graph representation built from and nodes and complemented edges.
- CDCL A SAT search method that learns clauses from conflicts.
- Unit propagation Assigning the only remaining value that can keep a clause true.
- SAT search decision A provisional variable assignment chosen when propagation cannot continue.
- Conflict A clause made false by the current partial assignment.
- Backtracking Returning to an earlier search state after a conflict.
- Learned clause A new clause derived from a conflict and added to the SAT problem.
- Proof certificate A checkable record supporting a solver's result.
- DRAT A common SAT proof format based on redundant clause additions.