Production Case Study: Modern SAT Solvers & Package Dependency Resolution (DPLL, Unit Propagation & Two-Watched Literals)

1. From Naive Backtracking to DPLL & Boolean Constraint Propagation (BCP)

A Boolean formula in Conjunctive Normal Form (CNF) is an AND ($\wedge$) of clauses, where each clause is an OR ($\vee$) of literals ($x_i$ or $\neg x_i$). Package managers encode dependencies directly as CNF clauses:

• [email protected] requires [email protected] or [email protected] $\implies (\neg A_{1.2} \vee B_{2.0} \vee B_{2.1})$.
• [email protected] conflicts with [email protected] $\implies (\neg B_{2.0} \vee \neg B_{2.1})$.

The DPLL Algorithm (Davis–Putnam–Logemann–Loveland, 1962) enhances backtracking with Unit Propagation (Boolean Constraint Propagation / BCP): Whenever all literals in a clause except one are assigned FALSE, the remaining unassigned literal $l$ is a unit clause and must be assigned TRUE immediately. Assigning $l = \text{TRUE}$ may create new unit clauses in a cascade (fixed-point queue) before any branching decision is made.

2. How Two-Watched Literals & CDCL Work Together

When literal $l$ is assigned TRUE, its negation $\neg l$ becomes FALSE. We inspect only the watch list watches[~l]. For each clause $C$ watching $\neg l$ (with other watch $w_{other}$):

1. If $w_{other}$ is already TRUE, $C$ is satisfied—do nothing.
2. Scan the non-watched literals of $C$ for any literal $l_{new}$ that is not FALSE. If found, replace watch $\neg l$ with $l_{new}$ and move $C$ to watches[l_new] (no propagation needed).
3. If all non-watched literals are FALSE:
   • If $w_{other}$ is FALSE, $C$ is a Conflict Clause (all literals FALSE)—trigger conflict analysis / backtrack!
   • If $w_{other}$ is UNASSIGNED, $C$ is now a Unit Clause—enqueue $w_{other} = \text{TRUE}$ into the BCP trail!

In modern CDCL (Conflict-Driven Clause Learning) solvers, when a conflict occurs, the solver resolves the conflict along the implication graph to learn a new conflict clause (a nogood) and performs a non-chronological backjump directly to the decision level responsible for the conflict.

3. Complexity Matrix

4. Reference C++20 Implementation

#include <cstdint>
#include <vector>

// Compact DPLL SAT Solver with Unit Propagation and Trail-Based Undo
// Literals for variable v in [0..n-1] are encoded as: pos = 2*v, neg = 2*v ^ 1
class DpllSatSolver {
    int num_vars;
    std::vector<std::vector<int>> clauses;
    std::vector<std::vector<int>> watches; // watches[lit] = list of clause IDs watching lit
    std::vector<std::int8_t> val;          // -1: unassigned, 0: false, 1: true (indexed by literal)
    std::vector<int> trail;                // Stack of assigned literals
    int qhead = 0;                         // BCP queue pointer inside trail

    bool enqueue(int lit) {
        if (val[lit] == 1) return true;    // Already satisfied
        if (val[lit] == 0) return false;   // Conflict!
        val[lit] = 1;
        val[lit ^ 1] = 0;
        trail.push_back(lit);
        return true;
    }

    // Boolean Constraint Propagation (BCP) using Two-Watched Literals
    bool propagate() {
        while (qhead < static_cast<int>(trail.size())) {
            int falsified_lit = trail[qhead++] ^ 1; // ~lit just became FALSE
            auto& wl = watches[falsified_lit];
            std::size_t j = 0;
            for (std::size_t i = 0; i < wl.size(); ++i) {
                int cid = wl[i];
                auto& c = clauses[cid];
                // Ensure c[1] is the falsified watched literal, c[0] is the other watch
                if (c[0] == falsified_lit) std::swap(c[0], c[1]);

                if (val[c[0]] == 1) { // Other watch is already TRUE -> clause satisfied
                    wl[j++] = cid;
                    continue;
                }
                // Try to find a replacement watch in c[2..end] that is not FALSE
                bool moved = false;
                for (std::size_t k = 2; k < c.size(); ++k) {
                    if (val[c[k]] != 0) {
                        std::swap(c[1], c[k]);
                        watches[c[1]].push_back(cid);
                        moved = true;
                        break;
                    }
                }
                if (moved) continue; // Watch moved to c[1]; do NOT keep cid in wl

                // No replacement found: keep watching falsified_lit and unit-propagate c[0]
                wl[j++] = cid;
                if (!enqueue(c[0])) {
                    while (++i < wl.size()) wl[j++] = wl[i];
                    wl.resize(j);
                    return false; // Conflict!
                }
            }
            wl.resize(j);
        }
        return true;
    }

    void backtrack_to(int trail_pos) {
        while (static_cast<int>(trail.size()) > trail_pos) {
            int lit = trail.back();
            val[lit] = -1;
            val[lit ^ 1] = -1;
            trail.pop_back();
        }
        qhead = trail_pos; // Notice: ZERO watch-list updates required on backtrack!
    }

public:
    explicit DpllSatSolver(int n) : num_vars(n), watches(2 * n), val(2 * n, -1) {}

    bool add_clause(std::vector<int> lits) {
        if (lits.empty()) return false;
        if (lits.size() == 1) return enqueue(lits[0]) && propagate();
        int cid = static_cast<int>(clauses.size());
        watches[lits[0]].push_back(cid);
        watches[lits[1]].push_back(cid);
        clauses.push_back(std::move(lits));
        return true;
    }

    bool solve() {
        if (!propagate()) return false;
        // Find first unassigned variable
        int branch_var = -1;
        for (int v = 0; v < num_vars; ++v) {
            if (val[2 * v] == -1) { branch_var = v; break; }
        }
        if (branch_var == -1) return true; // All variables assigned without conflict -> SAT!

        int saved_pos = static_cast<int>(trail.size());
        for (int polarity : {0, 1}) {
            if (enqueue(2 * branch_var ^ polarity) && solve()) return true;
            backtrack_to(saved_pos);
        }
        return false;
    }
};