CDCL SAT solving

Deep dive

How it works

Parts:

• clause store — flat arena of original and learned clauses
• watch lists — watches[lit]: (clause, blocker) pairs
• trail — assigned literals in order, level and reason per variable
• decision heuristic — VSIDS activity in a heap, saved phase
• analysis — 1-UIP resolution: learned clause and backjump level
• policies — restarts, database reduction, pre/inprocessing

1. Propagate each newly false literal through its watch list: unit clauses assign (with reason), all-false is a conflict.
2. No conflict: all set means SAT; else open a level, decide the top-activity variable at its saved phase.
3. Conflict at level 0: UNSAT. Else resolve backwards along the trail with reasons until one current-level literal remains (first UIP); bump each variable seen.
4. Learn negated UIP plus the lower-level literals; backjump to the highest of those levels, where the clause asserts the UIP.
5. Decay: bump increment times 1/0.95. Phase saving: undone variables keep their polarity.
6. Restart (to level 0, keep clauses and activities): Luby sequence 1,1,2,1,1,2,4,... times about 100 conflicts, or Glucose-style when the recent average LBD exceeds the long-run one.
7. Reduce: delete half the learned clauses with the highest LBD (distinct decision levels in the clause); keep LBD about 2 and current reasons.
8. Pre/inprocessing: subsumption, variable elimination, vivification (proof-logged).

 decide ─► propagate ─► conflict? ─no─► all set? ─yes─► SAT
   ▲                       │yes            └no─► decide
   │              level 0? ─yes─► UNSAT
   │                       │no
   └─ restart/reduce ◄─ analyze (1-UIP) ► learn ► backjump ► assert

Incremental: assumptions are the first decisions; on UNSAT the solver returns the assumptions used (core) and keeps learned clauses.

Code

Watches (no blockers), levels, 1-UIP, backjump, phase saving, linear-scan VSIDS (no room for a heap). No restarts, deletion or proofs; clauses need 2+ literals. Checks: 500 small formulas vs brute force, 100 larger ones.

// Literal: var v -> 2v (positive), 2v+1 (negated); negation = lit ^ 1.
#[derive(Default)]
struct Solver {
    cl: Vec<Vec<u32>>,  // c[0], c[1] watched
    w: Vec<Vec<usize>>, // w[l]: visit when l becomes false
    val: Vec<i8>,       // 1 true, -1 false, 0 unset
    lvl: Vec<usize>, rsn: Vec<Option<usize>>, // per var
    trail: Vec<u32>, lim: Vec<usize>, qh: usize, // lim: trail length per level start
    act: Vec<f64>, inc: f64, phase: Vec<bool>,
    conflicts: u64, decisions: u64,
}
impl Solver {
    fn enqueue(&mut self, l: u32, r: Option<usize>) {
        self.val[l as usize] = 1; self.val[(l ^ 1) as usize] = -1;
        self.lvl[(l >> 1) as usize] = self.lim.len(); self.rsn[(l >> 1) as usize] = r; self.trail.push(l);
    }
    fn attach(&mut self, c: Vec<u32>) -> usize {
        let i = self.cl.len(); self.w[c[0] as usize].push(i); self.w[c[1] as usize].push(i);
        self.cl.push(c); i
    }
    fn propagate(&mut self) -> Option<usize> {
        while self.qh < self.trail.len() {
            let f = self.trail[self.qh] ^ 1; self.qh += 1; // f just became false
            let ws = std::mem::take(&mut self.w[f as usize]);
            let mut keep = Vec::with_capacity(ws.len());
            for (i, &ci) in ws.iter().enumerate() {
                let c = &mut self.cl[ci];
                if c[0] == f { c.swap(0, 1); } // now c[1] == f
                let c0 = c[0];
                if self.val[c0 as usize] == 1 { keep.push(ci); continue; }
                if let Some(k) = (2..c.len()).find(|&k| self.val[c[k] as usize] != -1) {
                    c.swap(1, k); let nl = c[1]; self.w[nl as usize].push(ci); continue;
                }
                keep.push(ci);
                if self.val[c0 as usize] == -1 { keep.extend_from_slice(&ws[i + 1..]); self.w[f as usize] = keep; return Some(ci); } // conflict
                self.enqueue(c0, Some(ci)); // unit
            }
            self.w[f as usize] = keep;
        }
        None
    }
    /// 1-UIP: resolve back along the trail until one current-level literal is left
    fn analyze(&mut self, mut confl: usize) -> (Vec<u32>, usize) {
        let (cur, mut seen) = (self.lim.len(), vec![false; self.act.len()]);
        let (mut learnt, mut cnt, mut idx, mut p) = (vec![0u32], 0, self.trail.len(), u32::MAX);
        loop {
            for j in 0..self.cl[confl].len() {
                let q = self.cl[confl][j]; let v = (q >> 1) as usize;
                if q == p || seen[v] || self.lvl[v] == 0 { continue; }
                seen[v] = true; self.act[v] += self.inc; // VSIDS bump
                if self.lvl[v] == cur { cnt += 1 } else { learnt.push(q) }
            }
            loop { idx -= 1; if seen[(self.trail[idx] >> 1) as usize] { break; } }
            p = self.trail[idx]; cnt -= 1;
            if cnt == 0 { break; }
            confl = self.rsn[(p >> 1) as usize].unwrap();
        }
        learnt[0] = p ^ 1; // asserting literal
        let mut bt = 0; // backjump level = highest of the rest, kept watched at c[1]
        for i in 1..learnt.len() { let l = self.lvl[(learnt[i] >> 1) as usize]; if l > bt { bt = l; learnt.swap(1, i); } }
        self.inc /= 0.95; // decay (no rescale: small runs only)
        (learnt, bt)
    }
    fn solve(&mut self) -> bool {
        loop {
            if let Some(confl) = self.propagate() {
                self.conflicts += 1;
                if self.lim.is_empty() { return false; }
                let (learnt, bt) = self.analyze(confl);
                while self.trail.len() > self.lim[bt] { // backjump
                    let l = self.trail.pop().unwrap();
                    self.phase[(l >> 1) as usize] = l & 1 == 0; // phase saving
                    self.val[l as usize] = 0; self.val[(l ^ 1) as usize] = 0;
                }
                self.lim.truncate(bt); self.qh = self.trail.len();
                let a = learnt[0]; let r = if learnt.len() > 1 { Some(self.attach(learnt)) } else { None };
                self.enqueue(a, r);
            } else { // linear-scan VSIDS
                let best = (0..self.act.len()).filter(|&v| self.val[2 * v] == 0)
                    .max_by(|&a, &b| self.act[a].total_cmp(&self.act[b]));
                let Some(v) = best else { return true }; self.decisions += 1; self.lim.push(self.trail.len());
                self.enqueue(2 * v as u32 + if self.phase[v] { 0 } else { 1 }, None);
            }
        }
    }
}
fn run(n: usize, cls: &[Vec<u32>]) -> (Option<Vec<bool>>, u64, u64) {
    let mut s = Solver { w: vec![vec![]; 2 * n], val: vec![0; 2 * n], lvl: vec![0; n], rsn: vec![None; n],
                         act: vec![0.0; n], inc: 1.0, phase: vec![false; n], ..Default::default() };
    for c in cls { s.attach(c.clone()); }
    let sat = s.solve();
    (sat.then(|| (0..n).map(|v| s.val[2 * v] == 1).collect()), s.conflicts, s.decisions)
}
fn sat_by(m: &[bool], cls: &[Vec<u32>]) -> bool { cls.iter().all(|c| c.iter().any(|&l| m[(l >> 1) as usize] == (l & 1 == 0))) }
fn brute(n: usize, cls: &[Vec<u32>]) -> bool { (0u32..1 << n).any(|x| sat_by(&(0..n).map(|v| x >> v & 1 == 1).collect::<Vec<_>>(), cls)) }
fn random3(n: usize, r: &mut u64) -> Vec<Vec<u32>> { // seeded LCG, ratio 4.26
    let mut next = || { *r = r.wrapping_mul(6364136223846793005).wrapping_add(1442695040888963407); (*r >> 33) as u32 };
    (0..(4.26 * n as f64) as usize).map(|_| {
        let mut vs = vec![]; while vs.len() < 3 { let v = next() % n as u32; if !vs.contains(&v) { vs.push(v) } }
        vs.iter().map(|&v| 2 * v + (next() & 1)).collect()
    }).collect()
}
fn main() {
    let mut r = 42u64;
    for i in 0..500 { // vs brute force
        let (n, cls) = (8 + i % 10, random3(8 + i % 10, &mut r));
        match run(n, &cls).0 { Some(m) => assert!(sat_by(&m, &cls) && brute(n, &cls)), None => assert!(!brute(n, &cls)) }
    }
    let (t, mut tot, mut sat) = (std::time::Instant::now(), (0, 0), 0);
    for i in 0..100 {
        let (n, cls) = (50 + i / 2, random3(50 + i / 2, &mut r));
        let (m, c, d) = run(n, &cls); tot = (tot.0 + c, tot.1 + d);
        if let Some(m) = m { assert!(sat_by(&m, &cls)); sat += 1 }
    }
    println!("{sat}/100 sat, {} conflicts, {} decisions, {:?}", tot.0, tot.1, t.elapsed());
}

Complexity and constants

Analysis is linear in trail suffix and clauses touched; the learned database drives memory and cache misses. Random 3-SAT near ratio 4.26 is the hard region: here about 157 conflicts per instance.

Efficiency

• Cost: a propagation step chases a watch list and a clause: one to two cache misses. Memory-latency bound.
• Levers:
  • blocker literal in watches — skips the clause read — always
  • flat arena, 32-bit refs — fewer cache misses — large databases
  • binaries inlined in watches — no clause read — many binaries
  • LBD reduction — small hot database — long runs
  • heap-based VSIDS — O(log n) pick — beyond about a thousand variables
• Naive → standard → state of the art: counter-based DPLL, a visit per occurrence · watches, VSIDS, restarts, reduction (MiniSat, Glucose) · plus inprocessing and rephasing (CaDiCaL, Kissat).

Implementation notes

• Asserting literal at c[0], highest-level other at c[1]: watches stay valid after the jump.
• Cost drivers: watch bytes, clause reads, arena garbage after reduction (compact once).
• Proof: append each learned clause, d lines for deletions; buffered, binary DRAT.

Pitfalls

• A wrong backjump level (must be the max of the non-asserting literals) silently corrupts propagation.
• Deleting a clause that is a current reason.

Variants and alternatives

In production

CaDiCaL and Kissat are the actively maintained reference solvers; CryptoMiniSat for XOR-heavy formulas; libsolv resolves RPM/deb/Arch dependencies; RustSAT wraps solvers for Rust.

Implementations

Sources

• Marques-Silva, Sakallah, GRASP: a search algorithm for propositional satisfiability, IEEE Trans. Computers 1999. paper
• Moskewicz et al., Chaff: engineering an efficient SAT solver, DAC 2001. paper
• Eén, Sörensson, An extensible SAT-solver, SAT 2003. paper · code
• Audemard, Simon, Predicting learnt clauses quality in modern SAT solvers, IJCAI 2009. paper
• Luby, Sinclair, Zuckerman, Optimal speedup of Las Vegas algorithms, Inf. Process. Lett. 1993. paper
• Soos, Nohl, Castelluccia, Extending SAT solvers to cryptographic problems, SAT 2009. paper
• Wetzler, Heule, Hunt, DRAT-trim: efficient checking and trimming using expressive clausal proofs, SAT 2014. paper