logicaffeine_proof/
parity_cardinality.rs

1//! Fast refuter for the coupled **exactly-one + parity** family. An exactly-one group (an at-least-one
2//! clause plus the full at-most-one clique over its variables) forces EXACTLY one of its selectors true,
3//! so their XOR is `1` (odd). If the formula's parity substructure forces that same XOR to `0` (even),
4//! the two are inconsistent and the formula is UNSAT — the mixed obstruction neither theory sees alone.
5//!
6//! This decides it by pure GF(2) linear algebra: recover the implied XOR system, add the equation
7//! `⊕S = 1` for an exactly-one group `S`, and test the augmented system for inconsistency. That is
8//! microseconds — where the general fused route builds a whole CDCL solver with three theories (parity,
9//! cardinality, symmetry) to reach the same verdict in milliseconds.
10//!
11//! **Soundness:** the XOR equations are consequences of the formula's gadget clauses, and any model of
12//! the exactly-one clauses has `⊕S = 1`; so if `eqs ∪ {⊕S = 1}` is GF(2)-inconsistent, no model satisfies
13//! both — and the formula contains both — hence UNSAT. Conservative: fires only on a recovered
14//! exactly-one group whose augmented parity system is inconsistent; `false` otherwise.
15
16use crate::cdcl::Lit;
17use crate::xorsat::{self, XorEquation, XorOutcome};
18use std::collections::HashSet;
19
20/// Refute a coupled exactly-one + parity formula. `true` iff some exactly-one group's odd-parity
21/// requirement contradicts the formula's XOR system. Never a false refutation.
22pub fn refute(num_vars: usize, clauses: &[Vec<Lit>]) -> bool {
23    if num_vars == 0 {
24        return false;
25    }
26    let key2 = |x: u32, y: u32| if x < y { (x, y) } else { (y, x) };
27    // Binary at-most-one clauses (¬a ∨ ¬b).
28    let mut amo: HashSet<(u32, u32)> = HashSet::new();
29    for c in clauses {
30        if c.len() == 2 && !c[0].is_positive() && !c[1].is_positive() {
31            amo.insert(key2(c[0].var(), c[1].var()));
32        }
33    }
34    if amo.is_empty() {
35        return false;
36    }
37    // XOR equations implied by the formula's gadget clauses.
38    let eqs = crate::lyapunov::extract_xor(num_vars, clauses);
39    if eqs.is_empty() {
40        return false;
41    }
42    // Each all-positive clause is an at-least-one candidate; if its variables form a full at-most-one
43    // clique it is an exactly-one group, so exactly one selector is true and their XOR is 1.
44    for c in clauses {
45        if c.len() < 2 || !c.iter().all(|l| l.is_positive()) {
46            continue;
47        }
48        let set: HashSet<u32> = c.iter().map(|l| l.var()).collect();
49        if set.len() != c.len() {
50            continue; // a repeated variable
51        }
52        let mut full_clique = true;
53        'pairs: for i in 0..c.len() {
54            for j in (i + 1)..c.len() {
55                if !amo.contains(&key2(c[i].var(), c[j].var())) {
56                    full_clique = false;
57                    break 'pairs;
58                }
59            }
60        }
61        if !full_clique {
62            continue;
63        }
64        // exactly-one over S ⟹ ⊕S = 1. If the XOR system forces ⊕S = 0 the augmented system is
65        // GF(2)-inconsistent — the coupled contradiction.
66        let s: Vec<usize> = c.iter().map(|l| l.var() as usize).collect();
67        let mut augmented = eqs.clone();
68        augmented.push(XorEquation::new(s, true));
69        if matches!(xorsat::solve(&augmented, num_vars), XorOutcome::Unsat(_)) {
70            return true;
71        }
72    }
73    false
74}
logicaffeine_proof/parity_cardinality.rs

logicaffeine_proof/
parity_cardinality.rs
