Backtracking -- Brief ☧
Deep version -> | Back to SAT/SMT ->
Q: Have you ever been driving, missed a turn, and had to loop back
to the intersection to try a different road? That's basically backtracking.
But let's ground it in constraint solving. After we propagate constraints
and narrow domains, sometimes we're stuck: no more propagation is possible,
but variables still have multiple options. What do we do?
A: We guess. We pick a variable, choose one of its remaining values,
and see what happens. If the guess eventually leads to a contradiction
(some domain becomes empty), we undo that guess and try a different
value. We go back to the last choice point and take the other fork.
Q: So it's like exploring a maze?
A: Exactly. You walk forward. When you hit a dead end, you don't start
over from the entrance. You go back to the last junction and try a
different corridor. The Israelites wandering in the wilderness did the
same thing -- when they hit a mountain or an enemy camp, they turned back
to the last choice point and tried another direction.
Q: Can you show me step by step?
A: Sure. Three tribal leaders must sit in three seats (A, B, C).
Each seat draws from {Judah, Dan, Ephraim}. No two can be the same.
Step 1: Guess A = Judah Propagate: B in {Dan, Ephraim}, C in {Dan, Ephraim} Step 2: Guess B = Dan Propagate: C in {Ephraim} Step 3: C = Ephraim (forced -- only one option). Done! Solution: A=Judah, B=Dan, C=EphraimThat went smoothly. But now add a constraint: "A and C cannot both be
from southern tribes (Judah, Ephraim)":
Step 3: C = Ephraim, but A=Judah -- both southern! CONTRADICTION. -> Backtrack to Step 2. Step 2b: Guess B = Ephraim Propagate: C in {Dan} Step 3b: C = Dan. Check: A=Judah (south), C=Dan (north). OK! Solution: A=Judah, B=Ephraim, C=DanQ: This feels like it could be slow for big problems. What if you
backtrack a lot?
A: Good instinct. In the worst case, backtracking explores every
possible combination -- that's exponential time. But smart strategies
dramatically cut down the search. And our FPGA takes a different approach
entirely: it evaluates many branches in parallel. Instead of going
down one path and backtracking, it explores multiple paths at once --
each "world" is a row in a matrix.
Backtracking Strategies
Not all backtracking is created equal. The difference between a naive solver
and a state-of-the-art one often comes down to how it backtracks -- not
just that it backtracks. Here are the main approaches, from simplest to
most sophisticated:
| Strategy | How It Backtracks | Analogy |
|---|---|---|
| Chronological | Undo the most recent guess | Go back one step |
| Backjumping | Skip to the guess that caused the conflict | Jump back to the wrong turn |
| Conflict-driven (CDCL) | Learn a clause to avoid the same mistake forever | "Remember: that road has no water" |
Each strategy addresses a real problem. Chronological backtracking is
simple but wasteful -- it might undo a perfectly good guess just because it
was the most recent one, even though the real problem was three decisions ago.
Backjumping fixes this by analyzing which decision actually caused the
contradiction and jumping directly to it, skipping irrelevant intermediate
choices. CDCL goes even further: it does not just jump back but learns
from the failure, adding a new constraint that prevents the solver from ever
reaching the same dead end again.
CDCL is what modern SAT solvers use, and it is the reason they can solve
problems with millions of variables. When they hit a contradiction, they
analyze why it happened and add a new constraint (a "learned clause") to
prevent the same dead end from being explored again. It is
recursion with memory -- the solver
genuinely learns from its mistakes.
Our FPGA takes a fundamentally different approach: rather than exploring one
path and backtracking when it fails, it evaluates many branches in parallel.
Each "world" is an independent row in a matrix, and failed worlds are simply
discarded. This trades the clever learning of CDCL for raw parallelism -- and
for the domain-intersection problems our hardware is designed for, that
parallelism wins.
Soli Deo Gloria