--- title: CSP Search and Structure module: Search moduleNumber: 2 lessonNumber: 10 order: 210 summary: > Propagation prunes a CSP but rarely finishes it, so we search. This lesson builds backtracking search over partial assignments and the general-purpose heuristics that make it fast — MRV, degree, least-constraining-value, forward checking, MAC, and intelligent backtracking. It then shows how the shape of the constraint graph controls difficulty: tree-structured problems fall in linear time, cutset conditioning handles the rest, and min-conflicts local search solves a million queens in a constant number of steps. topics: [Search] sources: - book: AIMA ref: "Ch. 6 — Constraint Satisfaction Problems; §6.3 Backtracking Search for CSPs" - book: AIMA ref: "§6.4 Local Search for CSPs; §6.5 The Structure of Problems" --- The companion lesson, [Constraint Satisfaction Problems](/artificial-intelligence/search/constraint-satisfaction), defined the CSP as a triple $(X, D, C)$ of variables, domains, and constraints, and developed **constraint propagation** — node and arc consistency, and the AC-3 algorithm that shrinks domains before search. Propagation alone rarely solves the problem, though: it left Australia's $V$ and $T$ with choices still to make. This lesson supplies the search that finishes the job, the general-purpose heuristics that make it fast, and the structural facts that make whole classes of CSP easy. ## Backtracking search Inference alone rarely finishes the job, so we search. The naive move is standard depth-first search over partial assignments, adding one $\mathit{var} = \mathit{value}$ at a time — but that ignores a property every CSP has: **commutativity**. The order in which we assign variables never changes the resulting set of assignments, so at each node we need consider only a _single_ variable rather than branching over which variable to assign next. That collapses the tree from $n! \cdot d^n$ leaves to the $d^n$ we actually need.[^aima-commut] **Backtracking search** is depth-first search with this restriction: pick one unassigned variable, try its values in turn, recurse, and back up when a variable has no consistent value left. Because CSPs use a standardized representation, the algorithm needs no domain-specific initial state, action model, or goal test — the three plug-in functions $\textsc{Select-Unassigned-Variable}$, $\textsc{Order-Domain-Values}$, and $\textsc{Inference}$ carry all the cleverness.[^aima-bt] This is the same structure as generic [backtracking](/algorithms/backtracking/backtracking-fundamentals) over a [constraint search](/algorithms/backtracking/constraint-search) tree, specialized to the variable-domain-constraint frame. ```algorithm caption: $\textsc{Backtracking-Search}$ — depth-first search over assignments input: a CSP $\mathit{csp}$ return $\textsc{Backtrack}(\{\,\}, \mathit{csp})$ function $\textsc{Backtrack}(\mathit{assignment}, \mathit{csp})$ if $\mathit{assignment}$ is complete then return $\mathit{assignment}$ $\mathit{var} \gets \textsc{Select-Unassigned-Variable}(\mathit{csp})$ for each $\mathit{value}$ in $\textsc{Order-Domain-Values}(\mathit{var}, \mathit{assignment}, \mathit{csp})$ do if $\mathit{value}$ is consistent with $\mathit{assignment}$ then add $\{\mathit{var} = \mathit{value}\}$ to $\mathit{assignment}$ $\mathit{inferences} \gets \textsc{Inference}(\mathit{csp}, \mathit{var}, \mathit{value})$ if $\mathit{inferences} \ne \mathit{failure}$ then add $\mathit{inferences}$ to $\mathit{assignment}$ $\mathit{result} \gets \textsc{Backtrack}(\mathit{assignment}, \mathit{csp})$ if $\mathit{result} \ne \mathit{failure}$ then return $\mathit{result}$ remove $\{\mathit{var} = \mathit{value}\}$ and $\mathit{inferences}$ from $\mathit{assignment}$ return $\mathit{failure}$ ``` The tree it explores, on the Australia map with the fixed order $WA, NT, Q, \ldots$, begins by branching on $WA$'s three colors, then on $NT$'s, and so on. Most of that tree is dead weight — the figure shows the top two levels, where two of the three $NT$ branches under $WA=red$ already clash and get cut. A solver with good heuristics and forward checking never generates most of these nodes at all. $$ % caption: The top of the backtracking tree for the map, variables assigned in the % order $WA, NT, Q$. Under $WA=R$, choosing $NT=R$ violates the $WA \ne NT$ % constraint (struck, cut immediately); the two live branches continue to $Q$. \begin{tikzpicture}[>=stealth, font=\footnotesize, nd/.style={draw, minimum width=10mm, minimum height=5mm, inner sep=2pt, font=\scriptsize}, dead/.style={draw, minimum width=10mm, minimum height=5mm, inner sep=2pt, font=\scriptsize, text=red}] \definecolor{acc}{HTML}{2348F2} \definecolor{red}{HTML}{C0392B} \node[nd] (root) at (0,3) {WA=R}; \node[dead] (n1) at (-3,1.6) {NT=R}; \node[nd] (n2) at (0,1.6) {NT=G}; \node[nd] (n3) at (3,1.6) {NT=B}; \draw[->] (root) -- (n1); \draw[->, acc, thick] (root) -- (n2); \draw[->] (root) -- (n3); \node[red, font=\scriptsize] at (-3,0.8) {clash}; \draw[red, thick] (-3.55,1.35) -- (-2.45,1.85); \node[nd] (q1) at (-1,0.3) {Q=R}; \node[nd] (q2) at (1,0.3) {Q=B}; \draw[->, acc, thick] (n2) -- (q1); \draw[->, acc, thick] (n2) -- (q2); \node[font=\scriptsize] at (3,0.3) {(subtree)}; \draw[->] (n3) -- (3,0.6); \end{tikzpicture} $$ ### Heuristics that make it fast A CSP is solved efficiently _without_ any domain-specific heuristic — the structure supplies general ones instead. They answer three questions: which variable next, which value next, and what to infer after each choice. **Minimum-remaining-values (MRV).** Choose the variable with the fewest legal values left. Also called the "most constrained variable" or "fail-first" heuristic: a variable near the end of its options is the most likely to fail soon, and if one has _no_ legal values, MRV picks it and detects the dead end immediately instead of wandering. MRV routinely beats static ordering by a factor of a thousand or more.[^aima-order] **Degree heuristic.** MRV is useless at the very first move, when every variable has all its values. The degree heuristic breaks the tie by choosing the variable involved in the most constraints on other unassigned variables — it shrinks the branching factor of future choices. On Australia, $SA$ has degree $5$ against the others' $2$ or $3$; choosing $SA$ first lets any consistent color follow with no backtracking at all.[^aima-order] **Least-constraining-value (LCV).** Having picked a variable, order its values by how _few_ choices they rule out for neighbors — leave the maximum flexibility for the rest. With $WA=red$, $NT=green$ already set and $Q$ next, choosing $Q=blue$ would strip $SA$ of its last option, so LCV prefers $red$. Variable selection is fail-first, but value selection is fail-_last_: we need only one solution, so we try the value most likely to lead to one.[^aima-order] $$ % caption: The three ordering heuristics on the map. Degree picks $SA$ (five % edges, thick) at the root; MRV then favors whichever neighbor has the smallest % remaining domain; LCV orders that variable's colors to preserve options for % $SA$ and the others. \begin{tikzpicture}[>=stealth, font=\small, reg/.style={circle, draw, minimum size=8mm, inner sep=1pt}] \definecolor{acc}{HTML}{2348F2} \node[reg, draw=acc, thick, text=acc] (SA) at (0,0) {SA}; \node[reg] (WA) at (-2.2,1.1) {WA}; \node[reg] (NT) at (-1.1,2.0) {NT}; \node[reg] (Q) at (1.1,2.0) {Q}; \node[reg] (NSW) at (2.2,0.6) {NSW}; \node[reg] (V) at (0.7,-1.7) {V}; \draw[acc, thick] (SA) -- (WA); \draw[acc, thick] (SA) -- (NT); \draw[acc, thick] (SA) -- (Q); \draw[acc, thick] (SA) -- (NSW); \draw[acc, thick] (SA) -- (V); \draw (WA) -- (NT); \draw (NT) -- (Q); \draw (Q) -- (NSW); \draw (NSW) -- (V); \node[anchor=north east, text=acc, font=\footnotesize] at (-0.5,-0.5) {degree 5}; \end{tikzpicture} $$ ### Interleaving search and inference Inference is even stronger inside the loop than before it: every assignment is a fresh chance to prune neighbors. **Forward checking.** When $X$ is assigned, delete from each unassigned neighbor's domain any value inconsistent with $X$'s choice. It establishes arc consistency _for the assigned variable only_. Combined with MRV, it computes exactly the remaining-value counts MRV needs. But it looks only one step out: it can leave two _unassigned_ neighbors mutually inconsistent and not notice. $$ % caption: Forward checking on the map, one row per assignment. Domains start full % (R, G, B); assigning $WA=red$ deletes R from $NT$ and $SA$; $Q=green$ deletes G % from $NT$, $NSW$, $SA$; $V=blue$ empties $SA$ — the dead end is caught before % $SA$ is ever chosen. \begin{tikzpicture}[>=stealth, font=\footnotesize] \definecolor{acc}{HTML}{2348F2} \definecolor{red}{HTML}{C0392B} % column headers \foreach \name/\x in {WA/1, NT/2.4, Q/3.8, NSW/5.2, V/6.6, SA/8.0} { \node[acc] at (\x,3.4) {\name}; } \node[anchor=east, font=\scriptsize] at (0.2,2.7) {start}; \node[anchor=east, font=\scriptsize] at (0.2,1.8) {WA=red}; \node[anchor=east, font=\scriptsize] at (0.2,0.9) {Q=green}; \node[anchor=east, font=\scriptsize] at (0.2,0.0) {V=blue}; % row: start -- all full \foreach \x in {1,2.4,3.8,5.2,6.6,8.0} { \node at (\x,2.7) {R G B}; } % row: WA=red -> WA=R fixed; NT,SA lose R \node[acc] at (1,1.8) {R}; \node at (2.4,1.8) {G B}; \node at (3.8,1.8) {R G B}; \node at (5.2,1.8) {R G B}; \node at (6.6,1.8) {R G B}; \node at (8.0,1.8) {G B}; % row: Q=green -> NT->B, NSW->R B, SA->B \node[acc] at (1,0.9) {R}; \node at (2.4,0.9) {B}; \node[acc] at (3.8,0.9) {G}; \node at (5.2,0.9) {R B}; \node at (6.6,0.9) {R G B}; \node at (8.0,0.9) {B}; % row: V=blue -> NSW->R, SA empty \node[acc] at (1,0.0) {R}; \node at (2.4,0.0) {B}; \node[acc] at (3.8,0.0) {G}; \node at (5.2,0.0) {R}; \node[acc] at (6.6,0.0) {B}; \node[red] at (8.0,0.0) {none}; \end{tikzpicture} $$ **Maintaining Arc Consistency (MAC).** After assigning $X_i$, run AC-3 — but seed its queue only with the arcs $(X_j, X_i)$ from unassigned neighbors $X_j$, then let propagation recurse as usual. MAC catches exactly the inconsistency forward checking misses (two unassigned neighbors forced to clash), because forward checking does only the initial-arc pass while MAC recurses through the whole graph. MAC is strictly more powerful than forward checking.[^aima-mac] ### Looking backward: backjumping and no-goods When a branch dies, plain **chronological backtracking** just undoes the most recent decision — even when that decision is irrelevant to the failure. Fix the variable order $Q, NSW, V, T, SA, WA, NT$ and suppose search has reached $\{Q=red,\, NSW=green,\, V=blue,\, T=red\}$. The next variable, $SA$, borders $Q$, $NSW$, and $V$, and every color it could take clashes with one of them: it has no legal value. Chronological backtracking now backs up to $T$ and recolors Tasmania — which is absurd, because $T$ constrains nothing that touches $SA$. The repair is to record, for each variable, a **conflict set**: the earlier assignments that ruled out its values. Here $SA$'s conflict set is $\{Q=red,\, NSW=green,\, V=blue\}$. **Backjumping** retreats not to the previous variable but to the most recent assignment in that set — $V$ — skipping $T$ entirely. The conflict set falls out of forward checking for free: whenever assigning $X = x$ deletes a value from $Y$, add $X = x$ to $Y$'s conflict set.[^aima-back] Simple backjumping has a subtle limit — it fires only when a domain is _emptied_, and forward checking already prunes every such node before search reaches it, so on its own it is redundant. The idea becomes useful in the deeper form. Suppose $\{WA=red,\, NSW=red\}$ (already inconsistent for reasons downstream), then $T=red$, then $NT, Q, V, SA$ are tried and, after much thrashing, $NT$ runs out of values. $NT$'s _direct_ conflicts do not include a complete set of culprits, so plain backjumping is stuck. **Conflict-directed backjumping** propagates conflict sets backward: when the current variable $X_j$ exhausts its domain, the variable $X_i$ it jumps to absorbs $X_j$'s conflicts, $$ \mathit{conf}(X_i) \gets \mathit{conf}(X_i) \cup \mathit{conf}(X_j) \setminus \{X_i\}, $$ so the reason for failure flows back through the chain $SA \to Q \to NT \to NSW$ until it reaches $NSW$, the true culprit, and Tasmania is skipped every time.[^aima-back] **Constraint learning** goes one step further: extract a minimal subset of the conflict set that guarantees failure — a **no-good** — and record it as a new constraint (or in a side cache) so the same doomed combination is never tried again. Recording $\{WA=red,\, NT=green,\, Q=blue\}$ as a no-good is pointless if that branch is pruned once and never revisited, but if $V$ and $T$ are assigned _above_ it in the tree, the same $\{WA, NT, Q\}$ clash recurs under every setting of $V$ and $T$, and the cached no-good kills each recurrence instantly. Constraint learning is one of the most important techniques in modern CSP and SAT solvers, and we return to its SAT incarnation below. ## The structure of problems The shape of the constraint graph controls how hard the CSP is: a problem that splits into loosely connected pieces, or has no cycles, gives search almost nothing to backtrack over. Two structural facts do most of the work. **Independent subproblems.** If the constraint graph splits into [connected components](/artificial-intelligence/foundations/what-is-ai) — Tasmania touches no mainland region — each component is solved separately and the solutions combined. Splitting $n$ variables into subproblems of $c$ variables each turns $O(d^n)$ into $O(d^c \cdot n/c)$, linear in $n$. Dividing a Boolean CSP of 80 variables into four independent pieces of 20 cuts the worst case from the age of the universe to under a second.[^aima-struct] **Tree-structured CSPs.** A constraint graph that is a **tree** — any two variables joined by exactly one path — is solvable in _linear_ time. Pick any variable as the root and **topologically sort** so each variable follows its parent. Sweep from the leaves to the root making each parent-child arc consistent ($O(nd^2)$ over the $n-1$ arcs), then sweep root-to-leaf assigning values: because every arc is arc-consistent, each child always has a value compatible with its already-chosen parent, so no backtracking ever happens. $$ % caption: A tree-structured CSP (left) and a topological order rooting it at $A$ % (right). Directed arc consistency along the order guarantees a backtrack-free % assignment sweep, so the whole CSP solves in $O(n d^2)$ time. \begin{tikzpicture}[>=stealth, font=\small, v/.style={circle, draw, minimum size=7mm, inner sep=1pt}] \definecolor{acc}{HTML}{2348F2} % left: the tree \node[v] (A) at (0,0.9) {A}; \node[v] (B) at (1.2,0) {B}; \node[v] (C) at (0,-0.9) {C}; \node[v] (D) at (2.4,0) {D}; \node[v] (E) at (3.6,0.9) {E}; \node[v] (F) at (3.6,-0.9){F}; \draw (A) -- (B); \draw (C) -- (B); \draw (B) -- (D); \draw (D) -- (E); \draw (D) -- (F); % right: topological order \begin{scope}[xshift=6.2cm] \node[v] (tA) at (0,0) {A}; \node[v] (tB) at (1.1,0) {B}; \node[v] (tC) at (2.2,0) {C}; \node[v] (tD) at (3.3,0) {D}; \node[v] (tE) at (4.4,0) {E}; \node[v] (tF) at (5.5,0) {F}; \draw[->, acc, thick] (tA) -- (tB); \draw[->, acc, thick] (tB) -- (tC); \draw[->, acc, thick] (tC) -- (tD); \draw[->, acc, thick] (tD) -- (tE); \draw[->, acc, thick] (tE) -- (tF); \end{scope} \end{tikzpicture} $$ ```algorithm caption: $\textsc{Tree-CSP-Solver}$ — solve a tree-structured CSP in linear time input: a CSP with components $(X, D, C)$ whose graph is a tree $n \gets$ number of variables in $X$ $\mathit{root} \gets$ any variable in $X$ $X \gets \textsc{TopologicalSort}(X, \mathit{root})$ for $j = n$ downto $2$ do // leaves up to root: enforce directed arc consistency $\textsc{Make-Arc-Consistent}(\text{Parent}(X_j), X_j)$ if it cannot be made consistent then return $\mathit{failure}$ for $i = 1$ to $n$ do // root down to leaves: assign, never backtrack $\mathit{assignment}[X_i] \gets$ any consistent value from $D_i$ if there is no consistent value then return $\mathit{failure}$ return $\mathit{assignment}$ ``` **Cutset conditioning.** Most graphs are not trees, but many are _nearly_ trees. Choose a **cycle cutset** $S$ — a set of variables whose removal leaves a tree (deleting $SA$ turns Australia into a tree). For each assignment to $S$ that satisfies its own constraints, prune the neighbors' domains accordingly and solve the residual tree in linear time. With a cutset of size $c$ the total cost is $O(d^c \cdot (n-c) d^2)$: cheap when $c$ is small. Finding the smallest cutset is NP-hard, but good approximations exist, and the technique — **cutset conditioning** — recurs in probabilistic reasoning.[^aima-cutset] A related approach, **tree decomposition**, collapses clusters of variables into "mega-variables" and solves the resulting tree of subproblems; a graph of bounded **tree width** is solvable in polynomial time. ## Local search Backtracking works over _partial_ assignments. Local search takes the opposite tack: start from a _complete_ assignment (every variable set, constraints violated) and repair it one variable at a time. The heuristic is **min-conflicts** — reassign a randomly chosen conflicted variable to the value that violates the fewest constraints.[^aima-local] This connects the CSP frame to [local search](/artificial-intelligence/foundations/intelligent-agents) over complete states: no partial assignments, no backtracking, just hill-climbing on the count of violated constraints. ```algorithm caption: $\textsc{Min-Conflicts}$ — local search for CSPs by conflict repair input: a CSP $\mathit{csp}$; $\mathit{max\text{-}steps}$, the step budget $\mathit{current} \gets$ an initial complete assignment for $\mathit{csp}$ for $i = 1$ to $\mathit{max\text{-}steps}$ do if $\mathit{current}$ is a solution then return $\mathit{current}$ $\mathit{var} \gets$ a randomly chosen conflicted variable $\mathit{value} \gets$ the value $v$ minimizing $\textsc{Conflicts}(\mathit{var}, v, \mathit{current}, \mathit{csp})$ set $\mathit{var} = \mathit{value}$ in $\mathit{current}$ return $\mathit{failure}$ ``` $$ % caption: A min-conflicts step on one column. Each square in the chosen column % shows how many other queens it would conflict with; the queen (dot) sits on a % count-3 square and moves to the count-0 square (accent) at the bottom, breaking % ties at random. Repeating column by column drives total conflicts to zero. \begin{tikzpicture}[>=stealth, font=\footnotesize, sq/.style={draw, minimum size=7mm, inner sep=0pt, font=\scriptsize}, qn/.style={circle, fill=black, inner sep=1.4pt}] \definecolor{acc}{HTML}{2348F2} % board A: a single column with conflict counts; queen on the count-3 cell \node[font=\scriptsize, anchor=south] at (0.35,2.55) {(a) counts}; \node[sq] (a3) at (0,2.1) {3}; \node[sq] (a2) at (0,1.4) {2}; \node[sq] (a1) at (0,0.7) {2}; \node[sq, draw=acc] (a0) at (0,0) {0}; \node[qn] at (-0.28,2.1) {}; \node[font=\scriptsize, anchor=west] at (0.5,2.1) {queen now (3 attacks)}; \node[acc, font=\scriptsize, anchor=west] at (0.5,0) {min = 0: move here}; % board B: after move \begin{scope}[xshift=6cm] \node[font=\scriptsize, anchor=south] at (0.35,2.55) {(b) after}; \node[sq] at (0,2.1) {}; \node[sq] at (0,1.4) {}; \node[sq] at (0,0.7) {}; \node[sq, draw=acc] at (0,0) {}; \node[qn, acc] at (-0.28,0) {}; \node[font=\scriptsize, anchor=west] at (0.5,0) {0 attacks}; \end{scope} \end{tikzpicture} $$ On $n$-queens, ignoring the initial placement, the run time of min-conflicts is roughly _independent of problem size_. It solves the **million-queens** problem in about 50 steps on average. The reason is that solutions are densely scattered through the state space, so from almost anywhere a short greedy descent finds one.[^aima-local] The same method schedules the Hubble Space Telescope, cutting a week's scheduling from three weeks to around ten minutes, and — because it starts from a complete state — it repairs a broken schedule online with few changes, where backtracking would rebuild from scratch. The min-conflicts landscape is dominated by **plateaux**: there can be millions of assignments one conflict short of a solution, all with the same score, and greedy descent stalls among them with no downhill move. Three techniques address this.[^aima-local] **Sideways moves** (plateau search) allow steps to an equal-score neighbor, letting the search drift across a flat until a downhill exit appears. **Tabu search** keeps a short list of recently visited states and forbids returning to them, so the drift does not cycle. **Constraint weighting** attaches a weight $W_i$ to each constraint, all starting at $1$; each step minimizes the total weight of _violated_ constraints, and after each step every currently violated constraint has its weight incremented. Over time the persistently hard constraints accumulate weight, which both tilts the plateau (creating a downhill direction where there was none) and steers effort toward the constraints that actually block a solution — the same idea, under the name clause weighting, drives several strong SAT solvers. Min-conflicts also crosses the line into **constraint optimization**. When constraints are soft — violating one costs points rather than voiding the solution — the objective becomes the total penalty, and every technique from [local search](/artificial-intelligence/foundations/intelligent-agents) transfers directly: hill climbing on the penalty, simulated annealing to escape plateaux, genetic recombination of assignments. A **constraint optimization problem** (COP) is just a CSP whose goal is to minimize violation weight rather than reach zero, and it is how real schedulers encode preferences ("professor R would rather not teach at 8 a.m.") alongside hard rules ("no room hosts two classes at once"). ## SAT solvers and modern CSP systems The CSP machinery in AIMA is the entry point to a research area that scaled to industrial size. The clearest success is **Boolean satisfiability** — the CSP whose variables are true/false and whose constraints are disjunctive **clauses**. SAT is NP-complete (Cook, 1971), yet solvers routinely dispatch instances with millions of variables, and the reason is the algorithm named in this lesson's backtracking section, industrialized. Modern SAT solvers are built on **CDCL** — conflict-driven clause learning (Marques-Silva and Sakallah, 1999, in the GRASP solver; refined by Chaff, Moskewicz et al., 2001). CDCL combines backtracking search, conflict-directed backjumping, and no-good recording, specialized to clauses: when a partial assignment falsifies a clause, the solver analyzes the **implication graph** to derive a new **learned clause** (a no-good) that summarizes the conflict, adds it permanently, and backjumps to the assignment level that clause implicates.[^cdcl] Two engineering ideas make it fast. **Watched literals** (Chaff) detect unit clauses in near-constant time by tracking only two literals per clause instead of scanning all of them, so **unit propagation** — the SAT analog of forward checking — costs almost nothing. **VSIDS**, the variable-state-independent-decaying-sum branching heuristic (also Chaff), scores variables by how often they appear in recent learned clauses and decays old scores, focusing the search on the currently contentious part of the formula — a dynamic cousin of MRV. The learned clauses are the no-goods of the backtracking section, kept across the whole search rather than one subtree. $$ % caption: A CDCL step. A conflict (a falsified clause) is analyzed on the % implication graph to derive a learned clause (no-good); the solver adds it and % backjumps to the level that clause forces, rather than undoing one decision. \begin{tikzpicture}[>=stealth, font=\footnotesize, bx/.style={draw, minimum width=24mm, minimum height=7mm, inner sep=2pt, align=center, font=\scriptsize}] \definecolor{acc}{HTML}{2348F2} \definecolor{red}{HTML}{C0392B} \node[bx] (dec) at (0,0) {decide + propagate}; \node[bx, draw=red, text=red] (conf) at (3.7,0) {clash:\\clause broken}; \node[bx] (learn) at (3.7,-1.7) {analyze +\\learn clause}; \node[bx, draw=acc, text=acc] (jump) at (0,-1.7) {backjump}; \draw[->, thick] (dec) -- (conf); \draw[->, red, thick] (conf) -- (learn); \draw[->, acc, thick] (learn) -- (jump); \draw[->, thick] (jump) -- (dec); \end{tikzpicture} $$ Two solver families sit around CDCL. **Local-search SAT** solvers — **WalkSAT** (Selman, Kautz, Cohen, 1994) — apply the min-conflicts idea directly: from a random complete assignment, pick an unsatisfied clause and flip one of its variables, mixing a greedy min-conflict flip with random noise to escape plateaux.[^walksat] WalkSAT solves large random-3-SAT instances that stall CDCL, though it is incomplete (it never proves unsatisfiability). For hard structured problems, **portfolio** and **parameter-tuned** solvers dominate the annual **SAT Competition**: SATzilla (Xu, Hutter, Hoos, Leyton-Brown, 2008) picks a solver per instance from runtime predictors, and automated configuration tools tune a solver's dozens of heuristics to a problem class. General CSP solving scaled the same way. Finite-domain constraint-programming systems — **Gecode**, **Google OR-Tools CP-SAT**, and **Choco** — implement specialized **propagators** for global constraints like _Alldiff_ (Régin's 1994 matching-based filtering enforces _Alldiff_ far more strongly than pairwise $\ne$) and combine backtracking, MAC-style propagation, and learned no-goods. The **MiniZinc** modeling language (Nethercote et al., 2007) lets a user state a CSP once and dispatch it to any of these back ends, and the **MiniZinc Challenge** benchmarks them yearly. CP-SAT in particular translates constraint models into a CDCL SAT core extended with integer reasoning ("lazy clause generation," Ohrimenko, Stuckey, Codish, 2009), fusing the two lines above.[^cpsolvers] For practice, this means the map-coloring heuristics in this lesson are the conceptual seeds of solvers that plan factory schedules, route delivery fleets, and verify hardware — problems with variables in the millions, solved by machinery that is recognizably backtracking, inference, and no-good learning at scale. ## What the structure bought Exposing a state's internal structure pays off in three distinct ways. The factored form turns constraint violation into _inference_: node and arc consistency and AC-3 delete impossible values without any search. It turns variable order into _heuristics_: MRV, degree, and least-constraining-value are general rules a black-box searcher could never formulate, because it cannot see what "most constrained" means. And it turns the constraint graph into a _complexity map_: trees fall in linear time, cutset conditioning tames the rest, and min-conflicts exploits the density of solutions that structure creates. A generic search sees only states and a goal test; a CSP sees why a state fails, and prunes accordingly. [^aima-commut]: **Russell & Norvig**, _AIMA_, §6.3 — Backtracking Search for CSPs: commutativity of assignments collapsing the $n! \cdot d^n$ tree to $d^n$ leaves. [^aima-bt]: **Russell & Norvig**, _AIMA_, §6.3 — the $\textsc{Backtracking-Search}$ algorithm (Figure 6.5): the three plug-in functions and the standardized CSP representation that needs no domain-specific setup. [^aima-order]: **Russell & Norvig**, _AIMA_, §6.3.1 — Variable and value ordering: minimum-remaining-values, the degree heuristic as a tie-breaker, and the fail-first / fail-last logic of least-constraining-value. [^aima-mac]: **Russell & Norvig**, _AIMA_, §6.3.2 — Interleaving search and inference: forward checking, and MAC seeding AC-3 with the assigned variable's arcs, strictly stronger than forward checking. [^aima-back]: **Russell & Norvig**, _AIMA_, §6.3.3 — Intelligent backtracking: conflict sets, backjumping, conflict-directed backjumping, and constraint learning of no-goods. [^aima-struct]: **Russell & Norvig**, _AIMA_, §6.5 — The Structure of Problems: independent subproblems via connected components and the $O(d^c \cdot n/c)$ decomposition. [^aima-cutset]: **Russell & Norvig**, _AIMA_, §6.5 — cutset conditioning and tree decomposition: the cycle cutset, the $O(d^c (n-c) d^2)$ bound, and bounded tree width giving polynomial time. [^aima-local]: **Russell & Norvig**, _AIMA_, §6.4 — Local Search for CSPs: the $\textsc{Min-Conflicts}$ algorithm (Figure 6.8), the million-queens result, Hubble telescope scheduling, and the plateau techniques (sideways moves, tabu search, constraint weighting) and constraint optimization. [^cdcl]: **J. P. Marques-Silva & K. A. Sakallah**, "GRASP: A Search Algorithm for Propositional Satisfiability," _IEEE Trans. Computers_ 48(5), 1999 — conflict-driven clause learning and non-chronological backtracking for SAT. **M. Moskewicz, C. Madigan, Y. Zhao, L. Zhang, S. Malik**, "Chaff: Engineering an Efficient SAT Solver," _DAC_ 2001 — watched literals and the VSIDS branching heuristic. [^walksat]: **B. Selman, H. Kautz, B. Cohen**, "Noise Strategies for Improving Local Search," _AAAI_ 1994 — the WalkSAT local-search satisfiability procedure (min-conflicts flips with random noise). **S. A. Cook**, "The Complexity of Theorem-Proving Procedures," _STOC_ 1971 — NP-completeness of SAT. [^cpsolvers]: **J.-C. Régin**, "A Filtering Algorithm for Constraints of Difference in CSPs," _AAAI_ 1994 — matching-based _Alldiff_ propagation. **N. Nethercote et al.**, "MiniZinc: Towards a Standard CP Modelling Language," _CP_ 2007. **O. Ohrimenko, P. Stuckey, M. Codish**, "Propagation via Lazy Clause Generation," _Constraints_ 14(3), 2009 — the SAT/CP fusion behind CP-SAT. **L. Xu, F. Hutter, H. Hoos, K. Leyton-Brown**, "SATzilla: Portfolio-based Algorithm Selection for SAT," _JAIR_ 32, 2008.