Also known as: constraint propagation, forward checking

Constraint propagation solves a constraint-satisfaction problem by repeatedly using the constraints to shrink each variable’s set of possible values: fixing one variable forces others, whose new values force still more, cascading until the problem is solved or a contradiction appears.¹² It is the propagation engine inside SAT/SMT solvers and, hand-written for a specific problem shape, is often dramatically faster than a general solver.

Dense constraints make one assignment cascade through many cells, so the search either converges quickly or contradicts itself fast.

How it works

The solver keeps a partial assignment and a worklist. Each newly fixed variable triggers the constraints that mention it, which may fix or restrict further variables (forward checking / unit propagation); contradictions trigger backtracking. When the constraints are dense — many per variable — a single seed assignment forces a long chain, so most wrong guesses die almost immediately. This is exactly the regime where a purpose-built propagator beats a general SMT solver on chained-lookup problems that otherwise cause case-split blow-up.

Relevance to SDR

Recovering a hidden byte table from observed transitions is a constraint-satisfaction problem: each observation fixes or links table cells. In GopherTrunk’s clean-room analysis of the Motorola P25 talker-alias obfuscation (issue #773), a custom propagator over the table cells decided in a single propagation step that a candidate structure was inconsistent — a result the general solver could not reach because the chained lookups stalled it.

Sources

1. Constraint satisfaction problem — Wikipedia, for variables, constraints, and propagation/backtracking. ↩

2. Local consistency — Wikipedia, for constraint propagation and forward checking. ↩

See also

• SAT/SMT solving
• Algebraic attack
• Brute-force attack (exhaustive key search)
• Known-plaintext attack
• Scrambling (whitening)