Boolean satisfiability — the original hard problem

SAT is famously hard. Industrial solvers are famously good. The right move is to encode and dispatch.

Boolean satisfiability — does this logical formula have a true assignment — was the first problem proven NP-complete (Cook, 1971). Every other NP-complete problem reduces to it. By every theoretical measure, SAT is hard. And yet modern industrial SAT solvers routinely handle instances with millions of variables in seconds. The trick is conflict-driven clause learning (CDCL), a search strategy that learns from each dead-end and prunes the future search aggressively. Modern SAT solvers are the product of three decades of competitive benchmarking and engineering refinement. For business problems that can be encoded as logical constraints — scheduling, configuration, verification, planning — the right path is to encode in standard format (DIMACS) and call a solver. Rust has splr (pure Rust) and varisat. For maximum performance, the C++ solver CaDiCaL via FFI is hard to beat.

splr accepts CNF as a Vec<Vec<i32>> — positive integers are variables, negatives are negations. The solver returns a satisfying assignment or UNSAT. Encode your configuration validator this way and let three decades of CDCL engineering do the search.

use splr::*;

fn satisfy(clauses: Vec<Vec<i32>>) -> Option<Vec<i32>> {
    let mut solver = Solver::try_from((SolverConfig::default(), clauses.as_ref()))
        .expect("valid CNF");
    match solver.solve() {
        Ok(Certificate::SAT(assignment)) => Some(assignment),
        Ok(Certificate::UNSAT) => None,
        Err(_) => None,
    }
}

SAT's input is a logical formula written in Conjunctive Normal Form (CNF) — a giant AND of ORs. The Vec<Vec<i32>> shape is the DIMACS convention, the standard format SAT solvers everywhere accept. Each variable is encoded as a positive integer (1, 2, 3, …). A positive integer means "this variable is true" and its negative means "this variable is false." A literal is a variable or its negation — a positive or negative integer in the encoding. Each inner Vec<i32> is a clause: a list of literals joined by OR. The outer Vec is the formula: all those clauses joined by AND. A formula is satisfiable if there is some assignment of true / false to each variable that makes every clause come out true.

// DIMACS-style encoding — the standard SAT solver input format:
//
//    1  →  variable x₁ is TRUE
//   -1  →  variable x₁ is FALSE
//    2  →  variable x₂ is TRUE
//   -2  →  variable x₂ is FALSE
//   ...
//
// Each inner Vec is a clause — an OR of literals.
// The outer Vec is the formula — an AND of clauses.

let formula: Vec<Vec<i32>> = vec![
    vec![ 1, -2],       // (x₁  ∨  ¬x₂)
    vec![-1,  3],       // (¬x₁ ∨  x₃)
    vec![ 2,  3],       // (x₂  ∨  x₃)
];

// The whole formula, expanded:
//
//   (x₁ ∨ ¬x₂)  ∧  (¬x₁ ∨ x₃)  ∧  (x₂ ∨ x₃)
//
// "Find a TRUE/FALSE choice for each variable such that
//  every clause has at least one literal that came out true."

The solver returns Option<Vec<i32>>. Some(assignment) means a satisfying assignment exists; None means no assignment can make the formula true. The returned vector uses the same DIMACS convention: each entry is a literal, positive for "this variable came out true," negative for "this variable came out false." For a formula over n variables, the vector has n entries — one per variable, in order. Underneath, splr returns a richer Certificate enum (SAT(Vec<i32>) or UNSAT); the wrapper collapses both to Option because most callers do not need the richer distinction.

// One satisfying assignment for the formula above:
let solution: Vec<i32> = vec![1, -2, 3];
//                            ─  ──  ─
//                            │  │   └── x₃ is true
//                            │  └────── x₂ is false
//                            └───────── x₁ is true

// Verify it by hand:
//   (x₁ ∨ ¬x₂)  =  (true  ∨ true)  =  true   ✓
//   (¬x₁ ∨ x₃)  =  (false ∨ true)  =  true   ✓
//   (x₂ ∨ x₃)   =  (false ∨ true)  =  true   ✓
//
// Every clause has at least one literal that came out true → formula satisfied.


// A formula can be UNSAT — no assignment works:
let contradiction: Vec<Vec<i32>> = vec![
    vec![ 1],          // (x₁)       →  forces x₁ = true
    vec![-1],          // (¬x₁)      →  forces x₁ = false
];
// satisfy(contradiction)  →  None    (Certificate::UNSAT inside the solver)


// What the solver actually does:
//
// Brute force would try all 2ⁿ assignments — infeasible past about 30
// variables.  Modern CDCL solvers (Conflict-Driven Clause Learning)
// search far smarter: they pick a variable, assume true, propagate
// implications, learn from dead-ends, and prune the search aggressively.
// Real-world configuration and verification instances with millions of
// variables routinely solve in seconds.

The page-23 code is abstract — Vec<Vec<i32>> of integer literals. Where do business problems with that shape actually come from? The most common case is configuration validation. Imagine a product with five toggleable features: SSO, user_sync, audit, Pro, Enterprise. Map each to a positive integer — 1 = SSO, 2 = user_sync, 3 = audit, 4 = Pro, 5 = Enterprise — and the product's business rules become clauses. "If SSO is on, then user_sync must be on" is the implication SSO → user_sync, which in CNF becomes ¬SSO ∨ user_sync — the clause [-1, 2]. "Pro and Enterprise are mutually exclusive" becomes ¬Pro ∨ ¬Enterprise — clause [-4, -5]. "Audit requires Pro or Enterprise" becomes ¬audit ∨ Pro ∨ Enterprise — clause [-3, 4, 5]. Three English rules, three clauses. Ask the solver to satisfy them and you get one valid configuration back. Add the customer's requested settings as unit clauses ("they want audit on" → [3]) and the solver searches for a configuration that satisfies both the rules and the request, or returns UNSAT when the request is impossible. Other problems that fit the same shape: shift scheduling (each shift has a list of people who could cover it), package dependency resolution (each package needs one of several compatible versions of a dependency), software verification (each branch decision is a variable, the bug condition is a target), and puzzles like Sudoku.

// Five product features → five Boolean variables, numbered 1-5:
//
//   1  →  SSO
//   2  →  user_sync
//   3  →  audit
//   4  →  Pro
//   5  →  Enterprise

let rules: Vec<Vec<i32>> = vec![
    vec![-1,  2     ],     // ¬SSO  ∨  user_sync
    vec![-4, -5     ],     // ¬Pro  ∨  ¬Enterprise
    vec![-3,  4,  5 ],     // ¬audit ∨ Pro ∨ Enterprise
];
//
//   English rule                       CNF clause
//   ──────────────────────────────     ──────────────
//   SSO → user_sync                    ¬SSO ∨ user_sync         [-1, 2]
//   NOT both Pro and Enterprise        ¬Pro ∨ ¬Enterprise       [-4, -5]
//   audit → Pro ∨ Enterprise           ¬audit ∨ Pro ∨ Enterprise [-3, 4, 5]


// Ask the solver: is any configuration valid?
let answer = satisfy(rules.clone());
// → Some([..])      A valid assignment.  Many configurations satisfy
//                    these rules — including "every feature off."


// Add the customer's request as unit clauses (one literal each):
let mut with_request = rules.clone();
with_request.push(vec![3]);     // "we want audit on"

let answer = satisfy(with_request);
// → Some([-1, -2, 3, 4, -5])
//        SSO off, user_sync off, audit on, Pro on, Enterprise off.
//        The audit request forced clause 3 to pick Pro or Enterprise;
//        clause 2 says they can't both be on; the solver picked Pro.


// Try a request that violates the rules:
let mut impossible = rules.clone();
impossible.push(vec![4]);       // want Pro
impossible.push(vec![5]);       // AND want Enterprise

let answer = satisfy(impossible);
// → None      Certificate::UNSAT — clause 2 says Pro and Enterprise are
//                                  mutually exclusive, so this is impossible.


// The English → CNF translation table:
//
//   English                          Logic                       CNF
//   ─────────────────────────        ──────────────              ──────────
//   "if A then B"                    ¬A ∨ B                      [-A, B]
//   "A is required"                  A                           [A]
//   "not A"                          ¬A                          [-A]
//   "A or B"                         A ∨ B                       [A, B]
//   "not both A and B"               ¬A ∨ ¬B                     [-A, -B]
//   "A and B both required"          A ∧ B                       [A], [B]
//   "exactly one of A, B"            (A ∨ B) ∧ ¬(A ∧ B)          [A, B], [-A, -B]
//
// Once a business rule has been written down in plain English, the
// translation to clauses is mechanical.  The hard part is *spotting*
// that a problem has this shape — page 38 catalogs the lookalikes.

In plain terms

SAT is the canonical hard problem. Cook proved it NP-complete in 1971; every other NP-complete problem reduces to it. By every theoretical measure it is genuinely hard. And yet, decades of engineering have produced industrial SAT solvers that crack instances with millions of variables in seconds. This contradiction — theoretically hard, practically tractable on real inputs — is one of the most important lessons in applied complexity.

The reason modern SAT solvers work is that real-world SAT instances almost always have hidden structure that adversarial worst-case instances do not. Configuration constraints have local clustering. Scheduling problems have weak coupling between distant variables. Verification queries have natural decompositions. The conflict-driven clause learning (CDCL) architecture of modern solvers exploits this structure by learning from every dead-end and pruning the search aggressively.

The first business implication: when a problem can be encoded as Boolean logic — configuration validation, planning under constraints, verification, model checking — the right move is to encode it as CNF (the standard SAT format) and hand it to a solver. Do not write your own search. Modern SAT solvers are the product of three decades of competitive benchmarking and tens of thousands of engineering hours. You will not beat them in a quarter.

The second implication: even though SAT is "hard" in the worst case, the practical cost of using a SAT solver on real problems is often less than the cost of writing custom search code. Reach for the solver, see if it works, only commit to a bespoke approach if it does not.

In Rust, splr is the pure-Rust CDCL solver. Varisat is another option. For maximum performance, the C++ solver CaDiCaL is the current state of the art and is callable from Rust via FFI. All of them accept DIMACS-format input and return either a satisfying assignment or UNSAT.

The teaching: "NP-complete in theory" and "tractable in practice with the right solver" are both true for SAT. Plan around both.