Backtracking, N-Queens & SAT Solvers theory

Combinatorial search is the process of finding one or more configurations of discrete decision variables that satisfy a specified set of constraints.



1. State Space Tree Formalism:

A state space tree organizes combinatorial exploration hierarchically:

- Root: The uninstantiated problem state with zero variable assignments;

- Level k Nodes: Represent partial candidate solutions where variables (x₁, x₂, ..., x_k) have been assigned values from their respective domains;

- Leaves: Represent either complete candidate solutions or dead-end states where no further legal assignments exist.



2. Naive Brute-Force vs. Systematic Backtracking:

In naive brute-force search, every leaf of depth N is generated and checked against problem constraints, incurring an intractable complexity of O(b^N) where b is the domain branching factor. Backtracking systematically avoids this exponential explosion by evaluating a bounding predicate P(x₁, x₂, ..., x_k) at interior nodes:

- If P(x₁, ..., x_k) evaluates to False, the partial solution is provably invalid. Because no extension of an invalid prefix can satisfy monotonic constraints, the entire subtree rooted at that node is immediately pruned;

- The search terminates the current branch and backtracks to the parent node, advancing to the next alternative in the domain of x_k.



3. Quantitative Pruning Impact:

In the 8-Queens problem, the unrestricted state space contains 4.426 × 10⁹ configurations. Enforcing row uniqueness reduces this to 8⁸ = 16.78 × 10⁶. Backtracking with diagonal constraint checking prunes over 99.98% of the tree, visiting only 2,057 nodes to discover all 92 valid solutions.

The N-Queens puzzle requires placing N queens on an N × N chessboard such that no two queens attack each other along rows, columns, or diagonals.



1. Coordinate Representation & Permutations:

Let queen coordinates be denoted as (r, c), where r ∈ [0..N-1] is the row index and c ∈ [0..N-1] is the column index:

- Row Invariant: Because queens attack horizontally, each row must contain exactly one queen. We represent the board as a vector Q = [q₀, q₁, ..., q_{N-1}], where q_r = c indicates a queen placed at (r, c);

- Column Invariant: Because queens attack vertically, no two queens can share a column: q_{r₁} ≠ q_{r₂} for all r₁ ≠ r₂. This constrains Q to be a permutation of {0, 1, ..., N-1}, reducing the search space to N!.



2. Diagonal Conflict Geometry:

Two queens at (r₁, c₁) and (r₂, c₂) attack diagonally if the absolute slope of the connecting segment equals 1:

|r₁ - r₂| = |c₁ - c₂|

This absolute value condition separates into two orthogonal families of diagonals:

- Major / Left Diagonals (\\nwarrow \\searrow): Points along any left diagonal share an identical difference: r - c = const. Because r, c ∈ [0..N-1], the difference spans [-(N-1), N-1]. Adding the offset N - 1 normalizes indices to [0, 2N - 2] (total 2N - 1 diagonals);

- Minor / Right Diagonals (\\nearrow \\swarrow): Points along any right diagonal share an identical sum: r + c = const. The sum spans [0, 2N - 2] (total 2N - 1 diagonals).



3. Conflict Checking Invariant:

A candidate placement at row r and column c is safe if and only if:

column c is unoccupied AND left diagonal (r - c + N - 1) is unoccupied AND right diagonal (r + c) is unoccupied.

In 1991, Rich Burroughs formulated the Bitmask N-Queens algorithm, replacing array lookups with single-cycle CPU bitwise logic.



1. Bitmask Representation:

Instead of allocating boolean arrays, board constraints are stored in three unsigned integer machine registers:

- cols: Bit c is 1 if column c is occupied;

- diag_left: Bit d is 1 if the left diagonal passing through the current row is occupied;

- diag_right: Bit d is 1 if the right diagonal passing through the current row is occupied.



2. Bitwise Logic Pipeline per Row:

- Step 1 (Collision Mask): occupied = cols | diag_left | diag_right. Bitwise OR identifies all columns under attack in the current row;

- Step 2 (Free Squares): available = (~occupied) & full_mask, where full_mask = (1 << N) - 1. Inverting flips safe columns to 1, and masking discards unused high bits;

- Step 3 (Two's Complement Isolation): bit = available & (-available). In two's complement arithmetic, -x = (~x) + 1. Adding 1 propagates carries through trailing zeros, causing the bitwise AND to isolate the lowest 1-bit in a single clock cycle without any loops or branches;

- Step 4 (Bit Clearing): available &= (available - 1), efficiently removing the selected bit;

- Step 5 (State Shift to Next Row): Recurse to row r + 1 with: cols | bit, (diag_left | bit) << 1, and (diag_right | bit) >> 1. The bitwise left shift perfectly tracks left diagonals descending to the next row, while the right shift tracks right diagonals!



3. Microarchitectural Advantages:

- Array backtracking suffers from L1 cache line accesses, index bounds checking, and high branch misprediction rates;

- Bitmask backtracking operates entirely within high-speed CPU registers, executing in ~4 clock cycles per node and achieving 15x to 25x execution speedups.

Boolean Satisfiability (SAT) is the central foundational problem in computational complexity theory and mathematical logic.



1. Definitions & CNF Syntax:

- Boolean Variable: x_i ∈ {0, 1} (False, True);

- Literal: A variable x_i or its negation ¬x_i;

- Clause: A disjunction (OR) of literals: C_j = (l₁ ∨ l₂ ∨ ... ∨ l_k);

- Conjunctive Normal Form (CNF): A conjunction (AND) of clauses: Φ = C₁ ∧ C₂ ∧ ... ∧ C_m.

A formula Φ is satisfiable if there exists a truth assignment to all variables such that every clause evaluates to True.



2. The Cook-Levin Theorem (1971):

Stephen Cook and Leonid Levin independently proved that SAT is NP-complete:

- Any problem whose solution can be verified in polynomial time (class NP) can be transformed in polynomial time into an equivalent CNF formula;

- If a polynomial-time algorithm is ever discovered for SAT, then P = NP, and all thousands of known NP-complete problems can be solved in polynomial time.



3. Encoding N-Queens as a SAT Problem:

The N-Queens puzzle is encoded into CNF using N² boolean variables X_{r,c} (True iff queen at row r, col c):

- At least one queen per row: ⋁_{c=0}^{N-1} X_{r,c} for each row r (N clauses);

- At most one queen per row: ¬X_{r,c₁} ∨ ¬X_{r,c₂} for all c₁ < c₂ (N · (N(N-1)/2) clauses);

- At most one queen per column: ¬X_{r₁,c} ∨ ¬X_{r₂,c} for all r₁ < r₂;

- At most one queen per diagonal: pairwise exclusion clauses for all points sharing identical diagonals.

Modern SAT solvers routinely solve this CNF encoding for N = 1000 in seconds!

The DPLL algorithm (1962) transformed propositional satisfiability from theoretical logic into practical computation.



1. The Three Algorithmic Rules of DPLL:

- Rule 1: Boolean Constraint Propagation (BCP) / Unit Propagation:

If a clause contains only one unassigned literal and all other literals in that clause are False (a unit clause), that remaining literal MUST be assigned True to satisfy the clause. Propagating this forced assignment simplifies other clauses, frequently creating new unit clauses in an automated deductive cascade;

- Rule 2: Pure Literal Elimination:

If a variable appears in unresolved clauses with only one polarity (e.g., only as x_i, never as ¬x_i), assigning it True satisfies all clauses containing it without threatening any other clause;

- Rule 3: Branching Decision:

When no unit or pure literals remain, the algorithm selects an unassigned variable x, branches on x = True, and recursively evaluates. If that branch encounters a conflict (an empty falsified clause), it backtracks and assigns x = False.



2. Unit Propagation Mechanics:

Consider the clause set: { (x₁ ∨ x₂), (¬x₁ ∨ x₃), (¬x₃ ∨ ¬x₂) }.

- Assign decision x₁ = False;

- In clause (x₁ ∨ x₂), x₁ is False, leaving x₂ as a unit literal. BCP forces x₂ = True;

- Now evaluate (¬x₃ ∨ ¬x₂): since x₂ is True, ¬x₂ is False, leaving ¬x₃ as a unit literal. BCP forces x₃ = False;

- Now evaluate (¬x₁ ∨ x₃): ¬x₁ is True, satisfying the clause.

All clauses are satisfied without further branching!

Conflict-Driven Clause Learning (CDCL), pioneered in GRASP (1996) and Chaff (2001), powers modern industrial SAT solvers.



1. Architectural Limitations of Classic DPLL:

Classic DPLL backtracks chronologically to the most recent decision level. When a conflict occurs due to variable interactions decided 50 levels earlier, DPLL will exhaustively explore all 2⁵⁰ combinations of intervening irrelevant variables before discovering the conflict root, causing exponential thrashing.



2. The Implication Graph & Conflict Analysis:

CDCL records every variable assignment, its decision level, and its antecedent reason clause in a Directed Acyclic Graph (DAG):

- Decisions are root nodes;

- Unit-propagated variables have directed edges from the literals in their antecedent clause;

- When a clause is falsified (all literals become False), a conflict node is created.



3. 1UIP (First Unique Implication Point):

The solver traverses backward from the conflict node along the implication graph, applying boolean resolution between clauses:

- An Implication Point is a node at the current decision level through which all paths from the decision to the conflict must pass;

- The First UIP (1UIP) is the implication point closest to the conflict;

- Resolving up to the 1UIP derives a learned asserting clause containing exactly one literal from the current decision level and literals from earlier decision levels.



4. Non-Chronological Backjumping:

Instead of popping one decision level, CDCL inspects the learned clause, identifies the second-highest decision level among its literals, and jumps directly back to that level. The learned clause immediately acts as a unit clause at that earlier level, permanently preventing the solver from ever entering that conflict space again!

Modern SAT solvers achieve extraordinary microarchitectural throughput through Two-Watched-Literals (2WL) and VSIDS heuristics.



1. The Two-Watched-Literals (2WL) Innovation (Chaff, 2001):

In naive DPLL, every time a variable is assigned, every clause containing that variable must be updated, costing O(C) operations per assignment and requiring complete restoration upon backtracking:

- The 2WL Invariant: In each clause, maintain pointers to exactly two unassigned (or True) literals;

- So long as these two watched literals do not become False, the clause cannot possibly be unit and cannot possibly be falsified!

- When variable x is assigned False, the solver visits ONLY clauses watching ¬x. For each, it scans the clause for another non-false literal to watch;

- If an alternate non-false literal is found, the watcher pointer is moved. If only one non-false literal remains, Unit Propagation is triggered. If no non-false literal exists, a Conflict is flagged;

- Zero-Cost Backtracking: When unassigning variables during backjumping, watcher pointers do NOT need to be modified at all! Backtracking is instantaneous (O(1)).



2. VSIDS (Variable State Independent Decaying Sum):

Branching on arbitrary variables leads to erratic search times. VSIDS prioritizes variables based on conflict participation:

- Each variable has an activity score initialized to 0;

- Whenever a learned clause is derived, the score of every literal in the conflict graph is incremented;

- Periodically, all scores are multiplied by a decay factor (e.g., 0.95);

- VSIDS selects the unassigned variable with the highest activity score, dynamically focusing the solver's deductive power on the hardest local subproblem.