logicaffeine_proof/
twosat.rs

1//! 2-SAT in linear time via the implication graph + strongly-connected components.
2//!
3//! A clause of at most two literals `(a ∨ b)` is equivalent to the two implications `¬a → b` and
4//! `¬b → a`. Over all clauses these form an implication graph on the `2n` literals; the formula is
5//! unsatisfiable **iff some variable `x` lies in the same SCC as `¬x`** (so `x → ¬x` and `¬x → x`,
6//! forcing `x` both ways). Otherwise a model is read off the SCC condensation's topological order.
7//! Kosaraju's two-pass SCC makes the whole decision O(n+m) — and certified: a model is re-checkable,
8//! and an `Unsat` returns the conflicting variable, whose mutual implication [`is_refutation`]
9//! independently re-derives by reachability.
10
11/// A literal: variable `var`, positive when `pos`.
12#[derive(Clone, Copy, Debug, PartialEq, Eq)]
13pub struct Lit {
14    /// The variable index (`0..num_vars`).
15    pub var: usize,
16    /// `true` for `x`, `false` for `¬x`.
17    pub pos: bool,
18}
19
20impl Lit {
21    /// Positive literal `x`.
22    pub fn pos(var: usize) -> Self {
23        Lit { var, pos: true }
24    }
25    /// Negative literal `¬x`.
26    pub fn neg(var: usize) -> Self {
27        Lit { var, pos: false }
28    }
29}
30
31/// The outcome of solving a 2-SAT instance.
32#[derive(Clone, Debug, PartialEq, Eq)]
33pub enum TwoSatOutcome {
34    /// Satisfiable, with an assignment over `0..num_vars` (re-checkable via [`satisfies`]).
35    Sat(Vec<bool>),
36    /// Unsatisfiable: the variable forced both true and false (`x` and `¬x` in one SCC). Its mutual
37    /// implication is re-checkable via [`is_refutation`].
38    Unsat(usize),
39}
40
41// A literal's node in the implication graph: `2*var + pos`. The negation flips the low bit.
42#[inline]
43fn node(l: Lit) -> usize {
44    2 * l.var + l.pos as usize
45}
46#[inline]
47fn neg_node(n: usize) -> usize {
48    n ^ 1
49}
50
51fn dfs1(v: usize, adj: &[Vec<usize>], visited: &mut [bool], order: &mut Vec<usize>) {
52    visited[v] = true;
53    for &u in &adj[v] {
54        if !visited[u] {
55            dfs1(u, adj, visited, order);
56        }
57    }
58    order.push(v);
59}
60
61fn dfs2(v: usize, radj: &[Vec<usize>], comp: &mut [usize], c: usize) {
62    comp[v] = c;
63    for &u in &radj[v] {
64        if comp[u] == usize::MAX {
65            dfs2(u, radj, comp, c);
66        }
67    }
68}
69
70/// Decide a 2-SAT instance (`clauses` of two literals each — a unit clause is `(a, a)`). Returns a
71/// satisfying assignment, or the variable whose SCC contains both polarities.
72pub fn solve(clauses: &[(Lit, Lit)], num_vars: usize) -> TwoSatOutcome {
73    let nn = 2 * num_vars;
74    let mut adj = vec![Vec::new(); nn];
75    let mut radj = vec![Vec::new(); nn];
76    let mut edge = |from: usize, to: usize| {
77        adj[from].push(to);
78        radj[to].push(from);
79    };
80    for &(a, b) in clauses {
81        if a.var >= num_vars || b.var >= num_vars {
82            continue;
83        }
84        // (a ∨ b): ¬a → b and ¬b → a.
85        edge(neg_node(node(a)), node(b));
86        edge(neg_node(node(b)), node(a));
87    }
88    // Kosaraju: finish-order pass, then components in reverse finish order (topological).
89    let mut visited = vec![false; nn];
90    let mut order = Vec::with_capacity(nn);
91    for v in 0..nn {
92        if !visited[v] {
93            dfs1(v, &adj, &mut visited, &mut order);
94        }
95    }
96    let mut comp = vec![usize::MAX; nn];
97    let mut c = 0;
98    for &v in order.iter().rev() {
99        if comp[v] == usize::MAX {
100            dfs2(v, &radj, &mut comp, c);
101            c += 1;
102        }
103    }
104    // Conflict: x and ¬x share an SCC.
105    for v in 0..num_vars {
106        if comp[2 * v] == comp[2 * v + 1] {
107            return TwoSatOutcome::Unsat(v);
108        }
109    }
110    // Model: the literal whose SCC is later in topological order (larger Kosaraju id) is true.
111    let assignment = (0..num_vars)
112        .map(|v| comp[node(Lit::pos(v))] > comp[node(Lit::neg(v))])
113        .collect();
114    TwoSatOutcome::Sat(assignment)
115}
116
117/// Re-check a satisfying assignment: every clause has a true literal.
118pub fn satisfies(clauses: &[(Lit, Lit)], assignment: &[bool]) -> bool {
119    let holds = |l: Lit| l.var < assignment.len() && assignment[l.var] == l.pos;
120    clauses.iter().all(|&(a, b)| holds(a) || holds(b))
121}
122
123/// Re-check an `Unsat` witness: in the implication graph, `x` reaches `¬x` *and* `¬x` reaches `x`
124/// (mutual implication ⇒ no value of `x` is consistent). A solver-free certificate.
125pub fn is_refutation(clauses: &[(Lit, Lit)], num_vars: usize, var: usize) -> bool {
126    if var >= num_vars {
127        return false;
128    }
129    let nn = 2 * num_vars;
130    let mut adj = vec![Vec::new(); nn];
131    for &(a, b) in clauses {
132        if a.var < num_vars && b.var < num_vars {
133            adj[neg_node(node(a))].push(node(b));
134            adj[neg_node(node(b))].push(node(a));
135        }
136    }
137    let reaches = |from: usize, to: usize| {
138        let mut seen = vec![false; nn];
139        let mut stack = vec![from];
140        seen[from] = true;
141        while let Some(u) = stack.pop() {
142            if u == to {
143                return true;
144            }
145            for &w in &adj[u] {
146                if !seen[w] {
147                    seen[w] = true;
148                    stack.push(w);
149                }
150            }
151        }
152        from == to
153    };
154    let xt = node(Lit::pos(var));
155    let xf = node(Lit::neg(var));
156    reaches(xt, xf) && reaches(xf, xt)
157}
158
159#[cfg(test)]
160mod tests {
161    use super::*;
162
163    fn cl(a: Lit, b: Lit) -> (Lit, Lit) {
164        (a, b)
165    }
166
167    #[test]
168    fn simple_satisfiable_instance() {
169        // (x0 ∨ x1) ∧ (¬x0 ∨ x1) ∧ (¬x1 ∨ x2) — satisfiable.
170        let cs = vec![
171            cl(Lit::pos(0), Lit::pos(1)),
172            cl(Lit::neg(0), Lit::pos(1)),
173            cl(Lit::neg(1), Lit::pos(2)),
174        ];
175        match solve(&cs, 3) {
176            TwoSatOutcome::Sat(a) => assert!(satisfies(&cs, &a), "model must satisfy: {a:?}"),
177            o => panic!("expected Sat, got {o:?}"),
178        }
179    }
180
181    #[test]
182    fn forced_contradiction_is_unsat() {
183        // (x0)∧(¬x0) as units: (x0∨x0) and (¬x0∨¬x0) ⇒ x0 forced both ways.
184        let cs = vec![cl(Lit::pos(0), Lit::pos(0)), cl(Lit::neg(0), Lit::neg(0))];
185        match solve(&cs, 1) {
186            TwoSatOutcome::Unsat(v) => {
187                assert_eq!(v, 0);
188                assert!(is_refutation(&cs, 1, v), "refutation must re-check");
189            }
190            o => panic!("expected Unsat, got {o:?}"),
191        }
192    }
193
194    #[test]
195    fn implication_cycle_is_unsat() {
196        // x0→x1, x1→¬x0, ¬x0→x0 collapses {x0,¬x0,x1} — classic 2-SAT contradiction.
197        // (¬x0∨x1)=x0→x1 ; (¬x1∨¬x0)=x1→¬x0 ; (x0∨x0)=¬x0→x0.
198        let cs = vec![
199            cl(Lit::neg(0), Lit::pos(1)),
200            cl(Lit::neg(1), Lit::neg(0)),
201            cl(Lit::pos(0), Lit::pos(0)),
202        ];
203        match solve(&cs, 2) {
204            TwoSatOutcome::Unsat(v) => assert!(is_refutation(&cs, 2, v)),
205            o => panic!("expected Unsat, got {o:?}"),
206        }
207    }
208
209    #[test]
210    fn empty_is_satisfiable() {
211        assert!(matches!(solve(&[], 3), TwoSatOutcome::Sat(_)));
212    }
213
214    #[test]
215    fn matches_brute_force_on_random_2sat() {
216        let mut s: u64 = 0x2545F4914F6CDD1D;
217        let mut next = || {
218            s ^= s << 13;
219            s ^= s >> 7;
220            s ^= s << 17;
221            s
222        };
223        for _ in 0..500 {
224            let num_vars = (next() % 6) as usize + 1;
225            let m = (next() % 10) as usize + 1;
226            let lit = |r: u64, nv: usize| Lit {
227                var: (r as usize) % nv,
228                pos: (r >> 8) & 1 == 1,
229            };
230            let cs: Vec<(Lit, Lit)> = (0..m)
231                .map(|_| (lit(next(), num_vars), lit(next(), num_vars)))
232                .collect();
233            let brute_sat = (0..(1u32 << num_vars)).any(|mask| {
234                let a: Vec<bool> = (0..num_vars).map(|i| (mask >> i) & 1 == 1).collect();
235                satisfies(&cs, &a)
236            });
237            match solve(&cs, num_vars) {
238                TwoSatOutcome::Sat(a) => {
239                    assert!(brute_sat, "we said SAT, brute force UNSAT: {cs:?}");
240                    assert!(satisfies(&cs, &a), "model is wrong: {a:?} for {cs:?}");
241                }
242                TwoSatOutcome::Unsat(v) => {
243                    assert!(!brute_sat, "we said UNSAT, brute force SAT: {cs:?}");
244                    assert!(is_refutation(&cs, num_vars, v), "bogus refutation var={v}");
245                }
246            }
247        }
248    }
249}
logicaffeine_proof/twosat.rs

logicaffeine_proof/
twosat.rs
