Two watched literals

Deep dive

How it works

In: the clause database, the assignment trail, the next assigned literal · Out: new implied literals or a conflicting clause · State: watches[l] lists with a blocker per entry, kept across backtracking · Cost: work per assignment proportional to the clauses watching the falsified literal; nothing on backtrack

Invariant: every clause of length ≥ 2 keeps two literals c[0], c[1] that are non-false, or, if it cannot, the clause is unit/conflicting and the other watched literal is true or being set.

1. watches[l] lists the clauses watching literal l. It is visited when l becomes false.
2. Take the next assigned literal p from the trail; f = ¬p is falsified. Scan watches[f].
3. For each entry: if its blocker literal is true, keep the entry and move on (clause not read).
4. Else load the clause, make sure c[1] == f. If c[0] is true, keep the watch (update the blocker to c[0]).
5. Else look for c[k], k ≥ 2, that is not false. Found: swap it into slot 1 and move the entry to watches[c[1]].
6. None found: the clause is unit (set c[0], reason = this clause) or, if c[0] is false, a conflict.
7. Backtrack: unassign trail literals; the watch lists are left as they are.

clause (a b c d), watches a,b          a becomes false:
  a* b* c d   --- a:=F --->   c is non-false: swap  --->  c* b* a d   (watch moved a -> c)
  c* b* a d   --- c:=F --->   d is non-false: swap  --->  d* b* a c
  d* b* a c   --- d:=F --->   nothing left: b unit (or conflict if b is false)

Code

// Literal: var v -> 2v (positive), 2v+1 (negated); negation = lit ^ 1.
pub type Lit = u32;
const TRUE: i8 = 1;
const FALSE: i8 = -1;
const UNDEF: i8 = 0;

#[derive(Clone, Copy)]
struct Watcher { cref: u32, blocker: Lit }

pub struct Solver {
    arena: Vec<Lit>,                // all clause literals, back to back
    clauses: Vec<(u32, u32)>,       // (start, len) into arena
    watches: Vec<Vec<Watcher>>,     // watches[l]: clauses to visit when l becomes FALSE
    val: Vec<i8>,                   // value per literal (val[l] == -val[l ^ 1])
    trail: Vec<Lit>,
    lim: Vec<usize>,                // trail length at each decision level
    qhead: usize,
    pub visits: u64,                // watcher entries touched (for measurements)
}

impl Solver {
    pub fn new(nvars: usize) -> Self {
        Solver { arena: vec![], clauses: vec![], watches: vec![vec![]; 2 * nvars],
                 val: vec![UNDEF; 2 * nvars], trail: vec![], lim: vec![], qhead: 0, visits: 0 }
    }
    /// Call before any decision. No duplicate or complementary literals. false = trivially UNSAT.
    pub fn add_clause(&mut self, lits: &[Lit]) -> bool {
        match lits.len() {
            0 => false,
            1 => self.val[lits[0] as usize] != FALSE && { self.enqueue(lits[0]); true },
            _ => {
                let cref = self.clauses.len() as u32;
                self.clauses.push((self.arena.len() as u32, lits.len() as u32));
                self.arena.extend_from_slice(lits);
                self.watches[lits[0] as usize].push(Watcher { cref, blocker: lits[1] });
                self.watches[lits[1] as usize].push(Watcher { cref, blocker: lits[0] });
                true
            }
        }
    }
    fn enqueue(&mut self, l: Lit) {
        self.val[l as usize] = TRUE;
        self.val[(l ^ 1) as usize] = FALSE;
        self.trail.push(l);
    }
    /// Returns the conflicting clause, if any.
    pub fn propagate(&mut self) -> Option<u32> {
        while self.qhead < self.trail.len() {
            let falsified = self.trail[self.qhead] ^ 1;
            self.qhead += 1;
            let mut ws = std::mem::take(&mut self.watches[falsified as usize]);
            let (mut i, mut j) = (0, 0);
            let mut conflict = None;
            while i < ws.len() {
                let w = ws[i];
                i += 1;
                self.visits += 1;
                if self.val[w.blocker as usize] == TRUE { ws[j] = w; j += 1; continue; } // no clause access
                let (s, n) = self.clauses[w.cref as usize];
                let c = &mut self.arena[s as usize..(s + n) as usize];
                if c[0] == falsified { c.swap(0, 1); }        // invariant: c[1] is the falsified watch
                let first = c[0];
                if first != w.blocker && self.val[first as usize] == TRUE {
                    ws[j] = Watcher { cref: w.cref, blocker: first }; j += 1; continue;
                }
                let mut k = 2;
                while k < c.len() && self.val[c[k] as usize] == FALSE { k += 1; }
                if k < c.len() {                               // move the watch: no work on backtrack
                    c.swap(1, k);
                    self.watches[c[1] as usize].push(Watcher { cref: w.cref, blocker: first });
                    continue;
                }
                ws[j] = w; j += 1;                             // clause is unit or conflicting
                if self.val[first as usize] == FALSE {
                    conflict = Some(w.cref);
                    self.qhead = self.trail.len();
                    while i < ws.len() { ws[j] = ws[i]; j += 1; i += 1; }
                } else {
                    self.enqueue(first);
                }
            }
            ws.truncate(j);
            self.watches[falsified as usize] = ws;
            if conflict.is_some() { return conflict; }
        }
        None
    }
    /// Undo to `level`; watch lists are untouched.
    pub fn backtrack(&mut self, level: usize) {
        if self.lim.len() <= level { return; }
        for &l in &self.trail[self.lim[level]..] { self.val[l as usize] = UNDEF; self.val[(l ^ 1) as usize] = UNDEF; }
        self.trail.truncate(self.lim[level]);
        self.lim.truncate(level);
        self.qhead = self.trail.len();
    }
    /// Tiny DPLL driver: decide, propagate, flip on conflict.
    pub fn solve(&mut self) -> bool {
        if self.propagate().is_some() { return false; }
        let Some(v) = (0..self.val.len() / 2).find(|&v| self.val[2 * v] == UNDEF) else { return true };
        for l in [2 * v as Lit, 2 * v as Lit + 1] {
            self.lim.push(self.trail.len());
            self.enqueue(l);
            if self.solve() { return true; }
            self.backtrack(self.lim.len() - 1);
        }
        false
    }
    pub fn model(&self, v: usize) -> bool { self.val[2 * v] == TRUE }
}

Validated by me against brute force on 3000 random 3-SAT instances (3-12 variables); the model is checked against every clause.

Complexity and constants

• Propagating one assignment visits the entries in one watch list: on average (watches per literal) = 2·clauses / (2·vars).
• Per visit: the watch entry is 8 bytes (clause ref + blocker); a blocker hit costs one random read of the blocker's value (1 byte per literal or per variable) and no clause access. A non-blocker visit adds a clause read, normally a cache miss (order of 100 ns from DRAM, a few ns from L2).
• Long clauses: the scan for a replacement watch is O(length) per visit; the worst case over a branch is quadratic in clause length unless the scan resumes where it stopped (see Variants).
• Backtrack: O(unassigned vars), no watch work.

Efficiency

• Bound: memory latency. Propagation is pointer-chasing through watch lists and clauses; the solver is cache-miss-bound, not ALU-bound. Propagation is commonly reported as the majority of CDCL runtime.
• Work avoided: only clauses watching the falsified literal are visited. My measurement (code above with a fixed-seed xorshift generator, 20 random instances each, DPLL driver): counter-per-clause schemes (touch every clause containing the variable on assignment, counted once, not again on backtrack) did 5.3x (k=3), 10.2x (k=5), 7.9x (k=10), 15.7x (k=20) more clause touches than watcher visits. Real CDCL with learned clauses is not covered by this.
• Blocker literals turn most visits into a read of one value byte plus a sequential read of the 8-byte entry; the clause body stays cold.
• Layout: 8-byte entries in one contiguous Vec per literal, compacted in place while scanning; clauses in one flat arena with u32 refs (half a pointer).
• Cheaper alternative: for formulas with only binary clauses, store the other literal directly in the watch entry and never read a clause.

Implementation notes

• Watch lists indexed by literal, clause refs as u32 offsets into an arena; garbage-collect and compact the arena when learned clauses are deleted, fixing up the watch lists.
• Blocker: set it to the other watched literal on insertion, update it to the true c[0] when found (as above).
• Binary clauses: inline in the watch entry (flag + other literal) so propagating them reads no clause (done in CaDiCaL and Kissat, from memory; MiniSat 2.2 keeps them as ordinary clauses).
• Save a per-clause search position for long clauses and resume the replacement scan there (Gent 2013) instead of restarting at index 2.
• Learned clauses: watch the asserting literal and the false literal with the highest decision level, otherwise the invariant breaks after backjumping.

Pitfalls

• Borrowing: pushing to another watch list while scanning one needs the scanned list taken out (mem::take); the new watch is never f itself.
• Not copying the remaining entries after a conflict loses watches (the while i < ws.len() loop above).
• Forgetting to reset qhead to the trail length on conflict, or to the backtrack point after backtracking.
• Duplicate or complementary literals in a clause break the two-distinct-literals invariant; normalise on input.
• Adding a clause under a partial assignment: watch non-false literals first, or propagate/treat as unit at once.
• Watches are not cleaned on clause deletion; remove or lazily skip dead refs, or the lists grow.

Variants and alternatives

In production

MiniSat (and forks), CaDiCaL, Kissat, CryptoMiniSat, Glucose; Rust solvers like splr; SMT solvers (Z3, cvc5) via their SAT cores; also in constraint solvers for clausal constraints. Uses by field: chip verification through bounded model checking (chapter in the Handbook of Satisfiability); software packaging (libsolv resolves package dependencies with a SAT algorithm: README).

Implementations

Sources

• Matthew W. Moskewicz, Conor F. Madigan, Ying Zhao, Lintao Zhang, Sharad Malik, Chaff: Engineering an Efficient SAT Solver, DAC 2001. paper
• Ian P. Gent, Optimal Implementation of Watched Literals and More General Techniques, JAIR 48, 2013. paper
• Niklas Een, Niklas Sorensson, An Extensible SAT-solver, SAT 2003. paper · code
• Armin Biere, Marijn Heule, Hans van Maaren, Toby Walsh (eds.), Handbook of Satisfiability, 2nd ed., IOS Press 2021. book
• Geoffrey Chu, Aaron Harwood, Peter J. Stuckey, Cache Conscious Data Structures for Boolean Satisfiability Solvers, JSAT 6, 2009 (blocking literals; cited from memory, no link).
• Hantao Zhang, Mark Stickel, An Efficient Algorithm for Unit Propagation, AI-MATH 1996 (head/tail lists; cited from memory, no link).