elenchus_solver/sat/
mod.rs

1//! A compact, single-threaded CDCL SAT solver in `no_std`, replicating the core
2//! algorithm of varisat (jix/varisat) in a readable, lazy style.
3//!
4//! `Solver::run` drives the CDCL loop to a terminal state: it propagates, and on a
5//! conflict analyzes/backjumps/learns, otherwise it decides (`Solver::decide`).
6//! Model enumeration is a lazy [`Models`] iterator that solves **incrementally** —
7//! each `next()` adds a blocking clause and continues from the existing state
8//! rather than re-solving from scratch.
9//!
10//! **Assumptions** ([`solve_assuming`]): literals forced true before VSIDS
11//! branching. They are decided first; a contradicted assumption yields an unsat
12//! **core** (a sufficient subset of the assumptions) via MiniSat's `analyzeFinal`.
13//! This is the primitive behind incremental cores and what-if queries.
14//!
15//! Pieces mirror varisat's modules: the trail + decision levels
16//! (`prop/assignment.rs`), two-watched-literal propagation (`prop/long.rs`),
17//! 1-UIP conflict analysis with clause learning (`analyze_conflict.rs`),
18//! non-chronological backjumping, VSIDS decisions with phase saving, and
19//! assumption-based solving. Remaining infrastructure (proof/DRAT logging,
20//! clause-DB GC, restarts, the `partial_ref` context, multithreading) is
21//! intentionally omitted.
22
23use alloc::vec::Vec;
24
25mod models;
26mod solver;
27
28pub use models::{Models, all_models, models, models_upto};
29
30use solver::Solver;
31
32/// A boolean variable, identified by a dense index.
33pub type Var = u32;
34
35/// A literal: a variable plus a sign, packed as `var << 1 | negative`.
36#[derive(Clone, Copy, PartialEq, Eq, Debug)]
37pub struct SatLit(u32);
38
39impl SatLit {
40    /// A literal for `var`, positive (true) or negative (`NOT var`).
41    pub fn new(var: Var, positive: bool) -> Self {
42        SatLit((var << 1) | (!positive as u32))
43    }
44    /// The positive literal `var`.
45    pub fn positive(var: Var) -> Self {
46        Self::new(var, true)
47    }
48    /// The negative literal `NOT var`.
49    pub fn negative(var: Var) -> Self {
50        Self::new(var, false)
51    }
52    /// The underlying variable.
53    pub fn var(self) -> Var {
54        self.0 >> 1
55    }
56    /// Whether this is the negative polarity.
57    pub fn is_negative(self) -> bool {
58        self.0 & 1 == 1
59    }
60    /// The same variable with the opposite sign.
61    pub fn negate(self) -> SatLit {
62        SatLit(self.0 ^ 1)
63    }
64    /// The packed code, used directly as an index into the watch lists.
65    fn code(self) -> usize {
66        self.0 as usize
67    }
68}
69
70/// A CNF formula over `num_vars` variables.
71#[derive(Clone, Debug, Default)]
72pub struct Cnf {
73    /// Number of variables; every [`Var`] used must be `< num_vars`.
74    pub num_vars: usize,
75    /// The clauses, each a disjunction of literals (the formula is their AND).
76    pub clauses: Vec<Vec<SatLit>>,
77}
78
79impl Cnf {
80    /// An empty formula over `num_vars` variables.
81    pub fn new(num_vars: usize) -> Self {
82        Cnf {
83            num_vars,
84            clauses: Vec::new(),
85        }
86    }
87    /// Append one clause (a disjunction of literals).
88    pub fn add_clause(&mut self, lits: Vec<SatLit>) {
89        self.clauses.push(lits);
90    }
91}
92
93// --- internal state --------------------------------------------------------
94
95/// The outcome of [`solve_assuming`].
96#[derive(Clone, Debug, PartialEq, Eq)]
97pub enum Solved {
98    /// Satisfiable: a full model (`var -> bool`).
99    Sat(Vec<bool>),
100    /// Unsatisfiable under the assumptions: a *sufficient* subset of them (a core)
101    /// such that `cnf ∧ core` is unsatisfiable. Empty means the formula is
102    /// unsatisfiable regardless of the assumptions. Not guaranteed minimal.
103    Unsat(Vec<SatLit>),
104}
105
106/// Solve `cnf` with every literal in `assumptions` forced true. Returns a model,
107/// or an unsat core — a sufficient (not necessarily minimal) subset of
108/// `assumptions`. Minimize the core separately if you need 1-minimality.
109pub fn solve_assuming(cnf: &Cnf, assumptions: &[SatLit]) -> Solved {
110    let mut s = Solver::new(cnf);
111    s.assumptions = assumptions.to_vec();
112    match s.run() {
113        Ok(()) => Solved::Sat(s.model()),
114        Err(core) => Solved::Unsat(core),
115    }
116}
117
118/// Solve a CNF. Returns a full model (`var -> bool`) or `None` if unsatisfiable.
119pub fn solve(cnf: &Cnf) -> Option<Vec<bool>> {
120    match solve_assuming(cnf, &[]) {
121        Solved::Sat(model) => Some(model),
122        Solved::Unsat(_) => None,
123    }
124}
elenchus_solver/sat/mod.rs

elenchus_solver/sat/
mod.rs
