SAT Solving, in depth: CNF and Tseitin encodings, DPLL to CDCL, 1-UIP clause learning with a traced example, and driving real solvers

CNF and the DIMACS format

Solvers take formulas in conjunctive normal form: an AND of clauses, each clause an OR of literals, each literal a variable or its negation. A clause is satisfied when at least one literal is true; the formula is satisfied when every clause is. The exchange format is DIMACS CNF: a header p cnf <variables> <clauses>, then one clause per line as signed integers terminated by 0.

c (x1 or x4) and (x3 or x5) and (not x4 or not x5 or x6) ...
p cnf 8 6
1 4 0
3 5 0
-4 -5 6 0
-5 7 0
-6 -7 0
2 8 0

That six-clause formula is the worked example used throughout. By convention, competition solvers print s SATISFIABLE with a v line of literals, or s UNSATISFIABLE, and exit with status 10 or 20 respectively.

Encoding real problems

Most problems are not born in CNF. Two encodings cover the bulk of practical work.

Tseitin transformation. Naively distributing OR over AND can blow a formula up exponentially. Tseitin's method instead introduces a fresh variable for each subformula and adds clauses stating that the variable equals the subformula. For g = a AND b that is (¬g ∨ a) (¬g ∨ b) (g ∨ ¬a ∨ ¬b). The result is linear in size and equisatisfiable: satisfiable exactly when the original is, though not logically equivalent.

Cardinality constraints. "Exactly one of these" appears everywhere: one version per package, one colour per vertex, one slot per job. At-least-one is a single clause. At-most-one can be pairwise, adding (¬a ∨ ¬b) for every pair, which is quadratic, or a sequential counter with auxiliary variables, which is linear. Pairwise is fine below about ten literals.

def at_most_one_pairwise(lits):
    return [[-a, -b] for i, a in enumerate(lits) for b in lits[i + 1:]]

def at_most_one_sequential(lits, next_var):
    """Sinz sequential counter: s_i is true if some of lits[0..i] is true."""
    n, clauses = len(lits), []
    s = list(range(next_var, next_var + n - 1))
    for i in range(n - 1):
        clauses.append([-lits[i], s[i]])                 # x_i implies s_i
        if i > 0:
            clauses.append([-s[i - 1], s[i]])            # s_{i-1} implies s_i
            clauses.append([-lits[i], -s[i - 1]])        # x_i forbids an earlier true
    clauses.append([-lits[n - 1], -s[n - 2]])
    return clauses, next_var + n - 1

# Dependency resolution: app needs lib >= 2; lib 1, 2, 3 are variables 1, 2, 3; app is 4.
app, lib = 4, [1, 2, 3]
clauses = [[app], [-app, 2, 3]] + at_most_one_pairwise(lib)

The dependency encoding is the one package managers use: "app is installed" is a unit clause, "app requires lib 2 or lib 3" is an implication, and at-most-one forbids two versions of the same package. Optimisation goals, such as preferring newer versions, are then handled by repeated solving or a MaxSAT solver.

DPLL: backtracking plus unit propagation

The DPLL procedure (Davis, Putnam, Logemann and Loveland, early 1960s) is backtracking search plus one powerful inference rule. Unit propagation: if every literal of a clause is false except one unassigned literal, that literal must be true. Propagation repeats until nothing changes or some clause has every literal false, a conflict.

DPLL picks an unassigned variable, assigns it, propagates, and on conflict undoes the most recent decision and tries the other value. It is a backtracking search in the strict sense, and its weakness is that it forgets why a conflict happened. The same bad combination of two early decisions can be rediscovered under thousands of later decisions that had nothing to do with it.

CDCL: learning from conflicts

CDCL, introduced by GRASP in 1996 and made fast by Chaff in 2001, fixes that by analysing each conflict. Every assignment records its decision level (how many decisions were on the stack) and its reason (the clause that propagated it, or none for a decision). Together these form an implication graph. On conflict the solver resolves the conflicting clause backwards with reason clauses until exactly one literal from the current level remains. That literal is the first unique implication point (1-UIP), and the resulting clause is learned. The solver then backjumps to the second-highest level in the learned clause, where it becomes unit and propagates immediately.

def cdcl(n, clauses, trace=False):
    clauses = [list(c) for c in clauses]
    assign, trail = {}, []                # var -> (value, level, reason index); literal order

    def val(l):
        a = assign.get(abs(l))
        return None if a is None else (a[0] == (l > 0))

    def enqueue(l, lvl, reason):
        assign[abs(l)] = (l > 0, lvl, reason)
        trail.append(l)

    def propagate(lvl):                   # naive scan; real solvers use watched literals
        changed = True
        while changed:
            changed = False
            for i, c in enumerate(clauses):
                vals = [val(l) for l in c]
                if True in vals:
                    continue
                free = [l for l, v in zip(c, vals) if v is None]
                if not free:
                    return i              # conflict clause index
                if len(free) == 1:
                    enqueue(free[0], lvl, i)
                    changed = True
                    if trace:
                        print(f"  L{lvl} propagate {free[0]:+d} by clause {i} {c}")
        return None

    def analyze(ci, lvl):                 # resolve back to the first UIP
        learned = set(clauses[ci])
        while sum(assign[abs(l)][1] == lvl for l in learned) > 1:
            last = next(l for l in reversed(trail) if -l in learned)
            learned = (learned | set(clauses[assign[abs(last)][2]])) - {last, -last}
        back = max((assign[abs(l)][1] for l in learned if assign[abs(l)][1] != lvl), default=0)
        return sorted(learned, key=abs), back

    lvl = 0
    if propagate(0) is not None:
        return None                       # UNSAT without any decision
    while True:
        free = [v for v in range(1, n + 1) if v not in assign]
        if not free:
            return {v: assign[v][0] for v in assign}
        lvl += 1
        enqueue(-free[0], lvl, None)      # decide: lowest variable, false first
        if trace:
            print(f"L{lvl} decide {-free[0]:+d}")
        while (ci := propagate(lvl)) is not None:
            if lvl == 0:
                return None               # conflict with no decisions left: UNSAT
            learned, back = analyze(ci, lvl)
            if trace:
                print(f"  conflict in clause {ci} {clauses[ci]} -> learn {learned}, backjump to L{back}")
            while trail and assign[abs(trail[-1])][1] > back:
                del assign[abs(trail.pop())]
            clauses.append(learned)
            lvl = back

This version was checked against brute-force enumeration on 3,000 random formulas of up to nine variables before publication. It is deliberately naive in propagation and decision order so the learning logic stays visible.

Worked example: learning a clause and backjumping

Run the solver with trace=True on the six-clause DIMACS file above. Decisions pick the lowest free variable and try false first. The trace:

L1 decide -1
  L1 propagate +4 by clause 0 [1, 4]
L2 decide -2
  L2 propagate +8 by clause 5 [2, 8]
L3 decide -3
  L3 propagate +5 by clause 1 [3, 5]
  L3 propagate +6 by clause 2 [-4, -5, 6]
  L3 propagate +7 by clause 3 [-5, 7]
  conflict in clause 4 [-6, -7] -> learn [-4, -5], backjump to L1
  L1 propagate -5 by clause 6 [-4, -5]
  L1 propagate +3 by clause 1 [3, 5]
L2 decide -2
  L2 propagate +8 by clause 5 [2, 8]
L3 decide -6
L4 decide -7
# returned model: x1=0 x2=0 x3=1 x4=1 x5=0 x6=0 x7=0 x8=1

Analysis starts from the conflict clause (¬x6 ∨ ¬x7). The most recent assignment in it is x7, whose reason is (¬x5 ∨ x7); resolving on x7 gives (¬x5 ∨ ¬x6). Next is x6, reason (¬x4 ∨ ¬x5 ∨ x6); resolving gives (¬x4 ∨ ¬x5). Only x5 is now at level 3, so this is the 1-UIP clause. Its other literal, x4, sits at level 1, so the solver discards levels 3 and 2 together. Plain DPLL would only have flipped x3 and kept the x2 decision, which was irrelevant. At level 1 the learned clause is unit, forcing x5 false, which in turn forces x3 true, and the search finishes without another conflict.

What makes production solvers fast

The naive solver rescans every clause on every assignment. Production solvers are fast because of the following ideas, most of which come from Chaff, MiniSat and Glucose.

# Two-watched-literal propagation, in outline
on assigning literal L true:
    for clause C in watches[-L]:            # C was watching the now-false literal -L
        if C's other watch is true: continue
        if some literal K in C, not watched, is not false:
            move the watch from -L to K      # clause is still fine
        elif other watch is unassigned:
            enqueue(other watch, reason=C)   # unit
        else:
            return conflict(C)

Driving a solver from code

In practice you rarely write the solver; you write the encoding and drive a mature one. The simplest integration is the DIMACS file plus the exit code, which works with any competition-style solver binary such as Kissat or CaDiCaL:

import subprocess, tempfile

def solve_dimacs(n_vars, clauses, solver="kissat", timeout_s=60):
    with tempfile.NamedTemporaryFile("w", suffix=".cnf", delete=False) as f:
        f.write(f"p cnf {n_vars} {len(clauses)}\n")
        for cl in clauses:
            f.write(" ".join(map(str, cl)) + " 0\n")
    r = subprocess.run([solver, f.name], capture_output=True, text=True, timeout=timeout_s)
    if r.returncode == 20:
        return None                                    # UNSAT
    if r.returncode != 10:
        raise RuntimeError(f"solver returned {r.returncode}: unknown or error")
    model = []
    for line in r.stdout.splitlines():
        if line.startswith("v "):
            model += [int(t) for t in line[2:].split() if t != "0"]
    return {abs(l): l > 0 for l in model}

For many related queries, use incremental solving: keep one solver instance, add clauses as you go, and pass temporary assumptions per call. The IPASIR interface standardises this with ipasir_add, ipasir_assume, ipasir_solve and ipasir_failed; the failed assumptions after an UNSAT answer form a core that explains which requested choices conflict. In the dependency example, assuming each requested package as a literal tells the user exactly which requests cannot coexist.

When an answer is UNSAT and stakes are high, ask the solver for a proof. Modern solvers can emit a DRAT proof that an independent checker such as drat-trim validates, so you do not have to trust solver code that is tens of thousands of lines long.

Failure modes

• Encoding blow-up. Pairwise at-most-one over 1,000 literals is about half a million clauses. Use counters or let a solver with native cardinality support handle it.
• Symmetry. Pigeonhole-style problems, such as fitting n+1 items into n interchangeable slots, are exponentially hard for resolution-based solvers. Add symmetry-breaking clauses, such as ordering identical slots.
• Treating timeout as UNSAT. A timeout is "unknown". Code that maps it to "no solution" ships wrong answers.
• Arithmetic in pure SAT. Bit-blasted multipliers are hard. For heavy integer arithmetic, consider an SMT solver or an ILP formulation instead.
• Performance variance. Shuffling clause order or changing a seed can change runtime by orders of magnitude on hard instances. Benchmark with several seeds and report the spread.

What to do next

1. Type in the solver above, reproduce the trace, then add a VSIDS-style activity score and compare conflict counts on random 3-SAT near 4.26 clauses per variable.
2. Replace the naive propagation with two watched literals and measure the speed-up on 200 variables.
3. Encode a 9×9 Sudoku with exactly-one constraints and compare it with the hand-written Sudoku backtracking solver.
4. Encode k-colouring of a graph and check it against the heuristics in graph colouring.
5. Install Kissat or CaDiCaL, solve a competition instance through the subprocess wrapper, and verify an UNSAT result with drat-trim.
6. Model one real dependency-resolution or scheduling problem from your work as CNF and measure where the time goes.