Why does encoding a hard scheduling problem for a mature satisfiability solver usually beat writing your own backtracking search?

## What you are handing over The decision is not *search versus no search* — both approaches search. It is **who writes the search**. A hand-rolled backtracker over a scheduling problem usually amounts to: pick an unassigned decision, try each option, recurse, and on contradiction undo the last choice. That is where most in-house implementations stop, because everything past it is hard to build and harder to keep correct. ## What a conflict-driven solver adds - **Unit propagation.** Whenever a constraint has one remaining way to be satisfied, the solver fixes it immediately and cascades. Implemented with a watched-literal scheme, this costs almost nothing per assignment and does most of the real work. - **Conflict analysis and clause learning.** On reaching a contradiction the solver analyses *why*, derives a new clause that rules out the responsible combination, and adds it. The learned clause is logically implied by the original formula, so the solution set is unchanged — but the same contradiction is never re-derived, anywhere else in the tree. - **Backjumping.** Rather than undoing the most recent decision, the solver jumps back to the decision level the conflict actually depended on, discarding irrelevant work between. - **Activity-based branching.** Variables that appear in recent conflicts are branched on first, so the search concentrates where the instance is genuinely hard. - **Restarts that keep what was learned.** The assignment trail is abandoned, the learned clauses are not. This re-samples the search order while retaining the pruning bought so far. A plain backtracking search re-derives the same contradiction once per subtree that contains it. Learning it once is the single biggest difference between the two approaches. | | Hand-written backtracker | Mature conflict-driven solver | |---|---|---| | Contradiction | undo last choice, retry | learn a clause, jump back | | Same conflict elsewhere | re-derived every time | ruled out once, globally | | Branching order | fixed by your code | driven by recent conflicts | | Your responsibility | the whole search | the encoding | ## The encoding becomes the work Handing search over does not hand over modelling. You now choose what each variable *means* and how each rule is expressed, and those choices swing runtime by orders of magnitude. - **At-most-one constraints.** The direct encoding forbids every pair, which over `k` candidates is `k(k-1)/2` clauses — for `k = 100` that is 4,950 clauses for a single rule, and the quadratic growth soon dominates the input. Compact alternatives introduce auxiliary variables and encode the same rule in a number of clauses that grows far more slowly. - **Counting and cardinality rules.** Naive expansions explode; structured encodings stay manageable and often propagate better, which matters more than raw clause count. - **Symmetry.** If two interchangeable resources make two assignments that differ only by a relabelling, the search may explore both. Adding constraints that fix an arbitrary order among symmetric objects removes that duplicated work. - **Propagation-friendliness.** Two encodings with the same solution set can differ sharply in how early propagation detects a dead branch. Prefer the one whose forced consequences fire soon. ## What you give up 1. **A decision procedure is not an optimiser.** A satisfiability answer is *satisfiable with this assignment* or *unsatisfiable*. To minimise a cost you solve, add a constraint requiring a strictly better cost, and solve again — each round either improves the incumbent or proves the previous one optimal. 2. **Runtimes are erratic.** Nearly identical instances can differ enormously in solve time, so nightly capacity planning must assume the tail, not the median. 3. **Structure is flattened.** Rich domain structure becomes undifferentiated variables and clauses, and a solver cannot exploit what your encoding threw away. 4. **Debugging moves.** An unsatisfiable answer is now ambiguous between *the requirement really is impossible* and *my encoding says something I did not mean*. Keeping a minimal reproducing subset of constraints, and testing the model against known-feasible plans, is how you tell those apart. ## Which solver, though The question of which solver matters and is often glossed. A **satisfiability solver** takes a formula over Boolean variables in conjunctive normal form; everything else you express by encoding. A **constraint solver** keeps variables with richer finite domains and supports global constraints — for example *all these assignments must differ* — each with a specialised propagator that reasons about the whole group at once, which a flattened Boolean encoding cannot do as sharply. Where a problem is naturally about distinctness, capacities and intervals, the richer model often wins; where it is naturally Boolean and conflict-heavy, clause learning often wins. Naming that choice, rather than saying *use a solver*, is what a senior answer sounds like.