SAT Solving

Why SAT Solving Matters

A feature configuration might require that enabling an extension also enables its runtime, that two drivers cannot be installed together, and that at least one storage backend is selected. Each individual rule is simple; deciding whether all the rules can hold together can require many interacting choices. Boolean satisfiability, or SAT, asks whether there is any assignment of true and false values that satisfies every rule.

SAT also provides a useful way to search for mistakes. Encode a circuit or a bounded program execution together with the condition “the expected property fails.” A satisfying assignment describes a counterexample within that encoding. An UNSAT result means no such assignment exists for the encoded instance; a finite execution bound does not establish correctness for every possible execution length.

This lesson extends recursive constraint search to propositional formulas. First build DPLL, with unit propagation, pure-literal choices, and chronological backtracking. Then retain explanations for implications and turn a conflict into a learned clause: CDCL, with first-UIP analysis, nonchronological backjumping, a simplified VSIDS activity rule, and geometric restarts. Both executable modes share a two-watched-literal propagation engine, so the connection between logical reasoning and state management remains visible.

Core Concepts and Terminology

Let $x_1,\ldots,x_n$ be Boolean variables. A literal is $x_i$ or its negation $\neg x_i$. A clause is a disjunction of literals, and a formula in conjunctive normal form, or CNF, is a conjunction of clauses:

$$F=\bigwedge_{j=0}^{m-1}C_j,\qquad C_j=\bigvee_{\ell\in C_j}\ell.$$

Every clause must have at least one true literal. An unassigned variable is distinct from false. Under a partial assignment, a clause is satisfied if some literal is true, conflicting if every literal is false, unit if exactly one literal is unassigned and all others are false, and otherwise unresolved. A branch conflict disproves that partial assignment; it does not by itself prove that the whole formula is UNSAT.

The programs encode $x_i$ by integer $i$ and $\neg x_i$ by $-i$. For example, [-1,2] represents $\neg x_1\lor x_2$. Internally, assignment values are $1$ for true, $-1$ for false, and $0$ for unassigned; returned models use ordinary bits, $1$ for true and $0$ for false. Literal zero is invalid in this API. This is a list-of-clauses interface, rather than a DIMACS parser with zero-terminated lines.

Two boundary cases matter: the empty conjunction [] is true, while a formula containing the empty clause, such as [[]], is false. A clause containing both $x_i$ and $\neg x_i$ is a tautology and can be discarded. Repeating the same literal does not create a second logical alternative: [1,1] is a unit clause after duplicate removal.

A trail records assigned literals in order. Decisions start new decision levels; unit implications inherit the current level and record the clause that forced them. Level zero contains assignments made before any decision. A saved trail boundary lets the solver undo a whole level, including its implications.

The tree uses the six-clause worked formula introduced below. The true branch of $x_1$ forces $x_2$ and immediately conflicts; the false branch is satisfiable. Both branches begin from the same root assignment, so an implication from the failed branch must not leak into its sibling.

How SAT Solving Works, Step by Step

Begin by normalizing the clauses, attaching their watches, and enqueueing every original unit clause with its clause ID as the reason. An empty clause or incompatible original units establishes UNSAT immediately. Otherwise, process the trail as a queue until propagation reaches a fixed point or finds a conflict.

Two-watched-literal propagation. For each nonunit clause, store two distinct positions and register the clause in the watch list of each watched literal. A unit clause has both stored positions equal to zero but is registered only once. In these implementations the lists are indexed by the literal actually watched. When assigned literal $p$ is dequeued, inspect the list for $\neg p$, because that literal just became false.

For each affected clause:

1. If its other watched literal is true, leave both watches where they are. The clause is satisfied even though one watch is false.
2. Otherwise, look for a nonwatched literal that is not false: true or unassigned are both valid replacements. Move the false watch there, remove the clause from the old bucket by swapping in the last entry, and append it to the new bucket. Reprocess the same bucket index after removal so the swapped-in entry is not skipped.
3. If no replacement exists and the other watch is unassigned, enqueue that other literal with this clause as its reason.
4. If no replacement exists and the other watch is false, return this clause ID as a conflict.

Moving watches changes an index structure, not the logical formula. Watch positions survive backtracking. The assignment trail, levels, reasons, and propagation head must be rolled back together.

DPLL mode. After each propagation fixed point, scan only unsatisfied clauses for pure unassigned variables. Choose the lowest-ID pure variable, assign its satisfying polarity, and propagate again. Once no pure literal remains, return SAT if all clauses are satisfied. Otherwise choose the lowest-ID unassigned variable, try true first, and recurse. Save a trail boundary before the decision; on return, undo the branch even if it succeeded. If the true branch fails, try false. If both fail, return failure to the caller. The satisfying model is copied before successful assignments are undone.

Unit propagation is a logical consequence of the formula and the current trail. A pure-literal assignment is a safe choice, rather than necessarily a logical consequence. For $x_1\lor x_2$, choosing pure $x_1$ true preserves the existence of a solution, but the model with $x_1$ false and $x_2$ true also existed. Therefore this rule needs different treatment in model counting.

CDCL mode. Omit pure-literal choices from this engine so every nondecision assignment has a clause reason. On a nonroot conflict, start with the falsified clause. While it contains more than one literal assigned at the current decision level, take its latest such variable on the trail and resolve with that variable's reason clause. Stop when exactly one current-level literal remains. This is a first-UIP learned clause. Keep that literal first, and place a literal from the greatest remaining level second, if one exists.

The backjump target is the highest level of the learned clause's other literals, or zero for a unit learned clause. Undo every higher level, attach the learned clause, and enqueue its first literal with the new clause ID as the reason. Its other literals are still false, so the clause is asserting. The implementation keeps level-zero literals in resolvents rather than silently dropping them.

The CDCL branching score is a transparent VSIDS-style variant, initialized to zero. At each analyzed conflict, halve every variable activity and add one to each variable appearing in the starting conflict or a reason used in resolution:

$$a_v\leftarrow \tfrac12a_v+\begin{cases}1,&v\text{ participates in the analysis},\\0,&\text{otherwise}.\end{cases}$$

Choose the unassigned variable with greatest activity, breaking ties by lowest ID, and choose its true polarity. The code scans scores directly; it has no heap, phase saving, or learned-clause deletion. This is a teaching implementation of decaying conflict activity, not a reproduction of one particular solver's tuning.

After a conflict-free propagation pass, check SAT first. If clauses remain unresolved and the restart conflict budget has been reached at a nonzero level, backtrack to zero while preserving learned clauses and scores. Reset the conflicts-since-restart count and double the next budget. The sample uses budgets $1,2,4,\ldots$ so the effect is visible; the default Python/C++ argument is two. The flowchart shows this CDCL loop; DPLL's alternative continuation is the two-branch recursion described above.

flowchart TD
    A["Normalize clauses; attach watches; enqueue root units"] --> B["Propagate queued assignments"]
    B --> C{"Conflicting clause?"}
    C -->|Yes| D{"Decision level zero?"}
    D -->|Yes| E["Return UNSAT; clear assignment state"]
    D -->|No| F["Resolve to first UIP; update activities"]
    F --> G["Backjump; attach learned clause; assert its first literal"]
    G --> B
    C -->|No| H{"Every clause satisfied?"}
    H -->|Yes| I["Copy model; return SAT; clear assignment state"]
    H -->|No| J{"Restart due at nonzero level?"}
    J -->|Yes| K["Backtrack to zero; retain learning; double budget"]
    K --> B
    J -->|No| L["Choose highest-activity unassigned variable"]
    L --> M["Start decision level; enqueue positive literal"]
    M --> B

Worked Example with a Full Trace

Use four variables and these six clauses, preserving the listed literal order and clause IDs:

Every variable initially occurs in both polarities, and there are no units. Every clause is binary, so its two watches remain on its two literal positions throughout this run. Watch movement is illustrated separately by the watch move sample.

DPLL. Entry 1 has trail [], level zero, and queue head zero. Decide literal 1 at level one, saving boundary zero. Entry 2 dequeues 1, so it scans clauses watching -1. Clause 0 enqueues 2, with reason 0. Clause 1 now has both literals false and returns conflict before queued 2 is processed. The trail is [1,2] and head is one.

Undo to the saved boundary: pop 2, then 1; clear both reasons and levels and reset head to zero. Decide -1 at a fresh level one. Entry 3 processes that decision and the implications as follows. The implication total includes 2 from the failed branch and never decreases during undo.

All clauses are satisfied. Copy model $[0,0,1,1]$, undo the successful level, and return SAT. Totals: three recursive entries, two decision assignments, four implications, no pure choices, and one conflict.

CDCL. Entries 1 and 2 make the same initial decision and encounter the same conflict. Resolve clause 1 with the reason for 2, clause 0:

$$\frac{(\neg x_1\lor\neg x_2)\qquad(\neg x_1\lor x_2)}{\neg x_1}.$$

The learned clause [-1] has one current-level literal, so it is a first-UIP clause and its backjump target is zero. Give variables 1 and 2 activity one, undo [1,2], attach learned clause 6, and enqueue -1 at level zero with reason 6. Entry 3 then enqueues -2, 3, and 4 for reasons 2, 3, and 4. The same model satisfies all clauses. CDCL uses one decision and five implications: the failed-branch 2, the learned assertion -1, and the three final implications. It learns one clause and performs no restart because it reaches SAT first.

A second small example makes backjumping and restarting visible. The restart fixture has clauses [-1,-3,4], [-1,-3,-4], [3,5,6], with six variables and restart budget one. With initially tied scores, CDCL decides 1, then the irrelevant variable 2, then 3, at levels 1, 2, and 3. The first clause forces 4; the second conflicts. Resolving on $x_4$ learns $\neg x_3\lor\neg x_1$, stored as [-3,-1]. Backjump to level 1, skipping level 2, and assert -3 there. The remaining clause needs $x_5\lor x_6$, so the formula is still unresolved after propagation.

The budget now triggers a restart to zero. Keep [-3,-1] and the activities of variables 1, 3, and 4. Decide 1 again, which propagates -3 through the learned clause. Decisions 4, 2, and 5 then complete a model. This run has ten loop entries, seven decisions, three implications, one learned clause, and one restart. The irrelevant variable can still be selected by the simple scan when its activity ties other remaining variables; the code has no clause-relevance filter for branching.

Implementation in Python, C++, and Java

Each complete program contains both engines, with identical normalization, clause order, watch-bucket mutation, positive decision polarity, tie breaking, activity updates, and restart policy. Python names use underscores and Java uses its usual method naming; the logical operations and printed results match.

Inputs are non-null sequences of non-null clauses with integer literals. The demonstration accepts at most 16 variables, 256 raw clauses, and 4,096 raw literal occurrences. Validate every literal, including literals in a clause that will eventually be discarded as tautological. Duplicate literals are removed in their first-occurrence order; tautological clauses are dropped. Input data is copied and never changed. Empty clauses remain available to the initial contradiction check.

DPLL scans unresolved clauses for pure literals after every propagation fixed point. CDCL uses first-UIP resolution with simple lists, an activity scan, and a geometric restart budget. The sample explicitly passes budget one. C++ and Java use 64-bit instrumentation counters. These limits keep the examples inspectable; they are not a promise of quick solving for every accepted input. The implementation retains all learned clauses, so memory can grow substantially on harder formulas.

Both modes return a SAT flag, a copied total model on success, and seven counters. When all clauses are already satisfied under a partial assignment, unused variables are completed as false. UNSAT returns an empty model. For zero variables, an empty model can also be a valid SAT witness, so always consult the flag. Calling solve again rebuilds the working clause database, watches, activities, and counters from the normalized original formula.

Counter definitions are precise:

• nodes: DPLL recursive entries, or CDCL loop entries before propagation; these are different control-flow units, not a common search-tree size.
• decisions: explicit decision assignments, including the opposite branch in DPLL and repeated choices after a restart.
• implied: newly enqueued assignments with a clause reason, including original units and learned assertions; repeated implication events are counted again.
• pure: DPLL pure-literal choices, separate from implications and decisions.
• conflicts: detected propagation conflicts; an initial empty clause or incompatible original units counts as one initial contradiction.
• learned: clauses added by nonroot conflict analysis.
• restarts: actual policy backtracks to zero; ordinary backjumps are separate.

Before returning, the code clears assignments, levels, reasons, the trail, decision boundaries, and the queue head. restored=YES refers to that assignment state. Watch movement is deliberately preserved during branch undo, and learned clauses deliberately survive CDCL restarts. Neither is required to match the initial arrays. The next public solve rebuilds them.

class SAT:
    def __init__(self, variables, formula):
        if type(variables) is not int or not 0 <= variables <= 16 or len(formula) > 256:
            raise ValueError("input exceeds demonstration limits")
        if sum(map(len, formula)) > 4096:
            raise ValueError("too many literal occurrences")
        self.n, self.base = variables, []
        for raw in formula:
            seen, clause, tautology = set(), [], False
            for lit in raw:
                if type(lit) is not int or lit == 0 or not -variables <= lit <= variables:
                    raise ValueError("invalid literal")
                if -lit in seen:
                    tautology = True
                if lit not in seen:
                    seen.add(lit)
                    clause.append(lit)
            if not tautology:
                self.base.append(clause)

    def index(self, lit):
        return 2 * (abs(lit) - 1) + (1 if lit < 0 else 0)

    def value(self, lit):
        x = self.assign[abs(lit)]
        return x if lit > 0 else -x

    def add_clause(self, clause):
        cid = len(self.clauses)
        self.clauses.append(clause.copy())
        self.watch.append([0, 1 if len(clause) > 1 else 0])
        if clause:
            self.lists[self.index(clause[0])].append(cid)
            if len(clause) > 1:
                self.lists[self.index(clause[1])].append(cid)
        return cid

    def enqueue(self, lit, reason):
        if self.value(lit) != 0:
            return self.value(lit) == 1
        v = abs(lit)
        self.assign[v] = 1 if lit > 0 else -1
        self.level[v], self.reason[v] = len(self.limits), reason
        self.trail.append(lit)
        if reason >= 0:
            self.implied += 1
        return True

    def propagate(self):
        while self.head < len(self.trail):
            false = -self.trail[self.head]
            self.head += 1
            bucket = self.lists[self.index(false)]
            i = 0
            while i < len(bucket):
                cid = bucket[i]
                clause, watches = self.clauses[cid], self.watch[cid]
                side = 0 if clause[watches[0]] == false else 1
                other = watches[1 - side]
                if self.value(clause[other]) == 1:
                    i += 1
                    continue
                replacement = next((k for k in range(len(clause))
                                    if k != watches[0] and k != watches[1]
                                    and self.value(clause[k]) != -1), -1)
                if replacement >= 0:
                    watches[side] = replacement
                    bucket[i] = bucket[-1]
                    bucket.pop()
                    self.lists[self.index(clause[replacement])].append(cid)
                    continue
                if self.value(clause[other]) == -1:
                    return cid
                self.enqueue(clause[other], cid)
                i += 1
        return -1

    def undo(self, mark):
        while len(self.trail) > mark:
            v = abs(self.trail.pop())
            self.assign[v], self.level[v], self.reason[v] = 0, 0, -1
        self.head = min(self.head, mark)

    def backtrack(self, level):
        if len(self.limits) > level:
            self.undo(self.limits[level])
            del self.limits[level:]

    def satisfied(self):
        return all(any(self.value(lit) == 1 for lit in c) for c in self.clauses)

    def save_model(self):
        self.model = [1 if x == 1 else 0 for x in self.assign[1:]]

    def pure_literal(self):
        signs = [0] * (self.n + 1)
        for clause in self.clauses:
            if any(self.value(lit) == 1 for lit in clause):
                continue
            for lit in clause:
                if self.value(lit) == 0:
                    signs[abs(lit)] |= 1 if lit > 0 else 2
        for v in range(1, self.n + 1):
            if signs[v] in (1, 2):
                return v if signs[v] == 1 else -v
        return 0

    def dpll(self):
        self.nodes += 1
        while True:
            if self.propagate() >= 0:
                self.conflicts += 1
                return False
            lit = self.pure_literal()
            if lit == 0:
                break
            self.enqueue(lit, -1)
            self.pures += 1
        if self.satisfied():
            self.save_model()
            return True
        v = next(v for v in range(1, self.n + 1) if self.assign[v] == 0)
        parent = len(self.limits)
        for lit in (v, -v):
            self.limits.append(len(self.trail))
            self.decisions += 1
            self.enqueue(lit, -1)
            found = self.dpll()
            self.backtrack(parent)
            if found:
                return True
        return False

    def analyze(self, cid):
        learned = self.clauses[cid].copy()
        involved = {abs(lit) for lit in learned}
        depth = len(self.limits)
        while sum(self.level[abs(lit)] == depth for lit in learned) > 1:
            variables = {abs(lit) for lit in learned}
            v = next(abs(lit) for lit in reversed(self.trail)
                     if abs(lit) in variables and self.level[abs(lit)] == depth)
            rid = self.reason[v]
            if rid < 0:
                raise RuntimeError("missing implication reason")
            learned = [lit for lit in learned if abs(lit) != v]
            for lit in self.clauses[rid]:
                involved.add(abs(lit))
                if abs(lit) != v and lit not in learned:
                    learned.append(lit)
        pos = next(i for i, lit in enumerate(learned) if self.level[abs(lit)] == depth)
        learned[0], learned[pos] = learned[pos], learned[0]
        back = max((self.level[abs(lit)] for lit in learned[1:]), default=0)
        if len(learned) > 1:
            pos = next(i for i in range(1, len(learned))
                       if self.level[abs(learned[i])] == back)
            learned[1], learned[pos] = learned[pos], learned[1]
        for v in range(1, self.n + 1):
            self.activity[v] = self.activity[v] * 0.5 + (1.0 if v in involved else 0.0)
        return learned, back

    def cdcl(self, restart_base):
        budget, since = restart_base, 0
        while True:
            self.nodes += 1
            conflict = self.propagate()
            if conflict >= 0:
                self.conflicts += 1
                if not self.limits:
                    return False
                clause, back = self.analyze(conflict)
                self.backtrack(back)
                cid = self.add_clause(clause)
                self.learned += 1
                if not self.enqueue(clause[0], cid):
                    raise RuntimeError("learned clause is not asserting")
                since += 1
                continue
            if self.satisfied():
                self.save_model()
                return True
            if since >= budget and self.limits:
                self.backtrack(0)
                self.restarts += 1
                since, budget = 0, budget * 2
                continue
            v = max((v for v in range(1, self.n + 1) if self.assign[v] == 0),
                    key=lambda v: (self.activity[v], -v))
            self.limits.append(len(self.trail))
            self.decisions += 1
            self.enqueue(v, -1)

    def solve(self, mode, restart_base=2):
        if mode not in ("DPLL", "CDCL") or type(restart_base) is not int or not 1 <= restart_base <= 1024:
            raise ValueError("invalid mode or restart budget")
        self.clauses, self.watch = [], []
        self.lists = [[] for _ in range(2 * self.n)]
        self.assign, self.level = [0] * (self.n + 1), [0] * (self.n + 1)
        self.reason, self.activity = [-1] * (self.n + 1), [0.0] * (self.n + 1)
        self.trail, self.limits, self.model, self.head = [], [], [], 0
        self.nodes = self.decisions = self.implied = self.pures = 0
        self.conflicts = self.learned = self.restarts = 0
        bad = False
        for clause in self.base:
            cid = self.add_clause(clause)
            if not clause:
                bad = True
            elif len(clause) == 1 and not self.enqueue(clause[0], cid):
                bad = True
        if bad:
            self.conflicts = 1
            found = False
        else:
            found = self.dpll() if mode == "DPLL" else self.cdcl(restart_base)
        self.undo(0)
        self.limits.clear()
        if any(self.assign) or any(self.level) or any(r != -1 for r in self.reason) or self.head:
            raise RuntimeError("assignment undo failed")
        stats = [self.nodes, self.decisions, self.implied, self.pures,
                 self.conflicts, self.learned, self.restarts]
        return found, self.model.copy(), stats


def show(name, n, formula):
    for mode in ("DPLL", "CDCL"):
        found, model, stats = SAT(n, formula).solve(mode, 1)
        labels = ("nodes", "decisions", "implied", "pure", "conflicts", "learned", "restarts")
        print(name + " / " + mode + ": " + ("SAT" if found else "UNSAT") + ", "
              + ", ".join(f"{k}={v}" for k, v in zip(labels, stats)))
        print("model=[" + ",".join(map(str, model)) + "], restored=YES")


def main():
    show("backtrack", 4, [[-1, 2], [-1, -2], [1, -2], [1, 3], [-3, 4], [-4, 3]])
    show("watch move", 4, [[-1, -2, 3, 4], [1], [2], [-3]])
    show("pure", 3, [[1, 2], [-2, 3]])
    show("unsat", 2, [[1, 2], [1, -2], [-1, 2], [-1, -2]])
    show("restart", 6, [[-1, -3, 4], [-1, -3, -4], [3, 5, 6]])
    print("checks = PASS")


if __name__ == "__main__":
    main()

#include <algorithm>
#include <array>
#include <iostream>
#include <stdexcept>
#include <string>
#include <vector>
using namespace std;

struct Result { bool sat; vector<int> model; vector<long long> stats; };
class SAT {
public:
    int n, head = 0;
    vector<vector<int>> base, clauses, lists;
    vector<array<int, 2>> watch;
    vector<int> assign, level, reason, trail, limits, model;
    vector<double> activity;
    long long nodes=0, decisions=0, implied=0, pures=0, conflicts=0, learned=0, restarts=0;

    SAT(int variables, const vector<vector<int>>& formula) : n(variables) {
        if (n < 0 || n > 16 || formula.size() > 256) throw invalid_argument("input exceeds limits");
        size_t total=0;
        for (const auto& raw : formula) total+=raw.size();
        if (total > 4096) throw invalid_argument("too many literals");
        for (const auto& raw : formula) {
            vector<int> clause; bool tautology=false;
            for (int lit : raw) {
                if (lit==0 || lit < -n || lit > n) throw invalid_argument("invalid literal");
                if (find(clause.begin(),clause.end(),-lit)!=clause.end()) tautology=true;
                if (find(clause.begin(),clause.end(),lit)==clause.end()) clause.push_back(lit);
            }
            if (!tautology) base.push_back(clause);
        }
    }
    int index(int lit) const { return 2*(abs(lit)-1)+(lit<0 ? 1 : 0); }
    int value(int lit) const { return lit>0 ? assign[lit] : -assign[-lit]; }
    int add_clause(const vector<int>& clause) {
        int cid=static_cast<int>(clauses.size()); clauses.push_back(clause);
        watch.push_back({0,clause.size()>1 ? 1 : 0});
        if (!clause.empty()) {
            lists[index(clause[0])].push_back(cid);
            if (clause.size()>1) lists[index(clause[1])].push_back(cid);
        }
        return cid;
    }
    bool enqueue(int lit, int rid) {
        if (value(lit)!=0) return value(lit)==1;
        int v=abs(lit); assign[v]=lit>0 ? 1 : -1;
        level[v]=static_cast<int>(limits.size()); reason[v]=rid;
        trail.push_back(lit); if (rid>=0) ++implied;
        return true;
    }
    int propagate() {
        while (head<static_cast<int>(trail.size())) {
            int falselit=-trail[head++]; auto& bucket=lists[index(falselit)];
            size_t i=0;
            while (i<bucket.size()) {
                int cid=bucket[i]; auto& clause=clauses[cid]; auto& w=watch[cid];
                int side=clause[w[0]]==falselit ? 0 : 1, other=w[1-side];
                if (value(clause[other])==1) { ++i; continue; }
                int replacement=-1;
                for (int k=0;k<static_cast<int>(clause.size());++k)
                    if (k!=w[0] && k!=w[1] && value(clause[k])!=-1) { replacement=k; break; }
                if (replacement>=0) {
                    w[side]=replacement; bucket[i]=bucket.back(); bucket.pop_back();
                    lists[index(clause[replacement])].push_back(cid); continue;
                }
                if (value(clause[other])==-1) return cid;
                enqueue(clause[other],cid); ++i;
            }
        }
        return -1;
    }
    void undo(int mark) {
        while (static_cast<int>(trail.size())>mark) {
            int v=abs(trail.back()); trail.pop_back(); assign[v]=level[v]=0; reason[v]=-1;
        }
        head=min(head,mark);
    }
    void backtrack(int target) {
        if (static_cast<int>(limits.size())>target) { undo(limits[target]); limits.resize(target); }
    }
    bool satisfied() const {
        for (const auto& clause : clauses) {
            bool ok=false; for (int lit : clause) if (value(lit)==1) { ok=true; break; }
            if (!ok) return false;
        }
        return true;
    }
    void save_model() {
        model.clear(); for (int v=1;v<=n;++v) model.push_back(assign[v]==1 ? 1 : 0);
    }
    int pure_literal() const {
        vector<int> signs(n+1,0);
        for (const auto& clause : clauses) {
            bool ok=false; for (int lit : clause) if (value(lit)==1) { ok=true; break; }
            if (ok) continue;
            for (int lit : clause) if (value(lit)==0) signs[abs(lit)]|=lit>0 ? 1 : 2;
        }
        for (int v=1;v<=n;++v) if (signs[v]==1 || signs[v]==2) return signs[v]==1 ? v : -v;
        return 0;
    }
    bool dpll() {
        ++nodes;
        while (true) {
            if (propagate()>=0) { ++conflicts; return false; }
            int lit=pure_literal(); if (lit==0) break;
            enqueue(lit,-1); ++pures;
        }
        if (satisfied()) { save_model(); return true; }
        int v=1; while (assign[v]!=0) ++v;
        int parent=static_cast<int>(limits.size());
        for (int lit : {v,-v}) {
            limits.push_back(static_cast<int>(trail.size())); ++decisions; enqueue(lit,-1);
            bool found=dpll(); backtrack(parent); if (found) return true;
        }
        return false;
    }
    pair<vector<int>,int> analyze(int cid) {
        vector<int> clause=clauses[cid]; vector<bool> involved(n+1,false);
        for (int lit : clause) involved[abs(lit)]=true;
        int depth=static_cast<int>(limits.size());
        while (true) {
            int current=0; for (int lit : clause) current+=level[abs(lit)]==depth;
            if (current<=1) break;
            int v=0;
            for (auto it=trail.rbegin();it!=trail.rend();++it)
                if (level[abs(*it)]==depth && any_of(clause.begin(),clause.end(),[&](int l){return abs(l)==abs(*it);})) { v=abs(*it); break; }
            int rid=reason[v]; if (rid<0) throw logic_error("missing reason");
            clause.erase(remove_if(clause.begin(),clause.end(),[v](int l){return abs(l)==v;}),clause.end());
            for (int lit : clauses[rid]) {
                involved[abs(lit)]=true;
                if (abs(lit)!=v && find(clause.begin(),clause.end(),lit)==clause.end()) clause.push_back(lit);
            }
        }
        size_t pos=0; while (level[abs(clause[pos])]!=depth) ++pos;
        swap(clause[0],clause[pos]); int back=0;
        for (size_t i=1;i<clause.size();++i) back=max(back,level[abs(clause[i])]);
        if (clause.size()>1) {
            pos=1; while (level[abs(clause[pos])]!=back) ++pos;
            swap(clause[1],clause[pos]);
        }
        for (int v=1;v<=n;++v) activity[v]=activity[v]*0.5+(involved[v] ? 1.0 : 0.0);
        return {clause,back};
    }
    bool cdcl(int restart_base) {
        long long budget=restart_base,since=0;
        while (true) {
            ++nodes; int conflict=propagate();
            if (conflict>=0) {
                ++conflicts; if (limits.empty()) return false;
                auto a=analyze(conflict); backtrack(a.second);
                int cid=add_clause(a.first); ++learned;
                if (!enqueue(a.first[0],cid)) throw logic_error("nonasserting clause");
                ++since; continue;
            }
            if (satisfied()) { save_model(); return true; }
            if (since>=budget && !limits.empty()) {
                backtrack(0); ++restarts; since=0; budget*=2; continue;
            }
            int v=0;
            for (int x=1;x<=n;++x)
                if (assign[x]==0 && (v==0 || activity[x]>activity[v])) v=x;
            limits.push_back(static_cast<int>(trail.size())); ++decisions; enqueue(v,-1);
        }
    }
    Result solve(const string& mode, int restart_base=2) {
        if ((mode!="DPLL" && mode!="CDCL") || restart_base<1 || restart_base>1024)
            throw invalid_argument("invalid mode or restart budget");
        clauses.clear(); watch.clear(); lists.assign(2*n,{});
        assign.assign(n+1,0); level.assign(n+1,0); reason.assign(n+1,-1); activity.assign(n+1,0.0);
        trail.clear(); limits.clear(); model.clear(); head=0;
        nodes=decisions=implied=pures=conflicts=learned=restarts=0;
        bool bad=false;
        for (const auto& clause : base) {
            int cid=add_clause(clause);
            if (clause.empty()) bad=true;
            else if (clause.size()==1 && !enqueue(clause[0],cid)) bad=true;
        }
        bool found;
        if (bad) { conflicts=1; found=false; }
        else found=mode=="DPLL" ? dpll() : cdcl(restart_base);
        undo(0); limits.clear();
        for (int v=0;v<=n;++v)
            if (assign[v]!=0 || level[v]!=0 || reason[v]!=-1) throw logic_error("undo failed");
        if (head!=0) throw logic_error("queue undo failed");
        return {found,model,{nodes,decisions,implied,pures,conflicts,learned,restarts} };
    }
};

void show(const string& name,int n,const vector<vector<int>>& formula) {
    for (const string mode : {"DPLL","CDCL"}) {
        Result r=SAT(n,formula).solve(mode,1);
        vector<string> labels={"nodes","decisions","implied","pure","conflicts","learned","restarts"};
        cout<<name<<" / "<<mode<<": "<<(r.sat ? "SAT" : "UNSAT");
        for (size_t i=0;i<labels.size();++i) cout<<", "<<labels[i]<<'='<<r.stats[i];
        cout<<"\nmodel=[";
        for (size_t i=0;i<r.model.size();++i) { if(i) cout<<','; cout<<r.model[i]; }
        cout<<"], restored=YES\n";
    }
}
int main() {
    show("backtrack",4,{ {-1,2}, {-1,-2}, {1,-2}, {1,3}, {-3,4}, {-4,3} });
    show("watch move",4,{ {-1,-2,3,4}, {1}, {2}, {-3} });
    show("pure",3,{ {1,2}, {-2,3} });
    show("unsat",2,{ {1,2}, {1,-2}, {-1,2}, {-1,-2} });
    show("restart",6,{ {-1,-3,4}, {-1,-3,-4}, {3,5,6} });
    cout<<"checks = PASS\n";
}

import java.util.ArrayList;
import java.util.Arrays;
import java.util.List;

public class Main {
    static final class Result {
        boolean sat;
        List<Integer> model;
        long[] stats;
        Result(boolean sat,List<Integer> model,long[] stats) {
            this.sat=sat; this.model=new ArrayList<>(model); this.stats=stats.clone();
        }
    }
    static final class SAT {
        int n,head;
        List<List<Integer>> base=new ArrayList<>(),clauses,lists;
        List<int[]> watch;
        int[] assign,level,reason;
        double[] activity;
        List<Integer> trail,limits,model;
        long nodes,decisions,implied,pures,conflicts,learned,restarts;

        SAT(int variables,int[][] formula) {
            n=variables;
            if(n<0 || n>16 || formula.length>256) throw new IllegalArgumentException("input exceeds limits");
            long total=0; for(int[] c:formula) total+=c.length;
            if(total>4096) throw new IllegalArgumentException("too many literals");
            for(int[] raw:formula) {
                List<Integer> clause=new ArrayList<>(); boolean tautology=false;
                for(int lit:raw) {
                    if(lit==0 || lit < -n || lit>n) throw new IllegalArgumentException("invalid literal");
                    if(clause.contains(-lit)) tautology=true;
                    if(!clause.contains(lit)) clause.add(lit);
                }
                if(!tautology) base.add(clause);
            }
        }
        int index(int lit) { return 2*(Math.abs(lit)-1)+(lit<0 ? 1 : 0); }
        int value(int lit) { return lit>0 ? assign[lit] : -assign[-lit]; }
        int addClause(List<Integer> clause) {
            int cid=clauses.size(); clauses.add(new ArrayList<>(clause));
            watch.add(new int[] {0,clause.size()>1 ? 1 : 0});
            if(!clause.isEmpty()) {
                lists.get(index(clause.get(0))).add(cid);
                if(clause.size()>1) lists.get(index(clause.get(1))).add(cid);
            }
            return cid;
        }
        boolean enqueue(int lit,int rid) {
            if(value(lit)!=0) return value(lit)==1;
            int v=Math.abs(lit); assign[v]=lit>0 ? 1 : -1;
            level[v]=limits.size(); reason[v]=rid; trail.add(lit);
            if(rid>=0) ++implied;
            return true;
        }
        int propagate() {
            while(head<trail.size()) {
                int falselit=-trail.get(head++); List<Integer> bucket=lists.get(index(falselit));
                int i=0;
                while(i<bucket.size()) {
                    int cid=bucket.get(i); List<Integer> clause=clauses.get(cid); int[] w=watch.get(cid);
                    int side=clause.get(w[0])==falselit ? 0 : 1,other=w[1-side];
                    if(value(clause.get(other))==1) { ++i; continue; }
                    int replacement=-1;
                    for(int k=0;k<clause.size();++k)
                        if(k!=w[0] && k!=w[1] && value(clause.get(k))!=-1) { replacement=k; break; }
                    if(replacement>=0) {
                        w[side]=replacement; bucket.set(i,bucket.get(bucket.size()-1)); bucket.remove(bucket.size()-1);
                        lists.get(index(clause.get(replacement))).add(cid); continue;
                    }
                    if(value(clause.get(other))==-1) return cid;
                    enqueue(clause.get(other),cid); ++i;
                }
            }
            return -1;
        }
        void undo(int mark) {
            while(trail.size()>mark) {
                int v=Math.abs(trail.remove(trail.size()-1)); assign[v]=level[v]=0; reason[v]=-1;
            }
            head=Math.min(head,mark);
        }
        void backtrack(int target) {
            if(limits.size()>target) { undo(limits.get(target)); limits.subList(target,limits.size()).clear(); }
        }
        boolean satisfied() {
            for(List<Integer> clause:clauses) {
                boolean ok=false; for(int lit:clause) if(value(lit)==1) { ok=true; break; }
                if(!ok) return false;
            }
            return true;
        }
        void saveModel() {
            model=new ArrayList<>(); for(int v=1;v<=n;++v) model.add(assign[v]==1 ? 1 : 0);
        }
        int pureLiteral() {
            int[] signs=new int[n+1];
            for(List<Integer> clause:clauses) {
                boolean ok=false; for(int lit:clause) if(value(lit)==1) { ok=true; break; }
                if(ok) continue;
                for(int lit:clause) if(value(lit)==0) signs[Math.abs(lit)]|=lit>0 ? 1 : 2;
            }
            for(int v=1;v<=n;++v) if(signs[v]==1 || signs[v]==2) return signs[v]==1 ? v : -v;
            return 0;
        }
        boolean dpll() {
            ++nodes;
            while(true) {
                if(propagate()>=0) { ++conflicts; return false; }
                int lit=pureLiteral(); if(lit==0) break;
                enqueue(lit,-1); ++pures;
            }
            if(satisfied()) { saveModel(); return true; }
            int v=1; while(assign[v]!=0) ++v;
            int parent=limits.size();
            for(int lit:new int[] {v,-v}) {
                limits.add(trail.size()); ++decisions; enqueue(lit,-1);
                boolean found=dpll(); backtrack(parent); if(found) return true;
            }
            return false;
        }
        List<Integer> analyze(int cid) {
            List<Integer> clause=new ArrayList<>(clauses.get(cid)); boolean[] involved=new boolean[n+1];
            for(int lit:clause) involved[Math.abs(lit)]=true;
            int depth=limits.size();
            while(true) {
                int current=0; for(int lit:clause) if(level[Math.abs(lit)]==depth) ++current;
                if(current<=1) break;
                int v=0;
                for(int i=trail.size()-1;i>=0;--i) {
                    int x=Math.abs(trail.get(i)); boolean present=false;
                    for(int lit:clause) if(Math.abs(lit)==x) { present=true; break; }
                    if(present && level[x]==depth) { v=x; break; }
                }
                int rid=reason[v]; if(rid<0) throw new IllegalStateException("missing reason");
                for(int i=clause.size()-1;i>=0;--i) if(Math.abs(clause.get(i))==v) clause.remove(i);
                for(int lit:clauses.get(rid)) {
                    involved[Math.abs(lit)]=true;
                    if(Math.abs(lit)!=v && !clause.contains(lit)) clause.add(lit);
                }
            }
            int pos=0; while(level[Math.abs(clause.get(pos))]!=depth) ++pos;
            java.util.Collections.swap(clause,0,pos);
            int back=0; for(int i=1;i<clause.size();++i) back=Math.max(back,level[Math.abs(clause.get(i))]);
            if(clause.size()>1) {
                pos=1; while(level[Math.abs(clause.get(pos))]!=back) ++pos;
                java.util.Collections.swap(clause,1,pos);
            }
            for(int v=1;v<=n;++v) activity[v]=activity[v]*0.5+(involved[v] ? 1.0 : 0.0);
            return clause;
        }
        boolean cdcl(int restartBase) {
            long budget=restartBase,since=0;
            while(true) {
                ++nodes; int conflict=propagate();
                if(conflict>=0) {
                    ++conflicts; if(limits.isEmpty()) return false;
                    List<Integer> clause=analyze(conflict);
                    int back=0; for(int i=1;i<clause.size();++i) back=Math.max(back,level[Math.abs(clause.get(i))]);
                    backtrack(back); int cid=addClause(clause); ++learned;
                    if(!enqueue(clause.get(0),cid)) throw new IllegalStateException("nonasserting clause");
                    ++since; continue;
                }
                if(satisfied()) { saveModel(); return true; }
                if(since>=budget && !limits.isEmpty()) {
                    backtrack(0); ++restarts; since=0; budget*=2; continue;
                }
                int v=0;
                for(int x=1;x<=n;++x) if(assign[x]==0 && (v==0 || activity[x]>activity[v])) v=x;
                limits.add(trail.size()); ++decisions; enqueue(v,-1);
            }
        }
        Result solve(String mode,int restartBase) {
            if((!mode.equals("DPLL") && !mode.equals("CDCL")) || restartBase<1 || restartBase>1024)
                throw new IllegalArgumentException("invalid mode or restart budget");
            clauses=new ArrayList<>(); watch=new ArrayList<>(); lists=new ArrayList<>();
            for(int i=0;i<2*n;++i) lists.add(new ArrayList<>());
            assign=new int[n+1]; level=new int[n+1]; reason=new int[n+1]; activity=new double[n+1];
            Arrays.fill(reason,-1); trail=new ArrayList<>(); limits=new ArrayList<>(); model=new ArrayList<>(); head=0;
            nodes=decisions=implied=pures=conflicts=learned=restarts=0;
            boolean bad=false;
            for(List<Integer> clause:base) {
                int cid=addClause(clause);
                if(clause.isEmpty()) bad=true;
                else if(clause.size()==1 && !enqueue(clause.get(0),cid)) bad=true;
            }
            boolean found;
            if(bad) { conflicts=1; found=false; }
            else found=mode.equals("DPLL") ? dpll() : cdcl(restartBase);
            undo(0); limits.clear();
            for(int v=0;v<=n;++v)
                if(assign[v]!=0 || level[v]!=0 || reason[v]!=-1) throw new IllegalStateException("undo failed");
            if(head!=0) throw new IllegalStateException("queue undo failed");
            return new Result(found,model,new long[] {nodes,decisions,implied,pures,conflicts,learned,restarts});
        }
    }
    static void show(String name,int n,int[][] formula) {
        for(String mode:new String[] {"DPLL","CDCL"}) {
            Result r=new SAT(n,formula).solve(mode,1);
            String[] labels={"nodes","decisions","implied","pure","conflicts","learned","restarts"};
            StringBuilder out=new StringBuilder(name+" / "+mode+": "+(r.sat ? "SAT" : "UNSAT"));
            for(int i=0;i<labels.length;++i) out.append(", ").append(labels[i]).append('=').append(r.stats[i]);
            System.out.println(out); out=new StringBuilder("model=[");
            for(int i=0;i<r.model.size();++i) { if(i>0) out.append(','); out.append(r.model.get(i)); }
            System.out.println(out+"], restored=YES");
        }
    }
    public static void main(String[] args) {
        show("backtrack",4,new int[][] { {-1,2}, {-1,-2}, {1,-2}, {1,3}, {-3,4}, {-4,3} });
        show("watch move",4,new int[][] { {-1,-2,3,4}, {1}, {2}, {-3} });
        show("pure",3,new int[][] { {1,2}, {-2,3} });
        show("unsat",2,new int[][] { {1,2}, {1,-2}, {-1,2}, {-1,-2} });
        show("restart",6,new int[][] { {-1,-3,4}, {-1,-3,-4}, {3,5,6} });
        System.out.println("checks = PASS");
    }
}

Expected stdout, identical in all three languages:

• backtrack / DPLL: SAT, nodes=3, decisions=2, implied=4, pure=0, conflicts=1, learned=0, restarts=0
• model=[0,0,1,1], restored=YES
• backtrack / CDCL: SAT, nodes=3, decisions=1, implied=5, pure=0, conflicts=1, learned=1, restarts=0
• model=[0,0,1,1], restored=YES
• watch move / DPLL: SAT, nodes=1, decisions=0, implied=4, pure=0, conflicts=0, learned=0, restarts=0
• model=[1,1,0,1], restored=YES
• watch move / CDCL: SAT, nodes=1, decisions=0, implied=4, pure=0, conflicts=0, learned=0, restarts=0
• model=[1,1,0,1], restored=YES
• pure / DPLL: SAT, nodes=1, decisions=0, implied=0, pure=2, conflicts=0, learned=0, restarts=0
• model=[1,0,0], restored=YES
• pure / CDCL: SAT, nodes=3, decisions=2, implied=1, pure=0, conflicts=0, learned=0, restarts=0
• model=[1,1,1], restored=YES
• unsat / DPLL: UNSAT, nodes=3, decisions=2, implied=2, pure=0, conflicts=2, learned=0, restarts=0
• model=[], restored=YES
• unsat / CDCL: UNSAT, nodes=3, decisions=1, implied=3, pure=0, conflicts=2, learned=1, restarts=0
• model=[], restored=YES
• restart / DPLL: SAT, nodes=1, decisions=0, implied=0, pure=2, conflicts=0, learned=0, restarts=0
• model=[0,0,1,0,0,0], restored=YES
• restart / CDCL: SAT, nodes=10, decisions=7, implied=3, pure=0, conflicts=1, learned=1, restarts=1
• model=[1,1,0,1,1,0], restored=YES
• checks = PASS

The pure fixture illustrates why different valid models across solver modes are expected: DPLL makes two pure choices, whereas CDCL makes decisions and a unit implication. Neither mode counts models. The unsat fixture contains all four binary sign combinations on two variables; each assignment falsifies one of its clauses.

Validation used 8,433 inputs per language in both modes, giving 16,866 mode/input cases per language. The corpus includes every subset of the nine canonical clauses over two variables; every family of at most four canonical clauses of width at most two over three variables; 2,800 seeded random formulas; fifty 16-variable random 3-CNF formulas; pigeonhole instances under multiple restart budgets; boundary fixtures; and ten invalid inputs. The valid corpus has 4,577 SAT and 3,846 UNSAT formulas. Exhaustive truth tables independently checked each answer and each returned model. Both modes were repeated on the same solver object, with identical results and unchanged inputs.

Instrumented Python additionally performed 85,566 implication-reason checks, 39,834 watch-list membership checks, 33,988 successful propagation fixed-point checks, 38,800 undo checks, and 1,332 learned-clause checks. Each learned clause had exactly one current-level literal, was false at the conflict assignment, and held in every original satisfying assignment found by the independent oracle. Across one run per mode/input, CDCL learned 666 clauses and executed 92 restarts. C++ ran with address and undefined-behavior sanitizers; Java ran with assertions enabled. These checks validate the small implementation and corpus, not industrial-scale performance or proof-certificate generation.

Complexity, Correctness, and Invariants

Let $n$ be the variable count, $m$ the normalized original clause count, and $L$ the total normalized original literal count. Consider growing inputs rather than treating the fixed demonstration limits as an asymptotic bound. After normalization, each clause has width at most $n$. Stable duplicate checking in the C++ and Java versions gives a conservative normalization bound $O(n+m_{\text{raw}}+nL_{\text{raw}})$; Python's sets usually make this phase cheaper. Building the watch lists is linear in the stored formula size.

DPLL. Let $N$ be recursive entries. A conservative bound for these straightforward implementations is

$$T_{\mathrm{DPLL}}=O\bigl(N(n+1)(n+m+L+1)\bigr),\qquad N\le 2^{n+1}-1.$$

The polynomial factor accounts for propagation scans and repeated whole-formula scans for pure literals. Each pure choice assigns a new variable, so at most $n$ such choices occur in one entry. The binary search tree can still be exponential; propagation and purity often shrink it without providing a polynomial-time guarantee. Auxiliary storage, including the formula and watches, is $O(n+m+L)$: the trail and recursive depth are at most $n$, and the formula is not copied at every branch.

Watched literals. Only clauses with a falsified watch are revisited, but finding a replacement can scan an entire clause. The code starts that scan at the beginning each time. Therefore one propagation call is not automatically $O(L)$, and watching does not make SAT polynomial. During a monotone propagation segment, a clause of width $k$ can incur $O(k^2)$ literal inspections; the simpler bound above allows for this work. Backtracking may cause future rescanning.

CDCL. Let $P$ be loop entries, $C$ the number of conflicts, and $Q$ the maximum live database size measured as clauses plus literal occurrences, including learned clauses. A conservative implementation-specific bound is

$$T_{\mathrm{CDCL}}=O\bigl(P(n+1)(n+Q+1)+Cn^3\bigr),\qquad S_{\mathrm{CDCL}}=O(n+Q).$$

The $n^3$ term allows for the deliberately simple list-based first-UIP analysis: at most $n$ reverse-trail resolutions per conflict, with repeated trail searches and list membership work. This is a bound for the teaching code, rather than the data structures used in optimized solvers. With no learned-clause deletion, $Q$ can grow exponentially. Restarts revisit decisions, so the binary-tree entry bound for DPLL must not be applied to CDCL's loop counter. General CNF SAT retains exponential worst-case behavior for these approaches; learning and branching heuristics exploit structure rather than removing the underlying difficulty.

Best and average cases. An empty formula is accepted after setup; an explicit empty clause is rejected during setup; a chain of units may settle the answer without any decisions. Input processing still costs time proportional to what is read and stored, and the shown early-satisfaction checks scan the database. There is no distribution-independent average-case complexity: random formulas, circuit encodings, and structured configuration instances can behave very differently.

Correctness has several connected parts. Unit propagation forces a literal that every satisfying extension of the current assignment must make true. Pure-literal choice preserves the existence of at least one extension: assigning a pure variable to its satisfying polarity cannot falsify an unsatisfied clause, and already satisfied clauses remain true. DPLL then splits on the two exhaustive values of an unassigned variable and restores the parent trail before exploring its sibling.

For CDCL, resolution is sound: from $A\lor x$ and $B\lor\neg x$, derive $A\lor B$. Starting from original clauses and previously sound learned clauses, every new learned clause is entailed by the original CNF. Backjumping makes the learned clause unit without discarding any model of the original formula. Watches merely schedule the same unit/conflict checks. A SAT model satisfies every original clause; a level-zero conflict has no remaining branch decision on which it depends.

Completeness also needs progress. DPLL has finitely many binary decisions. In the shown CDCL policy, learned clauses are retained and restart budgets grow, rather than repeatedly resetting search to the same state with all learned information erased. After propagation reaches a fixed point, the engine must either finish, learn from a conflict, restart under the stated budget, or assign an unassigned variable. Correctness should not be inferred for an arbitrary restart/deletion policy substituted into the code.

Variants, Pitfalls, and Optimizations

Watch invariants and rollback. At a conflict-free propagation fixed point, a nonunit clause either has a true watched literal or both its watches are nonfalse; no unresolved unit is waiting to be assigned. A satisfied clause can have a false watch, so asserting “both watches are always nonfalse” is too strong. Check watch-list membership separately from assignment values. A moved watch is still a valid place to watch when assignments are undone; restore the trail suffix, not the old watch positions.

The queue head is part of assignment state. After removing a trail suffix, clamp the head to the new length so a newly enqueued opposite decision will be processed. Clear stale reason and level fields as well as values. Reasons are clause IDs, not a list of guessed assumptions. The supplied code keeps clause IDs stable and never deletes a clause that might be referenced.

Conflict analysis. First-UIP resolution proceeds backward through the trail, not by arbitrarily deleting decision literals from a conflict clause. A learned clause must be a logical consequence of the original instance. The asserting literal occupies the first watch position; a highest-level remaining literal occupies the second when there is one. This matters because the clause is attached under a partial assignment, after some falsification events have already been processed. Merely attaching it and waiting for an old event to happen again would miss its immediate unit consequence; enqueue that consequence explicitly.

Activities and restarts. Production solvers use tuned decay rates, efficient priority structures, phase selection, clause minimization, and policies for retaining or deleting learned clauses. The simple update $a_v\leftarrow a_v/2+\text{bump}_v$ emphasizes recent conflicts and stays numerically bounded here. It is a VSIDS-style variant, not a specification that every VSIDS implementation halves every score on every conflict. Restarts preserve learned clauses and scores, and preserve level-zero implications; they do not mean rebuilding an empty solver. A restart is distinct from the backjump justified by a particular learned clause.

CNF encoding. Naively distributing disjunction over conjunction can expand a formula dramatically. A Tseitin encoding introduces a variable for each subexpression and clauses enforcing its meaning, then asserts the output variable. For example, $y\leftrightarrow(a\land b)$ is represented by

$$(\neg y\lor a)\land(\neg y\lor b)\land(y\lor\neg a\lor\neg b).$$

The resulting formula is satisfiable exactly when the original asserted expression is, and auxiliary variables must be projected away when reporting original inputs. Encoding strength also affects propagation: logically correct encodings can expose different amounts of useful unit reasoning.

Related tasks. Incremental SAT reuses a clause database under changing assumptions and needs careful assumption management. AllSAT enumerates models by adding blocking clauses. Model counting requires accounting for every assignment, so the pure-literal shortcut used here cannot simply be treated as a forced truth value. MaxSAT optimizes satisfied soft constraints; SMT adds theory reasoning for objects such as integers or arrays. UNSAT proof logging and independent checking require additional machinery; this implementation returns a decision and a witness for SAT, without producing a refutation certificate.

Practice Problems and Real-World Use

Begin with truth tables over two or three variables. Generate clauses containing duplicates, tautologies, units, and the empty clause; compare each solver's SAT flag and evaluate every returned model. Then test a formula whose first branch fails, a long watched clause whose watch moves more than once, and repeated solves on the same object. An UNSAT oracle check is essential because a valid model alone cannot expose false UNSAT answers.

For graph coloring, introduce $x_{v,c}$ for “vertex $v$ receives color $c$.” Give each vertex an at-least-one-color clause, pairwise at-most-one-color clauses, and a clause $\neg x_{u,c}\lor\neg x_{v,c}$ for each edge and color. More compact cardinality encodings become useful as the number of choices grows. The model is only as faithful as the encoding: omitting the at-least-one constraint would allow an uncolored vertex.

For further reading, Carnegie Mellon's DPLL lecture notes develop propagation and resolution-based learning. The original Chaff paper explains watched propagation, VSIDS, and retained information across restarts. The programs here use their own deliberately small data structures and policies; the measured traces describe these programs.