logicaffeine_proof/
sym_dynamic.rs

1//! Dynamic symmetry breaking — **Symmetric Explanation Learning** (SEL), the in-search tier.
2//!
3//! Static symmetry breaking adds predicates up front (Phase 1). SEL is reactive: it watches what
4//! the solver *learns* and multiplies each learned clause by the formula's symmetry group, so the
5//! search never has to re-derive the symmetric twin of a lemma it already paid for. On a
6//! symmetry-rich UNSAT instance that is the whole game — the exponential blow-up resolution suffers
7//! is exactly the repeated rediscovery of symmetric variants.
8//!
9//! **The certification is free.** If a learned clause `C` is RUP w.r.t. the database and `σ` is an
10//! automorphism of that database, then `σ(C)` is RUP too: apply `σ` to `C`'s unit-propagation
11//! refutation and every clause it touches maps back into `σ(F) = F`. So a symmetric clause enters
12//! the proof as a plain [`ProofStep::Rup`] — DRAT/LRAT-checkable, no PR witness needed. We add a
13//! `σ(C)` only after re-confirming it is RUP against the *current* database (`rup::is_rup`), so
14//! the procedure is **fail-closed**: an amplification that does not check is silently dropped, never
15//! trusted.
16//!
17//! The loop alternates a conflict-budgeted solve ([`Solver::solve_budgeted`]) with an amplification
18//! pass over the round's learned clauses, accumulating a single RUP refutation that
19//! [`crate::pr::check_pr_refutation_fast`] verifies against the original formula alone.
20
21use std::collections::HashSet;
22
23use crate::cdcl::{BudgetedResult, Lit, Solver};
24use crate::proof::ProofStep;
25use crate::symmetry_detect::find_generators;
26
27/// The result of an SEL refutation attempt.
28#[derive(Clone, Debug)]
29pub enum SelOutcome {
30    /// Refuted, with a checkable RUP proof, the total conflicts spent, and how many clauses were
31    /// added by symmetric amplification (the lever's footprint).
32    Unsat { steps: Vec<ProofStep>, conflicts: u64, amplified: usize },
33    /// Satisfiable, with a model.
34    Sat(Vec<bool>),
35    /// Gave up within the round/budget bounds without a verdict (the procedure is deliberately
36    /// incomplete — it never returns a wrong answer, only an honest "don't know").
37    Unknown { conflicts: u64 },
38}
39
40/// Canonical clause key (sorted, deduped literal codes) for the seen-set.
41fn canon(c: &[Lit]) -> Vec<u32> {
42    let mut k: Vec<u32> = c.iter().map(|l| l.var() * 2 + u32::from(!l.is_positive())).collect();
43    k.sort_unstable();
44    k.dedup();
45    k
46}
47
48/// Add `x` as a RUP step iff it is new and genuinely RUP against the current database (fail-closed).
49fn try_add(
50    num_vars: usize,
51    db: &mut Vec<Vec<Lit>>,
52    steps: &mut Vec<ProofStep>,
53    seen: &mut HashSet<Vec<u32>>,
54    x: Vec<Lit>,
55) -> bool {
56    let key = canon(&x);
57    if seen.contains(&key) {
58        return false;
59    }
60    if crate::rup::is_rup(num_vars, db, &x) {
61        seen.insert(key);
62        db.push(x.clone());
63        steps.push(ProofStep::Rup(x));
64        true
65    } else {
66        false
67    }
68}
69
70/// Refute `clauses` with Symmetric Explanation Learning, or report SAT / Unknown. The conflict
71/// budget per round and the round cap bound the work; symmetric amplification is what makes the
72/// total conflict count collapse on symmetry-rich instances.
73pub fn sel_refute(num_vars: usize, clauses: &[Vec<Lit>]) -> SelOutcome {
74    let gens = find_generators(num_vars, clauses);
75    let mut db: Vec<Vec<Lit>> = clauses.to_vec();
76    let mut steps: Vec<ProofStep> = Vec::new();
77    let mut seen: HashSet<Vec<u32>> = db.iter().map(|c| canon(c)).collect();
78    let mut total_conflicts = 0u64;
79    let mut amplified = 0usize;
80    let mut budget = 64u64;
81    const MAX_ROUNDS: usize = 4000;
82
83    for _round in 0..MAX_ROUNDS {
84        if crate::rup::is_rup(num_vars, &db, &[]) {
85            break;
86        }
87        let mut solver = Solver::new(num_vars);
88        // Keep every learned clause for the round so the RUP trace we lift is complete; reduction
89        // would drop clauses the closing chain may depend on (the budget keeps the set small).
90        solver.set_reduce(false);
91        for c in &db {
92            solver.add_clause(c.clone());
93        }
94        let res = solver.solve_budgeted(budget);
95        total_conflicts += solver.conflicts();
96
97        match res {
98            BudgetedResult::Sat(model) => return SelOutcome::Sat(model),
99            BudgetedResult::Unsat => {
100                // Refuted within budget — append the closing learned clauses and finish.
101                let learned: Vec<Vec<Lit>> = solver.learned().iter().map(|l| l.lits.clone()).collect();
102                for c in learned {
103                    try_add(num_vars, &mut db, &mut steps, &mut seen, c);
104                }
105                break;
106            }
107            BudgetedResult::Budget => {
108                let learned: Vec<Vec<Lit>> = solver.learned().iter().map(|l| l.lits.clone()).collect();
109                let mut progress = false;
110                for c in learned {
111                    if try_add(num_vars, &mut db, &mut steps, &mut seen, c.clone()) {
112                        progress = true;
113                    }
114                    // The orbit of `c` under the generators — each image is RUP when σ is still a
115                    // symmetry of the current database, and dropped otherwise (fail-closed).
116                    for g in &gens {
117                        let image = g.apply_clause(&c);
118                        if try_add(num_vars, &mut db, &mut steps, &mut seen, image) {
119                            amplified += 1;
120                            progress = true;
121                        }
122                    }
123                }
124                if !progress {
125                    // No new lemmas at this budget — give the solver more rope before conceding.
126                    budget = budget.saturating_mul(2);
127                    if budget > 1_000_000 {
128                        break;
129                    }
130                }
131            }
132        }
133    }
134
135    if crate::pr::check_pr_refutation_fast(num_vars, clauses, &steps) {
136        SelOutcome::Unsat { steps, conflicts: total_conflicts, amplified }
137    } else {
138        SelOutcome::Unknown { conflicts: total_conflicts }
139    }
140}
141
142#[cfg(test)]
143mod tests {
144    use super::*;
145    use crate::cdcl::{SolveResult, Solver};
146
147    /// Brute-force satisfiability over `num_vars` variables — the independent oracle.
148    fn sat_brute(num_vars: usize, clauses: &[Vec<Lit>]) -> bool {
149        for mask in 0u32..(1u32 << num_vars) {
150            let model: Vec<bool> = (0..num_vars).map(|v| (mask >> v) & 1 == 1).collect();
151            if clauses.iter().all(|c| c.iter().any(|l| model[l.var() as usize] == l.is_positive())) {
152                return true;
153            }
154        }
155        false
156    }
157
158    #[test]
159    fn sel_never_reports_pigeonhole_satisfiable() {
160        // Regression guard: PHP is UNSAT at every size. A larger instance runs long enough to
161        // trigger clause-DB reduction inside the budgeted solve — which once deleted the original
162        // clauses and produced a bogus SAT. SEL must return UNSAT (or honest Unknown), NEVER SAT.
163        for n in 7..=7 {
164            let (cnf, _) = crate::families::php(n);
165            match sel_refute(cnf.num_vars, &cnf.clauses) {
166                SelOutcome::Sat(_) => panic!("PHP({n}) reported SATISFIABLE — soundness violation"),
167                SelOutcome::Unsat { steps, .. } => {
168                    assert!(crate::pr::check_pr_refutation_fast(cnf.num_vars, &cnf.clauses, &steps));
169                }
170                SelOutcome::Unknown { .. } => {}
171            }
172        }
173    }
174
175    #[test]
176    fn sel_certifies_pigeonhole() {
177        // SEL must refute PHP and the accumulated RUP proof must independently check.
178        for n in 3..=6 {
179            let (cnf, _) = crate::families::php(n);
180            match sel_refute(cnf.num_vars, &cnf.clauses) {
181                SelOutcome::Unsat { steps, .. } => {
182                    assert!(
183                        crate::pr::check_pr_refutation_fast(cnf.num_vars, &cnf.clauses, &steps),
184                        "PHP({n}) SEL proof must check"
185                    );
186                }
187                other => panic!("PHP({n}) must be refuted, got {other:?}"),
188            }
189        }
190    }
191
192    #[test]
193    fn sel_amplification_cuts_conflicts_on_pigeonhole() {
194        // The power metric: total conflicts under SEL must be strictly below plain CDCL on a
195        // symmetry-rich instance — the symmetric twins of each lemma come for free.
196        let (cnf, _) = crate::families::php(6);
197        let mut plain = Solver::new(cnf.num_vars);
198        for c in &cnf.clauses {
199            plain.add_clause(c.clone());
200        }
201        assert_eq!(plain.solve(), SolveResult::Unsat);
202        let plain_conflicts = plain.conflicts();
203
204        match sel_refute(cnf.num_vars, &cnf.clauses) {
205            SelOutcome::Unsat { conflicts, amplified, .. } => {
206                assert!(amplified > 0, "symmetry amplification must actually fire on PHP");
207                eprintln!(
208                    "PHP(6): plain CDCL = {plain_conflicts} conflicts, SEL = {conflicts} conflicts ({amplified} symmetric clauses), {:.1}x fewer",
209                    plain_conflicts as f64 / conflicts.max(1) as f64
210                );
211                assert!(
212                    conflicts < plain_conflicts,
213                    "SEL conflicts ({conflicts}) must beat plain CDCL ({plain_conflicts})"
214                );
215            }
216            other => panic!("expected refutation, got {other:?}"),
217        }
218    }
219
220    #[test]
221    fn sel_never_returns_a_wrong_verdict_random() {
222        // Soundness to the point of absurdity: over many seeded random small formulas, SEL must
223        // never contradict brute force — a `Unsat` only on truly UNSAT instances (with a checking
224        // proof), a `Sat(m)` only with a real model. `Unknown` is always permitted.
225        let mut state = 0xC0FFEE123456789Au64;
226        let mut next = || {
227            state = state.wrapping_add(0x9E3779B97F4A7C15);
228            let mut z = state;
229            z = (z ^ (z >> 30)).wrapping_mul(0xBF58476D1CE4E5B9);
230            z = (z ^ (z >> 27)).wrapping_mul(0x94D049BB133111EB);
231            z ^ (z >> 31)
232        };
233        let num_vars = 5usize;
234        for _ in 0..1500 {
235            let nclauses = next() as usize % 12;
236            let clauses: Vec<Vec<Lit>> = (0..nclauses)
237                .map(|_| {
238                    let len = 1 + (next() as usize % 3);
239                    let mut c = Vec::new();
240                    for _ in 0..len {
241                        let v = (next() as u32) % num_vars as u32;
242                        let lit = Lit::new(v, next() & 1 == 0);
243                        if !c.contains(&lit) && !c.contains(&lit.negated()) {
244                            c.push(lit);
245                        }
246                    }
247                    c
248                })
249                .filter(|c| !c.is_empty())
250                .collect();
251            let truth = sat_brute(num_vars, &clauses);
252            match sel_refute(num_vars, &clauses) {
253                SelOutcome::Unsat { steps, .. } => {
254                    assert!(!truth, "SEL refuted a satisfiable formula: {clauses:?}");
255                    assert!(
256                        crate::pr::check_pr_refutation_fast(num_vars, &clauses, &steps),
257                        "SEL Unsat proof must check: {clauses:?}"
258                    );
259                }
260                SelOutcome::Sat(model) => {
261                    assert!(truth, "SEL claimed SAT on an unsatisfiable formula: {clauses:?}");
262                    assert!(
263                        clauses.iter().all(|c| c.iter().any(|l| model[l.var() as usize] == l.is_positive())),
264                        "SEL returned an invalid model"
265                    );
266                }
267                SelOutcome::Unknown { .. } => {}
268            }
269        }
270    }
271}
logicaffeine_proof/sym_dynamic.rs

logicaffeine_proof/
sym_dynamic.rs
