Module cdcl 

A conflict-driven clause-learning (CDCL) SAT core — the modern competition-grade engine, built to the lineage that made SAT practical: two-watched-literal unit propagation (Moskewicz et al., Chaff, 2001), first-UIP conflict analysis with learned clauses and non-chronological backtracking (Marques-Silva & Sakallah, GRASP, 1996), VSIDS-style activity decisions, and Luby restarts (Luby et al., 1993). The clean reference implementation it follows is Eén & Sörensson’s MiniSat (2003).

This module is the propositional substrate of a DPLL(T) engine (Nieuwenhuis, Oliveras & Tinelli, JACM 2006): theory propagators (an AllDifferent GAC filter for grid categories, EUF, LIA, …) plug in through Theory, and every learned clause is a resolvent the solver can log as a DRAT/LRAT proof step (Wetzler/Heule/Hunt, 2014; Cruz-Filipe et al., 2017) for a downstream linear checker.

It is deliberately self-contained and value-typed (Var = u32, Lit a packed sign+index) so it can be exercised against a brute-force oracle in isolation before it is wired to the grid encoder — a SAT core is only as good as its cross-checks.

Structs

LearnedClause

A learned clause logged for proof reconstruction. Each is a resolvent derivable from the formula by reverse unit propagation — the unit of a DRAT/LRAT proof.

Lit

A literal: a variable plus a sign, packed as var << 1 | negated. Packing keeps the watch lists and the trail cache-dense, the way every fast solver stores them.

Solver

The CDCL solver.

Enums

BudgetedResult

The outcome of a conflict-budgeted solve: a verdict, or budget exhaustion (with the learned clauses left available for symmetric amplification).

RestartMode

The restart heuristic. Glucose’s dynamic LBD policy restarts when recent learned-clause quality (literal-block distance) degrades relative to the global average, and blocks a restart when the trail is unusually long — a sign the search is closing in on a model. Luby is the classic universal sequence (Luby et al., 1993). Adaptive alternates the two in geometrically growing phases (the CaDiCaL/Kissat “stabilizing / non-stabilizing” idea): aggressive Glucose restarts to EXPLORE, then calm Luby restarts to let phase-saving EXPLOIT and dig toward a model — capturing the strength of each and avoiding the per-instance losses of either alone. The choice is a pure search-ORDER heuristic: it never changes a verdict.

SolveResult

The verdict of Solver::solve.

Traits

Theory

A theory propagator (the DPLL(T) seam). The SAT core calls Theory::propagate at each fixpoint of Boolean propagation; a theory returns a fresh clause to add (an explanation/conflict) or None if it has nothing to say. AllDifferent GAC, EUF, and LIA all implement this without the core knowing the theory.

Type Aliases

Var

A propositional variable: an index 0..num_vars.