1use std::collections::HashMap;
27use std::collections::HashSet;
28
29use crate::cdcl::{BudgetedResult, Lit, SolveResult, Solver};
30use crate::lyapunov::{auto_collapse, extract_xor, AutoCollapse};
31use crate::proof::ProofStep;
32use crate::xor_engine::IncXor;
33use crate::xorsat::XorOutcome;
34use crate::ProofExpr;
35
36#[derive(Clone, Copy, Debug, PartialEq, Eq)]
45pub enum Route {
46 TwoSat,
47 Horn,
48 Lll,
49 Pigeonhole,
50 CuttingPlanes,
51 Parity,
52 ExactCover,
57 ModP,
58 ModM,
59 Collapse,
60 HybridXor,
61 Sos,
62 Nullstellensatz,
63 SymmetryBreak,
64 NestedSymmetry,
65 Sel,
66 LocalSymmetry,
67 OrbitalBranch,
68 SymmetricProbe,
69 SymmetricBinary,
70 OrbitWeightQuotient,
71 SymmetryPropagate,
72 SymmetricComponent,
73 SymmetrySimplify,
74 SemanticSymmetry,
75 AlmostSymmetry,
76 DeclaredSymmetry,
77 RecursiveBreak,
78 Incompressible,
81 Component,
84 BoundedVarElim,
88 EquivLit,
92 TreeWidth,
96 Cdcl,
97}
98
99#[derive(Clone, Debug)]
101pub enum Answer {
102 Sat(Vec<bool>),
103 Unsat,
104}
105
106#[derive(Clone, Debug)]
108pub struct Solved {
109 pub answer: Answer,
110 pub via: Route,
111 pub proof: Vec<ProofStep>,
114 pub conflicts: u64,
116}
117
118impl Solved {
119 fn unsat(via: Route) -> Self {
120 Solved { answer: Answer::Unsat, via, proof: Vec::new(), conflicts: 0 }
121 }
122}
123
124pub fn solve_structured(num_vars: usize, clauses: &[Vec<Lit>]) -> Solved {
128 structured_prefix(num_vars, clauses).unwrap_or_else(|| cdcl_fallback(num_vars, clauses))
129}
130
131pub fn structured_prefix(num_vars: usize, clauses: &[Vec<Lit>]) -> Option<Solved> {
136 if let Some(binary) = as_two_sat(clauses) {
138 return Some(match crate::twosat::solve(&binary, num_vars) {
139 crate::twosat::TwoSatOutcome::Sat(model) => {
140 Solved { answer: Answer::Sat(model), via: Route::TwoSat, proof: Vec::new(), conflicts: 0 }
141 }
142 crate::twosat::TwoSatOutcome::Unsat(_) => Solved::unsat(Route::TwoSat),
143 });
144 }
145
146 if let Some(horn) = as_horn(clauses) {
148 return Some(match crate::hornsat::solve(&horn, num_vars) {
149 crate::hornsat::HornOutcome::Sat(model) => {
150 Solved { answer: Answer::Sat(model), via: Route::Horn, proof: Vec::new(), conflicts: 0 }
151 }
152 crate::hornsat::HornOutcome::Unsat(_) => Solved::unsat(Route::Horn),
153 });
154 }
155
156 if !clauses.is_empty() && crate::lll::lll_certifies_sat(clauses).is_some() {
160 let budget = 1000 + 64 * clauses.len();
161 if let Some(model) = crate::lll::moser_tardos_witness(num_vars, clauses, 0x10C0_5EED_C0DE_F00D, budget)
162 {
163 if clauses
165 .iter()
166 .all(|c| c.iter().any(|l| model.get(l.var() as usize).copied().unwrap_or(false) == l.is_positive()))
167 {
168 return Some(Solved { answer: Answer::Sat(model), via: Route::Lll, proof: Vec::new(), conflicts: 0 });
169 }
170 }
171 }
172
173 if let Some(expr) = cnf_to_expr(clauses) {
175 if crate::pigeonhole::decide_pigeonhole_unsat(&expr) {
176 return Some(Solved::unsat(Route::Pigeonhole));
177 }
178 if crate::pseudo_boolean::refute_clausal(&expr) {
179 return Some(Solved::unsat(Route::CuttingPlanes));
180 }
181 if crate::xorsat::refute_via_parity(&expr) {
182 return Some(Solved::unsat(Route::Parity));
183 }
184 }
185
186 if let Some(solved) = exact_cover_route(num_vars, clauses) {
191 return Some(solved);
192 }
193
194 if let Some(solved) = modp_route(num_vars, clauses) {
199 return Some(solved);
200 }
201
202 match auto_collapse(num_vars, clauses) {
204 AutoCollapse::None => {}
205 _ => return Some(Solved::unsat(Route::Collapse)),
207 }
208
209 if let Some(solved) = hybrid_xor(num_vars, clauses) {
213 return Some(solved);
214 }
215
216 if num_vars <= 6 && crate::sos::sos_refutes(num_vars, clauses) {
221 return Some(Solved::unsat(Route::Sos));
222 }
223
224 if num_vars <= 12 {
230 for d in 2..=num_vars.min(3) {
231 if crate::polycalc::nullstellensatz_refutes(num_vars, clauses, d) {
232 return Some(Solved::unsat(Route::Nullstellensatz));
233 }
234 }
235 }
236
237 None
238}
239
240fn exact_cover_route(num_vars: usize, clauses: &[Vec<Lit>]) -> Option<Solved> {
250 use std::collections::HashSet;
251 let mut amo: HashSet<(u32, u32)> = HashSet::new();
252 for c in clauses {
253 if c.len() == 2 && c.iter().all(|l| !l.is_positive()) {
254 let (a, b) = (c[0].var(), c[1].var());
255 amo.insert((a.min(b), a.max(b)));
256 }
257 }
258 if amo.is_empty() {
259 return None;
260 }
261 let mut groups: Vec<Vec<u32>> = Vec::new();
262 for c in clauses {
263 if c.len() < 2 || !c.iter().all(|l| l.is_positive()) {
264 continue;
265 }
266 let mut g: Vec<u32> = c.iter().map(|l| l.var()).collect();
267 g.sort_unstable();
268 g.dedup();
269 if g.len() != c.len() {
270 continue;
271 }
272 let full_amo = (0..g.len())
273 .all(|i| (i + 1..g.len()).all(|j| amo.contains(&(g[i], g[j]))));
274 if full_amo {
275 groups.push(g);
276 }
277 }
278 if groups.len() < 2 {
279 return None; }
281 let eqs: Vec<crate::xorsat::XorEquation> = groups
283 .iter()
284 .map(|g| crate::xorsat::XorEquation::new(g.iter().map(|&v| v as usize).collect::<Vec<_>>(), true))
285 .collect();
286 if let crate::xorsat::XorOutcome::Unsat(refutation) = crate::xorsat::solve(&eqs, num_vars) {
287 if crate::xorsat::is_refutation(&eqs, num_vars, &refutation) {
288 return Some(Solved::unsat(Route::ExactCover));
289 }
290 }
291 for p in [3u64, 5] {
293 let meqs: Vec<crate::modp::ModpEquation> = groups
294 .iter()
295 .map(|g| {
296 crate::modp::ModpEquation::new(
297 g.iter().map(|&v| (v as usize, 1u64)).collect::<Vec<_>>(),
298 1,
299 )
300 })
301 .collect();
302 if let crate::modp::ModpOutcome::Unsat(combo) = crate::modp::solve(&meqs, num_vars, p) {
303 if crate::modp::is_refutation(&meqs, num_vars, p, &combo) {
304 return Some(Solved::unsat(Route::ExactCover));
305 }
306 }
307 }
308 None
309}
310
311fn cdcl_fallback(num_vars: usize, clauses: &[Vec<Lit>]) -> Solved {
315 let mut solver = Solver::new(num_vars);
316 for c in clauses {
317 solver.add_clause(c.clone());
318 }
319 for c in mine_clauses(num_vars, clauses) {
320 solver.add_clause(c);
321 }
322 match solver.solve() {
323 SolveResult::Sat(model) => {
324 Solved { answer: Answer::Sat(model), via: Route::Cdcl, proof: Vec::new(), conflicts: solver.conflicts() }
325 }
326 SolveResult::Unsat => {
327 let proof = solver.learned().iter().map(|lc| ProofStep::Rup(lc.lits.clone())).collect();
328 Solved { answer: Answer::Unsat, via: Route::Cdcl, proof, conflicts: solver.conflicts() }
329 }
330 }
331}
332
333pub fn solve_comprehensive(num_vars: usize, clauses: &[Vec<Lit>]) -> Solved {
341 if let Some(s) = structured_prefix(num_vars, clauses) {
342 return s;
343 }
344 if let crate::inprocess::EquivResult::Unsat(steps) = crate::inprocess::equivalent_literal_scc(num_vars, clauses) {
352 return Solved { answer: Answer::Unsat, via: Route::EquivLit, proof: steps, conflicts: 0 };
353 }
354 let (reduced, steps) = crate::inprocess::bve(num_vars, clauses);
355 if reduced.iter().any(|c| c.is_empty()) {
356 return Solved { answer: Answer::Unsat, via: Route::BoundedVarElim, proof: steps, conflicts: 0 };
357 }
358 if let Some(steps) = crate::inprocess::bucket_elimination_refute(num_vars, clauses, 12) {
362 return Solved { answer: Answer::Unsat, via: Route::TreeWidth, proof: steps, conflicts: 0 };
363 }
364 if crate::ait::incompressibility_gate(num_vars, clauses).is_some() {
369 let mut solved = cdcl_fallback(num_vars, clauses);
370 solved.via = Route::Incompressible;
371 return solved;
372 }
373 if let Some(s) = symmetric_component_solve(num_vars, clauses) {
378 return s;
379 }
380 if let Some(s) = symmetry_via_simplification_solve(num_vars, clauses) {
384 return s;
385 }
386 if let Some(s) = orbit_weight_quotient_solve(num_vars, clauses) {
390 return s;
391 }
392 if num_vars <= 16 {
395 for d in 2..=num_vars.min(3) {
396 if crate::polycalc::nullstellensatz_refutes(num_vars, clauses, d) {
397 return Solved::unsat(Route::Nullstellensatz);
398 }
399 }
400 }
401 if let Some(s) = dynamic_sel(num_vars, clauses) {
406 return s;
407 }
408 if let Some(s) = symmetric_probe_solve(num_vars, clauses) {
412 return s;
413 }
414 if let Some(s) = symmetric_binary_inference_solve(num_vars, clauses) {
418 return s;
419 }
420 if let Some(s) = nested_symmetry_solve(num_vars, clauses) {
424 return s;
425 }
426 if let Some(s) = orbital_branch_solve(num_vars, clauses) {
430 return s;
431 }
432 if let Some(s) = symmetry_propagate_solve(num_vars, clauses) {
435 return s;
436 }
437 if let Some(s) = symmetry_break_solve(num_vars, clauses) {
440 return s;
441 }
442 if let Some(s) = local_symmetry_solve(num_vars, clauses) {
446 return s;
447 }
448 if let Some(s) = semantic_symmetry_solve(num_vars, clauses) {
452 return s;
453 }
454 if let Some(s) = almost_symmetry_solve(num_vars, clauses) {
458 return s;
459 }
460 if let Some(s) = recursive_break_solve(num_vars, clauses) {
464 return s;
465 }
466 if let Some(s) = fused_modular_solve(num_vars, clauses) {
472 return s;
473 }
474 match crate::affine::affine_canonicalize(num_vars, clauses) {
480 crate::affine::AffineCanon::Refuted(drat) => {
481 let proof = drat.map(|res| res.into_iter().map(ProofStep::Rup).collect()).unwrap_or_default();
485 return Solved { answer: Answer::Unsat, via: Route::Parity, proof, conflicts: 0 };
486 }
487 crate::affine::AffineCanon::Canonical(canon) => {
488 let sub = cdcl_fallback(canon.num_vars, &canon.clauses);
491 return match sub.answer {
492 Answer::Unsat => Solved { answer: Answer::Unsat, via: sub.via, proof: Vec::new(), conflicts: sub.conflicts },
493 Answer::Sat(model) => {
494 let lifted = canon.lift(&model);
495 if clauses.iter().all(|c| c.iter().any(|l| lifted[l.var() as usize] == l.is_positive())) {
497 Solved { answer: Answer::Sat(lifted), via: sub.via, proof: Vec::new(), conflicts: sub.conflicts }
498 } else {
499 cdcl_fallback(num_vars, clauses) }
501 }
502 };
503 }
504 crate::affine::AffineCanon::Unchanged => {}
505 }
506 match crate::affine_gfp::affine_p_canonicalize(num_vars, clauses) {
511 crate::affine_gfp::AffinePCanon::Refuted(drat) => {
512 let proof = drat.map(|res| res.into_iter().map(ProofStep::Rup).collect()).unwrap_or_default();
513 return Solved { answer: Answer::Unsat, via: Route::ModP, proof, conflicts: 0 };
514 }
515 crate::affine_gfp::AffinePCanon::Canonical(canon) => {
516 let sub = cdcl_fallback(canon.num_vars, &canon.clauses);
517 return match sub.answer {
518 Answer::Unsat => Solved { answer: Answer::Unsat, via: sub.via, proof: Vec::new(), conflicts: sub.conflicts },
519 Answer::Sat(model) => {
520 let lifted = canon.lift(&model);
521 if clauses.iter().all(|c| c.iter().any(|l| lifted[l.var() as usize] == l.is_positive())) {
522 Solved { answer: Answer::Sat(lifted), via: sub.via, proof: Vec::new(), conflicts: sub.conflicts }
523 } else {
524 cdcl_fallback(num_vars, clauses) }
526 }
527 };
528 }
529 crate::affine_gfp::AffinePCanon::Unchanged => {}
530 }
531 match crate::affine_gfp::affine_m_canonicalize(num_vars, clauses) {
536 crate::affine_gfp::AffinePCanon::Refuted(drat) => {
537 let proof = drat.map(|res| res.into_iter().map(ProofStep::Rup).collect()).unwrap_or_default();
538 return Solved { answer: Answer::Unsat, via: Route::ModM, proof, conflicts: 0 };
539 }
540 crate::affine_gfp::AffinePCanon::Canonical(canon) => {
541 let sub = cdcl_fallback(canon.num_vars, &canon.clauses);
542 return match sub.answer {
543 Answer::Unsat => Solved { answer: Answer::Unsat, via: sub.via, proof: Vec::new(), conflicts: sub.conflicts },
544 Answer::Sat(model) => {
545 let lifted = canon.lift(&model);
546 if clauses.iter().all(|c| c.iter().any(|l| lifted[l.var() as usize] == l.is_positive())) {
547 Solved { answer: Answer::Sat(lifted), via: sub.via, proof: Vec::new(), conflicts: sub.conflicts }
548 } else {
549 cdcl_fallback(num_vars, clauses) }
551 }
552 };
553 }
554 crate::affine_gfp::AffinePCanon::Unchanged => {}
555 }
556 if let Some(s) = component_solve(num_vars, clauses) {
560 return s;
561 }
562 cdcl_fallback(num_vars, clauses)
563}
564
565fn recursive_break_solve(num_vars: usize, clauses: &[Vec<Lit>]) -> Option<Solved> {
571 if num_vars == 0 || num_vars > 64 {
572 return None;
573 }
574 let broken = break_all_symmetry(num_vars, clauses);
575 if broken.len() == clauses.len() {
576 return None; }
578 let mut solver = Solver::new(num_vars);
579 for c in &broken {
580 solver.add_clause(c.clone());
581 }
582 match solver.solve() {
583 SolveResult::Sat(model) => {
584 let projected: Vec<bool> = model[..num_vars].to_vec();
585 clauses
586 .iter()
587 .all(|c| c.iter().any(|l| projected[l.var() as usize] == l.is_positive()))
588 .then_some(Solved {
589 answer: Answer::Sat(projected),
590 via: Route::RecursiveBreak,
591 proof: Vec::new(),
592 conflicts: solver.conflicts(),
593 })
594 }
595 SolveResult::Unsat => {
596 Some(Solved { answer: Answer::Unsat, via: Route::RecursiveBreak, proof: Vec::new(), conflicts: solver.conflicts() })
597 }
598 }
599}
600
601fn local_symmetry_solve(num_vars: usize, clauses: &[Vec<Lit>]) -> Option<Solved> {
608 if num_vars == 0 || num_vars > 24 {
609 return None;
610 }
611 let fixed_gens = |lit: Lit| -> Vec<Vec<Lit>> {
613 let v = lit.var() as usize;
614 crate::sym_break::conditional_symmetry_generators(num_vars, clauses, &[lit])
615 .into_iter()
616 .filter(|img| img[v] == Lit::pos(v as u32))
617 .collect()
618 };
619 let mut best: Option<usize> = None;
620 let mut best_score = 0usize;
621 for v in 0..num_vars {
622 let score = fixed_gens(Lit::pos(v as u32)).len() + fixed_gens(Lit::neg(v as u32)).len();
623 if score > best_score {
624 best_score = score;
625 best = Some(v);
626 }
627 }
628 let v = best?; let mut conflicts = 0u64;
631 for polarity in [false, true] {
632 let lit = Lit::new(v as u32, polarity);
633 let (sbp, total) = crate::sym_break::lex_leader_sbp_lit(num_vars, &fixed_gens(lit));
634 let mut solver = Solver::new(total.max(num_vars));
635 for c in clauses {
636 solver.add_clause(c.clone());
637 }
638 solver.add_clause(vec![lit]); for c in &sbp {
640 solver.add_clause(c.clone());
641 }
642 match solver.solve() {
643 SolveResult::Sat(model) => {
644 return Some(Solved {
645 answer: Answer::Sat(model[..num_vars].to_vec()),
646 via: Route::LocalSymmetry,
647 proof: Vec::new(),
648 conflicts: conflicts + solver.conflicts(),
649 });
650 }
651 SolveResult::Unsat => conflicts += solver.conflicts(),
652 }
653 }
654 Some(Solved { answer: Answer::Unsat, via: Route::LocalSymmetry, proof: Vec::new(), conflicts })
655}
656
657fn dynamic_sel(num_vars: usize, clauses: &[Vec<Lit>]) -> Option<Solved> {
663 use crate::sym_dynamic::{sel_refute, SelOutcome};
664 if num_vars > 64 || crate::sym_break::literal_automorphism_generators(num_vars, clauses).is_empty() {
665 return None;
666 }
667 match sel_refute(num_vars, clauses) {
668 SelOutcome::Unsat { steps, conflicts, .. } => {
669 Some(Solved { answer: Answer::Unsat, via: Route::Sel, proof: steps, conflicts })
670 }
671 SelOutcome::Sat(model) => {
672 Some(Solved { answer: Answer::Sat(model), via: Route::Sel, proof: Vec::new(), conflicts: 0 })
673 }
674 SelOutcome::Unknown { .. } => None,
675 }
676}
677
678fn symmetry_break_solve(num_vars: usize, clauses: &[Vec<Lit>]) -> Option<Solved> {
683 if num_vars > 64 {
684 return None; }
686 let gens = crate::sym_break::literal_automorphism_generators(num_vars, clauses);
688 if gens.is_empty() {
689 return None; }
691 let point_gens: Vec<_> =
692 gens.iter().map(|s| crate::sym_break::litsym_to_points(s, num_vars)).collect();
693 let bsgs = crate::permgroup::schreier_sims(2 * num_vars, &point_gens);
694 if bsgs.order() <= 1 {
695 return None;
696 }
697 let (sbp, total) = match bsgs.elements(50_000) {
703 Some(pts) => crate::sym_break::lex_leader_sbp_lit(
704 num_vars,
705 &pts.iter().map(|p| crate::sym_break::litsym_from_points(p, num_vars)).collect::<Vec<_>>(),
706 ),
707 None => crate::sym_break::hierarchical_break(num_vars, clauses).unwrap_or_else(|| {
708 let mut s = gens;
709 s.extend(
710 bsgs.transversal_elements().iter().map(|p| crate::sym_break::litsym_from_points(p, num_vars)),
711 );
712 crate::sym_break::lex_leader_sbp_lit(num_vars, &s)
713 }),
714 };
715 let mut solver = Solver::new(total);
716 for c in clauses {
717 solver.add_clause(c.clone());
718 }
719 for c in &sbp {
720 solver.add_clause(c.clone());
721 }
722 match solver.solve() {
723 SolveResult::Sat(model) => {
724 let projected: Vec<bool> = model[..num_vars].to_vec();
725 clauses
727 .iter()
728 .all(|c| c.iter().any(|l| projected[l.var() as usize] == l.is_positive()))
729 .then_some(Solved {
730 answer: Answer::Sat(projected),
731 via: Route::SymmetryBreak,
732 proof: Vec::new(),
733 conflicts: solver.conflicts(),
734 })
735 }
736 SolveResult::Unsat => Some(Solved::unsat(Route::SymmetryBreak)),
737 }
738}
739
740fn orbital_branch_solve(num_vars: usize, clauses: &[Vec<Lit>]) -> Option<Solved> {
757 if num_vars == 0 || num_vars > 64 {
758 return None;
759 }
760 let gens = crate::sym_break::variable_automorphism_generators(num_vars, clauses)?;
763 if gens.is_empty() {
764 return None;
765 }
766 if !crate::permgroup::orbits(num_vars, &gens).iter().any(|o| o.len() >= 3) {
768 return None;
769 }
770 let mut conflicts = 0u64;
771 let mut budget = 1024u64; let answer = orbital_node(num_vars, clauses, &gens, &mut Vec::new(), &mut budget, &mut conflicts)?;
773 Some(Solved { answer, via: Route::OrbitalBranch, proof: Vec::new(), conflicts })
774}
775
776fn orbital_node(
780 num_vars: usize,
781 clauses: &[Vec<Lit>],
782 gens: &[crate::permgroup::Perm],
783 committed: &mut Vec<Lit>,
784 budget: &mut u64,
785 conflicts: &mut u64,
786) -> Option<Answer> {
787 let checked = |m: Vec<bool>| -> Option<Answer> {
788 clauses
789 .iter()
790 .all(|c| c.iter().any(|l| m[l.var() as usize] == l.is_positive()))
791 .then_some(Answer::Sat(m))
792 };
793 let committed_vars: HashSet<usize> = committed.iter().map(|l| l.var() as usize).collect();
796 let live: Vec<crate::permgroup::Perm> = if committed_vars.is_empty() {
797 gens.to_vec()
798 } else {
799 gens.iter().filter(|g| committed_vars.iter().all(|&v| g[v] == v)).cloned().collect()
800 };
801 let orbit = (*budget > 0)
803 .then(|| {
804 crate::permgroup::orbits(num_vars, &live)
805 .into_iter()
806 .filter(|o| o.len() >= 2 && o.iter().all(|v| !committed_vars.contains(v)))
807 .max_by_key(|o| o.len())
808 })
809 .flatten();
810 let orbit = match orbit {
811 Some(o) => o,
812 None => return solve_residual(num_vars, clauses, committed, conflicts), };
814 *budget -= 1;
815 let rep = orbit[0];
816
817 committed.push(Lit::pos(rep as u32));
819 let a = orbital_node(num_vars, clauses, gens, committed, budget, conflicts);
820 committed.pop();
821 match a {
822 Some(Answer::Sat(m)) => return checked(m),
823 None => return None, Some(Answer::Unsat) => {}
825 }
826
827 let n0 = committed.len();
829 committed.extend(orbit.iter().map(|&v| Lit::neg(v as u32)));
830 let b = orbital_node(num_vars, clauses, gens, committed, budget, conflicts);
831 committed.truncate(n0);
832 match b {
833 Some(Answer::Sat(m)) => checked(m),
834 Some(Answer::Unsat) => Some(Answer::Unsat), None => None,
836 }
837}
838
839fn solve_residual(
841 num_vars: usize,
842 clauses: &[Vec<Lit>],
843 committed: &[Lit],
844 conflicts: &mut u64,
845) -> Option<Answer> {
846 let mut s = Solver::new(num_vars);
847 for c in clauses {
848 s.add_clause(c.clone());
849 }
850 for &l in committed {
851 s.add_clause(vec![l]);
852 }
853 let r = s.solve();
854 *conflicts += s.conflicts();
855 Some(match r {
856 SolveResult::Sat(model) => Answer::Sat(model[..num_vars].to_vec()),
857 SolveResult::Unsat => Answer::Unsat,
858 })
859}
860
861fn symmetric_probe_solve(num_vars: usize, clauses: &[Vec<Lit>]) -> Option<Solved> {
871 if num_vars == 0 || num_vars > 64 {
872 return None;
873 }
874 let gens = crate::sym_break::literal_automorphism_generators(num_vars, clauses);
876 if gens.is_empty() {
877 return None;
878 }
879 let point_gens: Vec<_> =
880 gens.iter().map(|s| crate::sym_break::litsym_to_points(s, num_vars)).collect();
881 let lit_orbits = crate::permgroup::orbits(2 * num_vars, &point_gens);
882 let point_to_lit = |p: usize| Lit::new((p / 2) as u32, p % 2 == 0);
883
884 const PROBE_BUDGET: u64 = 200;
886 let probe_fails = |lit: Lit| -> bool {
887 let mut s = Solver::new(num_vars);
888 for c in clauses {
889 s.add_clause(c.clone());
890 }
891 s.add_clause(vec![lit]);
892 matches!(s.solve_budgeted(PROBE_BUDGET), BudgetedResult::Unsat)
893 };
894
895 let mut forced: Vec<Lit> = Vec::new();
898 for orbit in &lit_orbits {
899 if orbit.len() < 2 {
900 continue;
901 }
902 if probe_fails(point_to_lit(orbit[0])) {
903 forced.extend(orbit.iter().map(|&p| point_to_lit(p).negated()));
904 }
905 }
906 if forced.is_empty() {
907 return None; }
909
910 let mut solver = Solver::new(num_vars);
911 for c in clauses {
912 solver.add_clause(c.clone());
913 }
914 for &l in &forced {
915 solver.add_clause(vec![l]);
916 }
917 let r = solver.solve();
918 let conflicts = solver.conflicts();
919 match r {
920 SolveResult::Sat(model) => {
921 let projected: Vec<bool> = model[..num_vars].to_vec();
922 clauses
923 .iter()
924 .all(|c| c.iter().any(|l| projected[l.var() as usize] == l.is_positive()))
925 .then_some(Solved {
926 answer: Answer::Sat(projected),
927 via: Route::SymmetricProbe,
928 proof: Vec::new(),
929 conflicts,
930 })
931 }
932 SolveResult::Unsat => {
933 Some(Solved { answer: Answer::Unsat, via: Route::SymmetricProbe, proof: Vec::new(), conflicts })
934 }
935 }
936}
937
938fn bcp_forced(num_vars: usize, clauses: &[Vec<Lit>], assume: Lit) -> Option<Vec<Lit>> {
942 let mut val: Vec<Option<bool>> = vec![None; num_vars];
943 val[assume.var() as usize] = Some(assume.is_positive());
944 let mut forced = vec![assume];
945 loop {
946 let mut changed = false;
947 for c in clauses {
948 let mut sat = false;
949 let mut unassigned: Option<Lit> = None;
950 let mut count = 0;
951 for &l in c {
952 match val[l.var() as usize] {
953 Some(b) if b == l.is_positive() => {
954 sat = true;
955 break;
956 }
957 Some(_) => {}
958 None => {
959 count += 1;
960 unassigned = Some(l);
961 }
962 }
963 }
964 if sat {
965 continue;
966 }
967 if count == 0 {
968 return None; }
970 if count == 1 {
971 let u = unassigned.unwrap();
972 val[u.var() as usize] = Some(u.is_positive());
973 forced.push(u);
974 changed = true;
975 }
976 }
977 if !changed {
978 break;
979 }
980 }
981 Some(forced)
982}
983
984fn symmetric_binary_inference_solve(num_vars: usize, clauses: &[Vec<Lit>]) -> Option<Solved> {
993 if num_vars == 0 || num_vars > 64 {
994 return None;
995 }
996 let gens = crate::sym_break::variable_automorphism_generators(num_vars, clauses)?;
997 if gens.is_empty() {
998 return None;
999 }
1000 let key2 = |a: Lit, b: Lit| -> [(u32, bool); 2] {
1001 let mut k = [(a.var(), a.is_positive()), (b.var(), b.is_positive())];
1002 k.sort_unstable();
1003 k
1004 };
1005 let lit_apply = |g: &[usize], l: Lit| Lit::new(g[l.var() as usize] as u32, l.is_positive());
1006
1007 let mut seen: HashSet<[(u32, bool); 2]> =
1009 clauses.iter().filter(|c| c.len() == 2).map(|c| key2(c[0], c[1])).collect();
1010
1011 const CAP: usize = 4096;
1012 let mut new_bins: Vec<Vec<Lit>> = Vec::new();
1013 'outer: for orbit in crate::permgroup::orbits(num_vars, &gens) {
1014 let v = orbit[0];
1015 for pol in [false, true] {
1016 let lit = Lit::new(v as u32, pol);
1017 let Some(forced) = bcp_forced(num_vars, clauses, lit) else {
1018 continue; };
1020 for &m in &forced {
1021 if m.var() == lit.var() {
1022 continue;
1023 }
1024 let mut local: HashSet<[(u32, bool); 2]> = HashSet::new();
1026 let mut stack = vec![(lit.negated(), m)];
1027 while let Some((a, b)) = stack.pop() {
1028 if a.var() == b.var() {
1029 continue;
1030 }
1031 let k = key2(a, b);
1032 if !local.insert(k) {
1033 continue;
1034 }
1035 if seen.insert(k) {
1036 new_bins.push(vec![a, b]);
1037 if new_bins.len() >= CAP {
1038 break 'outer;
1039 }
1040 }
1041 for g in &gens {
1042 stack.push((lit_apply(g, a), lit_apply(g, b)));
1043 }
1044 }
1045 }
1046 }
1047 }
1048 if new_bins.is_empty() {
1049 return None; }
1051
1052 let mut solver = Solver::new(num_vars);
1053 for c in clauses {
1054 solver.add_clause(c.clone());
1055 }
1056 for c in &new_bins {
1057 solver.add_clause(c.clone());
1058 }
1059 let r = solver.solve();
1060 let conflicts = solver.conflicts();
1061 match r {
1062 SolveResult::Sat(model) => {
1063 let projected: Vec<bool> = model[..num_vars].to_vec();
1064 clauses
1065 .iter()
1066 .all(|c| c.iter().any(|l| projected[l.var() as usize] == l.is_positive()))
1067 .then_some(Solved {
1068 answer: Answer::Sat(projected),
1069 via: Route::SymmetricBinary,
1070 proof: Vec::new(),
1071 conflicts,
1072 })
1073 }
1074 SolveResult::Unsat => {
1075 Some(Solved { answer: Answer::Unsat, via: Route::SymmetricBinary, proof: Vec::new(), conflicts })
1076 }
1077 }
1078}
1079
1080fn orbit_weight_quotient_solve(num_vars: usize, clauses: &[Vec<Lit>]) -> Option<Solved> {
1094 if num_vars == 0 || num_vars > 64 {
1095 return None;
1096 }
1097 let gens = crate::sym_break::variable_automorphism_generators(num_vars, clauses)?;
1098 if gens.is_empty() {
1099 return None;
1100 }
1101 let orbits = crate::permgroup::orbits(num_vars, &gens);
1102 let bsgs = crate::permgroup::schreier_sims(num_vars, &gens);
1103
1104 for orbit in &orbits {
1106 for w in orbit.windows(2) {
1107 let mut t: Vec<usize> = (0..num_vars).collect();
1108 t.swap(w[0], w[1]);
1109 if !bsgs.contains(&t) {
1110 return None; }
1112 }
1113 }
1114
1115 let mut num_reps: u128 = 1;
1117 for o in &orbits {
1118 num_reps = num_reps.saturating_mul(o.len() as u128 + 1);
1119 }
1120 if num_reps > 200_000 || num_reps >= (1u128 << num_vars) {
1121 return None;
1122 }
1123
1124 let dims: Vec<usize> = orbits.iter().map(|o| o.len() + 1).collect();
1127 let total = num_reps as usize;
1128 let satisfies = |a: &[bool]| -> bool {
1129 clauses.iter().all(|c| c.iter().any(|l| a[l.var() as usize] == l.is_positive()))
1130 };
1131 for idx in 0..total {
1132 let mut rem = idx;
1133 let mut assign = vec![false; num_vars];
1134 for (oi, orbit) in orbits.iter().enumerate() {
1135 let w = rem % dims[oi];
1136 rem /= dims[oi];
1137 for &v in orbit.iter().take(w) {
1138 assign[v] = true;
1139 }
1140 }
1141 if satisfies(&assign) {
1142 return Some(Solved {
1143 answer: Answer::Sat(assign),
1144 via: Route::OrbitWeightQuotient,
1145 proof: Vec::new(),
1146 conflicts: 0,
1147 });
1148 }
1149 }
1150 Some(Solved::unsat(Route::OrbitWeightQuotient))
1152}
1153
1154struct LexLeaderTheory {
1164 num_vars: usize,
1165 generators: Vec<crate::permgroup::Perm>,
1166}
1167
1168impl crate::cdcl::Theory for LexLeaderTheory {
1169 fn propagate(&mut self, trail: &[Lit]) -> Vec<Vec<Lit>> {
1170 let mut val: Vec<Option<bool>> = vec![None; self.num_vars];
1171 for &l in trail {
1172 let v = l.var() as usize;
1173 if v < self.num_vars {
1174 val[v] = Some(l.is_positive());
1175 }
1176 }
1177 let actionable = |c: &[Lit]| -> bool {
1180 let mut unassigned = 0;
1181 for &lit in c {
1182 match val[lit.var() as usize] {
1183 Some(b) if b == lit.is_positive() => return false, Some(_) => {}
1185 None => unassigned += 1,
1186 }
1187 }
1188 unassigned <= 1
1189 };
1190
1191 let mut out: Vec<Vec<Lit>> = Vec::new();
1192 for g in &self.generators {
1193 let mut prefix: Vec<Lit> = Vec::new();
1194 for j in 0..self.num_vars {
1195 let k = g[j];
1196 if k == j {
1197 continue; }
1199 match (val[j], val[k]) {
1200 (Some(a), Some(b)) if a == b => {
1201 prefix.push(Lit::new(j as u32, !a));
1203 prefix.push(Lit::new(k as u32, !b));
1204 }
1205 _ => {
1206 let mut c = prefix.clone();
1208 c.push(Lit::new(j as u32, false)); c.push(Lit::new(k as u32, true)); if actionable(&c) {
1211 out.push(c);
1212 }
1213 break;
1214 }
1215 }
1216 }
1217 }
1218 out
1219 }
1220}
1221
1222fn symmetry_propagate_solve(num_vars: usize, clauses: &[Vec<Lit>]) -> Option<Solved> {
1228 if num_vars == 0 || num_vars > 64 {
1229 return None;
1230 }
1231 let gens = crate::sym_break::variable_automorphism_generators(num_vars, clauses)?;
1232 if gens.is_empty() {
1233 return None;
1234 }
1235 let mut solver = Solver::new(num_vars);
1236 for c in clauses {
1237 solver.add_clause(c.clone());
1238 }
1239 let mut theories: Vec<Box<dyn crate::cdcl::Theory>> =
1240 vec![Box::new(LexLeaderTheory { num_vars, generators: gens })];
1241 match solver.solve_with(&mut theories) {
1242 SolveResult::Sat(model) => {
1243 let projected: Vec<bool> = model[..num_vars].to_vec();
1244 clauses
1245 .iter()
1246 .all(|c| c.iter().any(|l| projected[l.var() as usize] == l.is_positive()))
1247 .then_some(Solved {
1248 answer: Answer::Sat(projected),
1249 via: Route::SymmetryPropagate,
1250 proof: Vec::new(),
1251 conflicts: solver.conflicts(),
1252 })
1253 }
1254 SolveResult::Unsat => Some(Solved {
1255 answer: Answer::Unsat,
1256 via: Route::SymmetryPropagate,
1257 proof: Vec::new(),
1258 conflicts: solver.conflicts(),
1259 }),
1260 }
1261}
1262
1263fn uf_find(parent: &mut [usize], mut x: usize) -> usize {
1265 while parent[x] != x {
1266 parent[x] = parent[parent[x]];
1267 x = parent[x];
1268 }
1269 x
1270}
1271
1272fn component_solve(num_vars: usize, clauses: &[Vec<Lit>]) -> Option<Solved> {
1281 if num_vars == 0 || num_vars > 64 || clauses.is_empty() {
1282 return None;
1283 }
1284 let mut parent: Vec<usize> = (0..num_vars).collect();
1285 for c in clauses {
1286 if c.is_empty() {
1287 return Some(Solved::unsat(Route::Component)); }
1289 let r0 = uf_find(&mut parent, c[0].var() as usize);
1290 for l in &c[1..] {
1291 let r = uf_find(&mut parent, l.var() as usize);
1292 parent[r] = r0;
1293 }
1294 }
1295 let mut comp_clauses: Vec<Vec<Vec<Lit>>> = vec![Vec::new(); num_vars];
1296 for c in clauses {
1297 let r = uf_find(&mut parent, c[0].var() as usize);
1298 comp_clauses[r].push(c.clone());
1299 }
1300 let roots: Vec<usize> = (0..num_vars).filter(|&r| !comp_clauses[r].is_empty()).collect();
1301 if roots.len() <= 1 {
1302 return None; }
1304 let mut model = vec![false; num_vars];
1305 let mut conflicts = 0u64;
1306 for &r in &roots {
1307 let sub = solve_comprehensive(num_vars, &comp_clauses[r]);
1308 conflicts += sub.conflicts;
1309 match sub.answer {
1310 Answer::Unsat => {
1311 return Some(Solved { answer: Answer::Unsat, via: Route::Component, proof: Vec::new(), conflicts });
1312 }
1313 Answer::Sat(m) => {
1314 let vars: std::collections::BTreeSet<usize> =
1315 comp_clauses[r].iter().flatten().map(|l| l.var() as usize).collect();
1316 for v in vars {
1317 model[v] = m[v];
1318 }
1319 }
1320 }
1321 }
1322 clauses
1324 .iter()
1325 .all(|c| c.iter().any(|l| model[l.var() as usize] == l.is_positive()))
1326 .then_some(Solved { answer: Answer::Sat(model), via: Route::Component, proof: Vec::new(), conflicts })
1327}
1328
1329pub fn solve_by_components(num_vars: usize, clauses: &[Vec<Lit>]) -> Solved {
1333 component_solve(num_vars, clauses).unwrap_or_else(|| cdcl_fallback(num_vars, clauses))
1334}
1335
1336fn symmetric_component_solve(num_vars: usize, clauses: &[Vec<Lit>]) -> Option<Solved> {
1346 if num_vars == 0 || num_vars > 64 || clauses.is_empty() {
1347 return None;
1348 }
1349 let mut parent: Vec<usize> = (0..num_vars).collect();
1351 for c in clauses {
1352 if c.is_empty() {
1353 return Some(Solved::unsat(Route::SymmetricComponent)); }
1355 let r0 = uf_find(&mut parent, c[0].var() as usize);
1356 for l in &c[1..] {
1357 let r = uf_find(&mut parent, l.var() as usize);
1358 parent[r] = r0;
1359 }
1360 }
1361 let mut appears = vec![false; num_vars];
1362 for c in clauses {
1363 for l in c {
1364 appears[l.var() as usize] = true;
1365 }
1366 }
1367 let mut comp_vars: Vec<Vec<usize>> = vec![Vec::new(); num_vars];
1368 for v in 0..num_vars {
1369 if appears[v] {
1370 let r = uf_find(&mut parent, v);
1371 comp_vars[r].push(v);
1372 }
1373 }
1374 let roots: Vec<usize> = (0..num_vars).filter(|&r| !comp_vars[r].is_empty()).collect();
1375 if roots.len() <= 1 {
1376 return None; }
1378 let mut comp_clauses: Vec<Vec<Vec<Lit>>> = vec![Vec::new(); num_vars];
1379 for c in clauses {
1380 let r = uf_find(&mut parent, c[0].var() as usize);
1381 comp_clauses[r].push(c.clone());
1382 }
1383 let gens = crate::sym_break::variable_automorphism_generators(num_vars, clauses)?;
1385 if gens.is_empty() {
1386 return None;
1387 }
1388 let identity: Vec<usize> = (0..num_vars).collect();
1390 let mut orbit_of: Vec<Option<usize>> = vec![None; num_vars];
1391 let mut orbits: Vec<Vec<(usize, Vec<usize>)>> = Vec::new();
1392 for &r in &roots {
1393 if orbit_of[r].is_some() {
1394 continue;
1395 }
1396 let oi = orbits.len();
1397 orbit_of[r] = Some(oi);
1398 let mut orbit: Vec<(usize, Vec<usize>)> = vec![(r, identity.clone())];
1399 let mut i = 0;
1400 while i < orbit.len() {
1401 let (cr, perm) = orbit[i].clone();
1402 i += 1;
1403 for g in &gens {
1404 let img_root = uf_find(&mut parent, g[comp_vars[cr][0]]);
1405 if orbit_of[img_root].is_none() {
1406 orbit_of[img_root] = Some(oi);
1407 let new_perm: Vec<usize> = (0..num_vars).map(|v| g[perm[v]]).collect();
1408 orbit.push((img_root, new_perm));
1409 }
1410 }
1411 }
1412 orbits.push(orbit);
1413 }
1414 if !orbits.iter().any(|o| o.len() >= 2) {
1416 return None;
1417 }
1418 let mut model = vec![false; num_vars];
1420 let mut conflicts = 0u64;
1421 for orbit in &orbits {
1422 let rep_root = orbit[0].0;
1423 let solved = solve_comprehensive(num_vars, &comp_clauses[rep_root]);
1424 conflicts += solved.conflicts;
1425 match solved.answer {
1426 Answer::Unsat => {
1427 return Some(Solved {
1428 answer: Answer::Unsat,
1429 via: Route::SymmetricComponent,
1430 proof: Vec::new(),
1431 conflicts,
1432 });
1433 }
1434 Answer::Sat(rep_model) => {
1435 for (_, perm) in orbit {
1436 for &v in &comp_vars[rep_root] {
1437 model[perm[v]] = rep_model[v];
1438 }
1439 }
1440 }
1441 }
1442 }
1443 clauses
1444 .iter()
1445 .all(|c| c.iter().any(|l| model[l.var() as usize] == l.is_positive()))
1446 .then_some(Solved { answer: Answer::Sat(model), via: Route::SymmetricComponent, proof: Vec::new(), conflicts })
1447}
1448
1449fn root_propagate(num_vars: usize, clauses: &[Vec<Lit>]) -> Option<(Vec<Lit>, Vec<Vec<Lit>>)> {
1453 let mut val: Vec<Option<bool>> = vec![None; num_vars];
1454 loop {
1455 let mut changed = false;
1456 for c in clauses {
1457 let mut sat = false;
1458 let mut unit: Option<Lit> = None;
1459 let mut count = 0;
1460 for &l in c {
1461 match val[l.var() as usize] {
1462 Some(b) if b == l.is_positive() => {
1463 sat = true;
1464 break;
1465 }
1466 Some(_) => {}
1467 None => {
1468 count += 1;
1469 unit = Some(l);
1470 }
1471 }
1472 }
1473 if sat {
1474 continue;
1475 }
1476 if count == 0 {
1477 return None; }
1479 if count == 1 {
1480 let u = unit.unwrap();
1481 val[u.var() as usize] = Some(u.is_positive());
1482 changed = true;
1483 }
1484 }
1485 if !changed {
1486 break;
1487 }
1488 }
1489 let forced: Vec<Lit> =
1490 (0..num_vars).filter_map(|v| val[v].map(|b| Lit::new(v as u32, b))).collect();
1491 let mut residual: Vec<Vec<Lit>> = Vec::new();
1492 for c in clauses {
1493 let mut sat = false;
1494 let mut shrunk: Vec<Lit> = Vec::new();
1495 for &l in c {
1496 match val[l.var() as usize] {
1497 Some(b) if b == l.is_positive() => {
1498 sat = true;
1499 break;
1500 }
1501 Some(_) => {} None => shrunk.push(l),
1503 }
1504 }
1505 if !sat {
1506 if shrunk.is_empty() {
1507 return None; }
1509 residual.push(shrunk);
1510 }
1511 }
1512 Some((forced, residual))
1513}
1514
1515fn symmetry_via_simplification_solve(num_vars: usize, clauses: &[Vec<Lit>]) -> Option<Solved> {
1524 if num_vars == 0 || num_vars > 64 {
1525 return None;
1526 }
1527 let (rho, residual) = match root_propagate(num_vars, clauses) {
1528 None => return Some(Solved::unsat(Route::SymmetrySimplify)), Some(x) => x,
1530 };
1531 if rho.is_empty() {
1532 return None; }
1534 let mut detect = residual.clone();
1538 for &l in &rho {
1539 detect.push(vec![l]);
1540 }
1541 let res_gens = crate::sym_break::variable_automorphism_generators(num_vars, &detect)
1542 .unwrap_or_default();
1543 if res_gens.is_empty() {
1544 return None; }
1546 let raw_set: HashSet<Vec<(u32, bool)>> = clauses
1548 .iter()
1549 .map(|c| {
1550 let mut k: Vec<(u32, bool)> = c.iter().map(|l| (l.var(), l.is_positive())).collect();
1551 k.sort_unstable();
1552 k
1553 })
1554 .collect();
1555 let is_raw_symmetry = |g: &[usize]| -> bool {
1556 clauses.iter().all(|c| {
1557 let mut img: Vec<(u32, bool)> =
1558 c.iter().map(|l| (g[l.var() as usize] as u32, l.is_positive())).collect();
1559 img.sort_unstable();
1560 raw_set.contains(&img)
1561 })
1562 };
1563 if res_gens.iter().all(|g| is_raw_symmetry(g)) {
1564 return None; }
1566
1567 let solved = solve_comprehensive(num_vars, &residual);
1569 match solved.answer {
1570 Answer::Unsat => Some(Solved {
1571 answer: Answer::Unsat,
1572 via: Route::SymmetrySimplify,
1573 proof: Vec::new(),
1574 conflicts: solved.conflicts,
1575 }),
1576 Answer::Sat(mut model) => {
1577 for &l in &rho {
1578 model[l.var() as usize] = l.is_positive();
1579 }
1580 clauses
1581 .iter()
1582 .all(|c| c.iter().any(|l| model[l.var() as usize] == l.is_positive()))
1583 .then_some(Solved {
1584 answer: Answer::Sat(model),
1585 via: Route::SymmetrySimplify,
1586 proof: Vec::new(),
1587 conflicts: solved.conflicts,
1588 })
1589 }
1590 }
1591}
1592
1593fn nested_block_tower_break(num_vars: usize, clauses: &[Vec<Lit>]) -> Option<(Vec<Vec<Lit>>, usize)> {
1601 let gens = crate::sym_break::variable_automorphism_generators(num_vars, clauses)?;
1602 if gens.is_empty() {
1603 return None;
1604 }
1605 let bsgs = crate::permgroup::schreier_sims(num_vars, &gens);
1606 let to_litsym = |p: &[usize]| -> Vec<Lit> { (0..num_vars).map(|v| Lit::pos(p[v] as u32)).collect() };
1607
1608 let mut structured: Vec<Vec<Lit>> = Vec::new();
1609 let mut blocks = crate::permgroup::minimal_block_system(num_vars, &gens)?; for _level in 0..num_vars {
1611 let k = blocks.len();
1612 let m = blocks[0].len();
1613 if blocks.iter().any(|b| b.len() != m) {
1614 break; }
1616 for i in 0..k.saturating_sub(1) {
1618 let mut p: Vec<usize> = (0..num_vars).collect();
1619 for j in 0..m {
1620 p[blocks[i][j]] = blocks[i + 1][j];
1621 p[blocks[i + 1][j]] = blocks[i][j];
1622 }
1623 if bsgs.contains(&p) {
1624 structured.push(to_litsym(&p));
1625 }
1626 }
1627 for j in 0..m.saturating_sub(1) {
1629 let mut p: Vec<usize> = (0..num_vars).collect();
1630 for b in &blocks {
1631 p[b[j]] = b[j + 1];
1632 p[b[j + 1]] = b[j];
1633 }
1634 if bsgs.contains(&p) {
1635 structured.push(to_litsym(&p));
1636 }
1637 }
1638 if k <= 1 {
1639 break;
1640 }
1641 let mut block_of = vec![usize::MAX; num_vars];
1643 for (bi, b) in blocks.iter().enumerate() {
1644 for &v in b {
1645 block_of[v] = bi;
1646 }
1647 }
1648 let induced: Vec<Vec<usize>> = gens
1649 .iter()
1650 .map(|g| (0..k).map(|bi| block_of[g[blocks[bi][0]]]).collect())
1651 .collect();
1652 let Some(super_blocks) = crate::permgroup::minimal_block_system(k, &induced) else {
1653 break; };
1655 let mut next: Vec<Vec<usize>> = Vec::new();
1656 for sb in &super_blocks {
1657 let mut nb = Vec::new();
1658 for &bi in sb {
1659 nb.extend_from_slice(&blocks[bi]);
1660 }
1661 next.push(nb);
1662 }
1663 if next.len() >= blocks.len() {
1664 break; }
1666 blocks = next;
1667 }
1668 if structured.is_empty() {
1669 return None;
1670 }
1671 Some(crate::sym_break::lex_leader_sbp_lit(num_vars, &structured))
1672}
1673
1674fn nested_symmetry_solve(num_vars: usize, clauses: &[Vec<Lit>]) -> Option<Solved> {
1679 if num_vars == 0 || num_vars > 64 {
1680 return None;
1681 }
1682 let (sbp, total) = nested_block_tower_break(num_vars, clauses)?;
1683 let mut solver = Solver::new(total);
1684 for c in clauses {
1685 solver.add_clause(c.clone());
1686 }
1687 for c in &sbp {
1688 solver.add_clause(c.clone());
1689 }
1690 match solver.solve() {
1691 SolveResult::Sat(model) => {
1692 let projected: Vec<bool> = model[..num_vars].to_vec();
1693 clauses
1694 .iter()
1695 .all(|c| c.iter().any(|l| projected[l.var() as usize] == l.is_positive()))
1696 .then_some(Solved {
1697 answer: Answer::Sat(projected),
1698 via: Route::NestedSymmetry,
1699 proof: Vec::new(),
1700 conflicts: solver.conflicts(),
1701 })
1702 }
1703 SolveResult::Unsat => {
1704 Some(Solved { answer: Answer::Unsat, via: Route::NestedSymmetry, proof: Vec::new(), conflicts: solver.conflicts() })
1705 }
1706 }
1707}
1708
1709fn canon_clause(c: &[Lit]) -> Vec<(u32, bool)> {
1711 let mut k: Vec<(u32, bool)> = c.iter().map(|l| (l.var(), l.is_positive())).collect();
1712 k.sort_unstable();
1713 k
1714}
1715
1716fn swap_clause_vars(c: &[Lit], a: usize, b: usize) -> Vec<Lit> {
1718 c.iter()
1719 .map(|l| {
1720 let v = l.var() as usize;
1721 let nv = if v == a {
1722 b
1723 } else if v == b {
1724 a
1725 } else {
1726 v
1727 };
1728 Lit::new(nv as u32, l.is_positive())
1729 })
1730 .collect()
1731}
1732
1733fn clause_is_implied(num_vars: usize, clauses: &[Vec<Lit>], c: &[Lit]) -> bool {
1735 let mut s = Solver::new(num_vars);
1736 for cl in clauses {
1737 s.add_clause(cl.clone());
1738 }
1739 for &l in c {
1740 s.add_clause(vec![l.negated()]);
1741 }
1742 matches!(s.solve(), SolveResult::Unsat)
1743}
1744
1745pub fn semantic_symmetry_pairs(num_vars: usize, clauses: &[Vec<Lit>]) -> (Vec<(usize, usize)>, bool) {
1751 let clause_set: HashSet<Vec<(u32, bool)>> = clauses.iter().map(|c| canon_clause(c)).collect();
1752 let mut pairs = Vec::new();
1753 let mut any_non_syntactic = false;
1754 for a in 0..num_vars {
1755 for b in (a + 1)..num_vars {
1756 let syntactic =
1757 clauses.iter().all(|c| clause_set.contains(&canon_clause(&swap_clause_vars(c, a, b))));
1758 let semantic = syntactic
1759 || clauses.iter().all(|c| {
1760 let sc = swap_clause_vars(c, a, b);
1761 clause_set.contains(&canon_clause(&sc)) || clause_is_implied(num_vars, clauses, &sc)
1762 });
1763 if semantic {
1764 pairs.push((a, b));
1765 if !syntactic {
1766 any_non_syntactic = true;
1767 }
1768 }
1769 }
1770 }
1771 (pairs, any_non_syntactic)
1772}
1773
1774fn semantic_symmetry_solve(num_vars: usize, clauses: &[Vec<Lit>]) -> Option<Solved> {
1781 if num_vars == 0 || num_vars > 20 || clauses.len() > 256 {
1782 return None; }
1784 let (pairs, any_non_syntactic) = semantic_symmetry_pairs(num_vars, clauses);
1785 if pairs.is_empty() || !any_non_syntactic {
1786 return None; }
1788 let gens: Vec<Vec<Lit>> = pairs
1789 .iter()
1790 .map(|&(a, b)| {
1791 (0..num_vars)
1792 .map(|v| {
1793 let img = if v == a {
1794 b
1795 } else if v == b {
1796 a
1797 } else {
1798 v
1799 };
1800 Lit::pos(img as u32)
1801 })
1802 .collect()
1803 })
1804 .collect();
1805 let (sbp, total) = crate::sym_break::lex_leader_sbp_lit(num_vars, &gens);
1806 let mut solver = Solver::new(total);
1807 for c in clauses {
1808 solver.add_clause(c.clone());
1809 }
1810 for c in &sbp {
1811 solver.add_clause(c.clone());
1812 }
1813 match solver.solve() {
1814 SolveResult::Sat(model) => {
1815 let projected: Vec<bool> = model[..num_vars].to_vec();
1816 clauses
1817 .iter()
1818 .all(|c| c.iter().any(|l| projected[l.var() as usize] == l.is_positive()))
1819 .then_some(Solved {
1820 answer: Answer::Sat(projected),
1821 via: Route::SemanticSymmetry,
1822 proof: Vec::new(),
1823 conflicts: solver.conflicts(),
1824 })
1825 }
1826 SolveResult::Unsat => {
1827 Some(Solved { answer: Answer::Unsat, via: Route::SemanticSymmetry, proof: Vec::new(), conflicts: solver.conflicts() })
1828 }
1829 }
1830}
1831
1832pub fn almost_symmetry_pairs(
1837 num_vars: usize,
1838 clauses: &[Vec<Lit>],
1839 max_broken: usize,
1840) -> Vec<(usize, usize, Vec<Vec<Lit>>)> {
1841 let clause_set: HashSet<Vec<(u32, bool)>> = clauses.iter().map(|c| canon_clause(c)).collect();
1842 let mut out = Vec::new();
1843 for a in 0..num_vars {
1844 for b in (a + 1)..num_vars {
1845 let mut images = Vec::new();
1846 for c in clauses {
1847 let sc = swap_clause_vars(c, a, b);
1848 if !clause_set.contains(&canon_clause(&sc)) {
1849 images.push(sc);
1850 }
1851 }
1852 if !images.is_empty() && images.len() <= max_broken {
1853 out.push((a, b, images));
1854 }
1855 }
1856 }
1857 out
1858}
1859
1860fn almost_symmetry_solve(num_vars: usize, clauses: &[Vec<Lit>]) -> Option<Solved> {
1869 if num_vars == 0 || num_vars > 20 || clauses.len() > 256 {
1870 return None;
1871 }
1872 let mut pairs = almost_symmetry_pairs(num_vars, clauses, 2);
1873 if pairs.is_empty() {
1874 return None;
1875 }
1876 pairs.sort_by_key(|(_, _, imgs)| imgs.len());
1878 let (a, b, images) = &pairs[0];
1879
1880 let mut aux = num_vars as u32;
1881 let mut extra: Vec<Vec<Lit>> = Vec::new();
1882 let mut guard_neg: Vec<Lit> = Vec::new();
1883 for img in images {
1884 let z = aux;
1885 aux += 1;
1886 for &l in img {
1888 extra.push(vec![l.negated(), Lit::pos(z)]);
1889 }
1890 let mut zc = vec![Lit::neg(z)];
1891 zc.extend(img.iter().copied());
1892 extra.push(zc);
1893 guard_neg.push(Lit::neg(z));
1894 }
1895 let mut guarded = guard_neg;
1897 guarded.push(Lit::neg(*a as u32));
1898 guarded.push(Lit::pos(*b as u32));
1899 extra.push(guarded);
1900
1901 let mut solver = Solver::new(aux as usize);
1902 for c in clauses {
1903 solver.add_clause(c.clone());
1904 }
1905 for c in &extra {
1906 solver.add_clause(c.clone());
1907 }
1908 match solver.solve() {
1909 SolveResult::Sat(model) => {
1910 let projected: Vec<bool> = model[..num_vars].to_vec();
1911 clauses
1912 .iter()
1913 .all(|c| c.iter().any(|l| projected[l.var() as usize] == l.is_positive()))
1914 .then_some(Solved {
1915 answer: Answer::Sat(projected),
1916 via: Route::AlmostSymmetry,
1917 proof: Vec::new(),
1918 conflicts: solver.conflicts(),
1919 })
1920 }
1921 SolveResult::Unsat => {
1922 Some(Solved { answer: Answer::Unsat, via: Route::AlmostSymmetry, proof: Vec::new(), conflicts: solver.conflicts() })
1923 }
1924 }
1925}
1926
1927fn apply_perm_to_clause(c: &[Lit], g: &[usize]) -> Vec<Lit> {
1929 c.iter().map(|l| Lit::new(g[l.var() as usize] as u32, l.is_positive())).collect()
1930}
1931
1932fn perm_preserves_clause_set(clauses: &[Vec<Lit>], g: &[usize]) -> bool {
1936 let set: HashSet<Vec<(u32, bool)>> = clauses.iter().map(|c| canon_clause(c)).collect();
1937 clauses.iter().all(|c| set.contains(&canon_clause(&apply_perm_to_clause(c, g))))
1938}
1939
1940pub fn common_automorphism_generators(
1947 num_vars: usize,
1948 f: &[Vec<Lit>],
1949 s: &[Vec<Lit>],
1950) -> Vec<crate::permgroup::Perm> {
1951 let mut candidates = crate::sym_break::variable_automorphism_generators(num_vars, f).unwrap_or_default();
1952 candidates.extend(crate::sym_break::variable_automorphism_generators(num_vars, s).unwrap_or_default());
1953 let mut out: Vec<Vec<usize>> = Vec::new();
1954 for g in candidates {
1955 let well_formed = g.len() == num_vars;
1956 let nontrivial = g.iter().enumerate().any(|(i, &x)| i != x);
1957 if well_formed
1958 && nontrivial
1959 && perm_preserves_clause_set(f, &g)
1960 && perm_preserves_clause_set(s, &g)
1961 && !out.contains(&g)
1962 {
1963 out.push(g);
1964 }
1965 }
1966 out
1967}
1968
1969fn clause_orbits(clauses: &[Vec<Lit>], gens: &[crate::permgroup::Perm]) -> Vec<Vec<usize>> {
1972 let index: HashMap<Vec<(u32, bool)>, usize> =
1973 clauses.iter().enumerate().map(|(i, c)| (canon_clause(c), i)).collect();
1974 let n = clauses.len();
1975 let mut parent: Vec<usize> = (0..n).collect();
1976 fn find(parent: &mut [usize], mut x: usize) -> usize {
1977 while parent[x] != x {
1978 parent[x] = parent[parent[x]];
1979 x = parent[x];
1980 }
1981 x
1982 }
1983 for (i, c) in clauses.iter().enumerate() {
1984 for g in gens {
1985 if let Some(&j) = index.get(&canon_clause(&apply_perm_to_clause(c, g))) {
1986 let (a, b) = (find(&mut parent, i), find(&mut parent, j));
1987 parent[a] = b;
1988 }
1989 }
1990 }
1991 let mut groups: std::collections::BTreeMap<usize, Vec<usize>> = std::collections::BTreeMap::new();
1992 for i in 0..n {
1993 let r = find(&mut parent, i);
1994 groups.entry(r).or_default().push(i);
1995 }
1996 groups.into_values().collect()
1997}
1998
1999fn entailment_counterexample(num_vars: usize, clauses: &[Vec<Lit>], c: &[Lit]) -> Option<Vec<bool>> {
2001 let mut s = Solver::new(num_vars);
2002 for cl in clauses {
2003 s.add_clause(cl.clone());
2004 }
2005 for &l in c {
2006 s.add_clause(vec![l.negated()]);
2007 }
2008 match s.solve() {
2009 SolveResult::Sat(m) => Some(m),
2010 SolveResult::Unsat => None,
2011 }
2012}
2013
2014#[derive(Clone, Debug, PartialEq, Eq)]
2016pub enum EquivVerdict {
2017 Equivalent,
2019 Differ(Vec<bool>),
2021}
2022
2023pub fn equivalent_modulo_symmetry(num_vars: usize, f: &[Vec<Lit>], s: &[Vec<Lit>]) -> EquivVerdict {
2031 let gens = common_automorphism_generators(num_vars, f, s);
2032 for orbit in clause_orbits(s, &gens) {
2034 if let Some(m) = entailment_counterexample(num_vars, f, &s[orbit[0]]) {
2035 return EquivVerdict::Differ(m); }
2037 }
2038 for orbit in clause_orbits(f, &gens) {
2040 if let Some(m) = entailment_counterexample(num_vars, s, &f[orbit[0]]) {
2041 return EquivVerdict::Differ(m);
2042 }
2043 }
2044 EquivVerdict::Equivalent
2045}
2046
2047pub fn equivalence_check_counts(num_vars: usize, f: &[Vec<Lit>], s: &[Vec<Lit>]) -> (usize, usize) {
2051 let gens = common_automorphism_generators(num_vars, f, s);
2052 (clause_orbits(s, &gens).len() + clause_orbits(f, &gens).len(), s.len() + f.len())
2053}
2054
2055pub fn optimization_symmetry_generators(
2060 num_vars: usize,
2061 clauses: &[Vec<Lit>],
2062 weights: &[i64],
2063) -> Vec<crate::permgroup::Perm> {
2064 crate::sym_break::variable_automorphism_generators(num_vars, clauses)
2065 .unwrap_or_default()
2066 .into_iter()
2067 .filter(|g| g.len() == num_vars && (0..num_vars).all(|v| weights[g[v]] == weights[v]))
2068 .collect()
2069}
2070
2071fn optimization_break(num_vars: usize, clauses: &[Vec<Lit>], weights: &[i64]) -> Vec<Vec<Lit>> {
2076 let mut broken = clauses.to_vec();
2077 for g in optimization_symmetry_generators(num_vars, clauses, weights) {
2078 if let Some(v) = (0..num_vars).find(|&v| g[v] != v) {
2079 broken.push(vec![Lit::new(v as u32, false), Lit::new(g[v] as u32, true)]); }
2081 }
2082 broken
2083}
2084
2085fn min_weight_model(num_vars: usize, clauses: &[Vec<Lit>], weights: &[i64]) -> Option<(i64, Vec<bool>, usize)> {
2091 let mut working = clauses.to_vec();
2092 let mut best: Option<(i64, Vec<bool>)> = None;
2093 let mut enumerated = 0usize;
2094 loop {
2095 let mut solver = Solver::new(num_vars);
2096 for c in &working {
2097 solver.add_clause(c.clone());
2098 }
2099 match solver.solve() {
2100 SolveResult::Unsat => break,
2101 SolveResult::Sat(model) => {
2102 enumerated += 1;
2103 let w: i64 = (0..num_vars).filter(|&i| model[i]).map(|i| weights[i]).sum();
2104 if best.as_ref().map_or(true, |(bw, _)| w < *bw) {
2105 best = Some((w, model[..num_vars].to_vec()));
2106 }
2107 working.push((0..num_vars).map(|i| Lit::new(i as u32, !model[i])).collect());
2108 }
2109 }
2110 }
2111 best.map(|(w, m)| (w, m, enumerated))
2112}
2113
2114pub fn optimize_modulo_symmetry(
2121 num_vars: usize,
2122 clauses: &[Vec<Lit>],
2123 weights: &[i64],
2124) -> Option<(i64, Vec<bool>)> {
2125 let broken = optimization_break(num_vars, clauses, weights);
2126 min_weight_model(num_vars, &broken, weights).map(|(w, m, _)| (w, m))
2127}
2128
2129pub fn optimize_enumeration_counts(num_vars: usize, clauses: &[Vec<Lit>], weights: &[i64]) -> (usize, usize) {
2133 let broken = optimization_break(num_vars, clauses, weights);
2134 let with = min_weight_model(num_vars, &broken, weights).map_or(0, |(_, _, c)| c);
2135 let without = min_weight_model(num_vars, clauses, weights).map_or(0, |(_, _, c)| c);
2136 (with, without)
2137}
2138
2139fn full_assignment_orbit(num_vars: usize, m: &[bool], gens: &[crate::permgroup::Perm]) -> Vec<Vec<bool>> {
2142 let mut seen: HashSet<Vec<bool>> = HashSet::from([m.to_vec()]);
2143 let mut out = vec![m.to_vec()];
2144 let mut i = 0;
2145 while i < out.len() {
2146 let cur = out[i].clone();
2147 i += 1;
2148 for g in gens {
2149 let mut pm = vec![false; num_vars];
2150 for v in 0..num_vars {
2151 pm[g[v]] = cur[v];
2152 }
2153 if seen.insert(pm.clone()) {
2154 out.push(pm);
2155 }
2156 }
2157 }
2158 out
2159}
2160
2161pub fn weighted_model_count(num_vars: usize, clauses: &[Vec<Lit>], weight: &[(i64, i64)]) -> i128 {
2168 let gens = crate::sym_break::variable_automorphism_generators(num_vars, clauses).unwrap_or_default();
2169 let weight_of = |m: &[bool]| -> i128 {
2170 (0..num_vars).map(|v| if m[v] { weight[v].1 as i128 } else { weight[v].0 as i128 }).product()
2171 };
2172 let mut working = clauses.to_vec();
2173 let mut z = 0i128;
2174 loop {
2175 let mut solver = Solver::new(num_vars);
2176 for c in &working {
2177 solver.add_clause(c.clone());
2178 }
2179 match solver.solve() {
2180 SolveResult::Unsat => break,
2181 SolveResult::Sat(model) => {
2182 let orbit = full_assignment_orbit(num_vars, &model[..num_vars], &gens);
2183 z += orbit.iter().map(|m| weight_of(m)).sum::<i128>();
2184 for m in &orbit {
2185 working.push((0..num_vars).map(|i| Lit::new(i as u32, !m[i])).collect());
2186 }
2187 }
2188 }
2189 }
2190 z
2191}
2192
2193pub fn weighted_model_count_solve_counts(num_vars: usize, clauses: &[Vec<Lit>]) -> (usize, usize) {
2197 let gens = crate::sym_break::variable_automorphism_generators(num_vars, clauses).unwrap_or_default();
2198 let mut working = clauses.to_vec();
2199 let (mut solves, mut models) = (0usize, 0usize);
2200 loop {
2201 let mut solver = Solver::new(num_vars);
2202 for c in &working {
2203 solver.add_clause(c.clone());
2204 }
2205 match solver.solve() {
2206 SolveResult::Unsat => break,
2207 SolveResult::Sat(model) => {
2208 solves += 1;
2209 let orbit = full_assignment_orbit(num_vars, &model[..num_vars], &gens);
2210 models += orbit.len();
2211 for m in &orbit {
2212 working.push((0..num_vars).map(|i| Lit::new(i as u32, !m[i])).collect());
2213 }
2214 }
2215 }
2216 }
2217 (solves, models)
2218}
2219
2220fn rank_signatures<S: Ord + Clone>(sigs: &[S]) -> Vec<usize> {
2223 let mut distinct: Vec<S> = sigs.to_vec();
2224 distinct.sort();
2225 distinct.dedup();
2226 sigs.iter().map(|s| distinct.binary_search(s).expect("present")).collect()
2227}
2228
2229pub fn color_refinement(num_vars: usize, clauses: &[Vec<Lit>]) -> Vec<usize> {
2240 equitable_refine(num_vars, clauses, &vec![0usize; num_vars])
2241}
2242
2243fn equitable_refine(num_vars: usize, clauses: &[Vec<Lit>], var_init: &[usize]) -> Vec<usize> {
2247 let mut var_color = rank_signatures(var_init);
2248 let mut clause_color: Vec<usize> = rank_signatures(&clauses.iter().map(|c| c.len()).collect::<Vec<_>>());
2249 loop {
2250 let clause_sig: Vec<(usize, Vec<(usize, bool)>)> = clauses
2252 .iter()
2253 .enumerate()
2254 .map(|(ci, c)| {
2255 let mut nbrs: Vec<(usize, bool)> =
2256 c.iter().map(|l| (var_color[l.var() as usize], l.is_positive())).collect();
2257 nbrs.sort_unstable();
2258 (clause_color[ci], nbrs)
2259 })
2260 .collect();
2261 let new_clause_color = rank_signatures(&clause_sig);
2262 let mut var_nbrs: Vec<Vec<(usize, bool)>> = vec![Vec::new(); num_vars];
2264 for (ci, c) in clauses.iter().enumerate() {
2265 for l in c {
2266 var_nbrs[l.var() as usize].push((new_clause_color[ci], l.is_positive()));
2267 }
2268 }
2269 for nbrs in var_nbrs.iter_mut() {
2270 nbrs.sort_unstable();
2271 }
2272 let var_sig: Vec<(usize, Vec<(usize, bool)>)> =
2273 (0..num_vars).map(|v| (var_color[v], std::mem::take(&mut var_nbrs[v]))).collect();
2274 let new_var_color = rank_signatures(&var_sig);
2275 if new_var_color == var_color && new_clause_color == clause_color {
2276 break; }
2278 var_color = new_var_color;
2279 clause_color = new_clause_color;
2280 }
2281 var_color
2282}
2283
2284pub fn color_refinement_cells(num_vars: usize, clauses: &[Vec<Lit>]) -> usize {
2287 color_refinement(num_vars, clauses).iter().copied().max().map_or(0, |m| m + 1)
2288}
2289
2290pub fn provably_asymmetric_variables(num_vars: usize, clauses: &[Vec<Lit>]) -> Vec<usize> {
2294 let cells = color_refinement(num_vars, clauses);
2295 let mut size = vec![0usize; num_vars];
2296 for &c in &cells {
2297 size[c] += 1;
2298 }
2299 (0..num_vars).filter(|&v| size[cells[v]] == 1).collect()
2300}
2301
2302fn cooccurrence_matrix(num_vars: usize, clauses: &[Vec<Lit>]) -> Vec<Vec<i64>> {
2305 let mut a = vec![vec![0i64; num_vars]; num_vars];
2306 for c in clauses {
2307 let vars: Vec<usize> = c.iter().map(|l| l.var() as usize).collect();
2308 for &u in &vars {
2309 for &v in &vars {
2310 if u != v {
2311 a[u][v] += 1;
2312 }
2313 }
2314 }
2315 }
2316 a
2317}
2318
2319fn equitable_partition_of(num_vars: usize, a: &[Vec<i64>]) -> Vec<usize> {
2322 let mut color = vec![0usize; num_vars];
2323 loop {
2324 let sig: Vec<(usize, Vec<(usize, i64)>)> = (0..num_vars)
2325 .map(|u| {
2326 let mut nbrs: Vec<(usize, i64)> =
2327 (0..num_vars).filter(|&v| a[u][v] != 0).map(|v| (color[v], a[u][v])).collect();
2328 nbrs.sort_unstable();
2329 (color[u], nbrs)
2330 })
2331 .collect();
2332 let next = rank_signatures(&sig);
2333 if next == color {
2334 return color;
2335 }
2336 color = next;
2337 }
2338}
2339
2340pub fn fractional_automorphism(num_vars: usize, clauses: &[Vec<Lit>]) -> Vec<usize> {
2351 equitable_partition_of(num_vars, &cooccurrence_matrix(num_vars, clauses))
2352}
2353
2354pub fn is_fractional_automorphism(num_vars: usize, clauses: &[Vec<Lit>], partition: &[usize]) -> bool {
2359 let a = cooccurrence_matrix(num_vars, clauses);
2360 let d = partition.iter().copied().max().map_or(0, |m| m + 1);
2361 let mut cell: Vec<Vec<usize>> = vec![Vec::new(); d];
2362 for (v, &c) in partition.iter().enumerate() {
2363 cell[c].push(v);
2364 }
2365 let sum_over = |rows: &[usize], w: usize, by_row: bool| -> i64 {
2366 rows.iter().map(|&x| if by_row { a[x][w] } else { a[w][x] }).sum()
2367 };
2368 for u in 0..num_vars {
2369 for w in 0..num_vars {
2370 let cu = &cell[partition[u]];
2371 let cw = &cell[partition[w]];
2372 let lhs = cw.len() as i64 * sum_over(cu, w, true);
2374 let rhs = cu.len() as i64 * sum_over(cw, u, false);
2375 if lhs != rhs {
2376 return false;
2377 }
2378 }
2379 }
2380 true
2381}
2382
2383pub fn two_wl_pair_colors(num_vars: usize, clauses: &[Vec<Lit>]) -> Vec<Vec<usize>> {
2394 let wl1 = color_refinement(num_vars, clauses);
2395 let mut cooc: Vec<Vec<Vec<(usize, bool, bool)>>> = vec![vec![Vec::new(); num_vars]; num_vars];
2397 for c in clauses {
2398 let lits: Vec<(usize, bool)> = c.iter().map(|l| (l.var() as usize, l.is_positive())).collect();
2399 for &(vi, si) in &lits {
2400 for &(vj, sj) in &lits {
2401 if vi != vj {
2402 cooc[vi][vj].push((c.len(), si, sj));
2403 }
2404 }
2405 }
2406 }
2407 for row in cooc.iter_mut() {
2408 for s in row.iter_mut() {
2409 s.sort_unstable();
2410 }
2411 }
2412 let mut flat: Vec<(bool, usize, usize, Vec<(usize, bool, bool)>)> = Vec::with_capacity(num_vars * num_vars);
2414 for i in 0..num_vars {
2415 for j in 0..num_vars {
2416 flat.push((i == j, wl1[i], wl1[j], cooc[i][j].clone()));
2417 }
2418 }
2419 let mut color: Vec<usize> = rank_signatures(&flat); let at = |i: usize, j: usize| i * num_vars + j;
2421 loop {
2422 let mut sig: Vec<(usize, Vec<(usize, usize)>)> = Vec::with_capacity(num_vars * num_vars);
2423 for i in 0..num_vars {
2424 for j in 0..num_vars {
2425 let mut tri: Vec<(usize, usize)> =
2426 (0..num_vars).map(|k| (color[at(i, k)], color[at(k, j)])).collect();
2427 tri.sort_unstable();
2428 sig.push((color[at(i, j)], tri));
2429 }
2430 }
2431 let next = rank_signatures(&sig);
2432 if next == color {
2433 break;
2434 }
2435 color = next;
2436 }
2437 (0..num_vars).map(|i| (0..num_vars).map(|j| color[at(i, j)]).collect()).collect()
2438}
2439
2440pub fn two_wl_pair_cells(num_vars: usize, clauses: &[Vec<Lit>]) -> usize {
2442 let c = two_wl_pair_colors(num_vars, clauses);
2443 c.iter().flatten().copied().max().map_or(0, |m| m + 1)
2444}
2445
2446pub fn two_wl_fingerprint(num_vars: usize, clauses: &[Vec<Lit>]) -> Vec<usize> {
2450 let c = two_wl_pair_colors(num_vars, clauses);
2451 let k = c.iter().flatten().copied().max().map_or(0, |m| m + 1);
2452 let mut sizes = vec![0usize; k];
2453 for &col in c.iter().flatten() {
2454 sizes[col] += 1;
2455 }
2456 sizes.sort_unstable();
2457 sizes
2458}
2459
2460pub fn coherent_configuration_constants(num_vars: usize, clauses: &[Vec<Lit>]) -> Option<(usize, Vec<Vec<Vec<u128>>>)> {
2471 let n = num_vars;
2472 let pc = two_wl_pair_colors(n, clauses);
2473 let d = pc.iter().flatten().copied().max().map_or(0, |m| m + 1);
2474 if d == 0 {
2475 return None;
2476 }
2477 let count_matrix = |x: usize, y: usize| -> Vec<Vec<u128>> {
2479 let mut m = vec![vec![0u128; d]; d];
2480 for z in 0..n {
2481 m[pc[x][z]][pc[z][y]] += 1;
2482 }
2483 m
2484 };
2485 let mut rep: Vec<Option<(usize, usize)>> = vec![None; d];
2487 for i in 0..n {
2488 for j in 0..n {
2489 rep[pc[i][j]].get_or_insert((i, j));
2490 }
2491 }
2492 let mut p = vec![vec![vec![0u128; d]; d]; d];
2493 for k in 0..d {
2494 let (x, y) = rep[k]?;
2495 let m = count_matrix(x, y);
2496 for i in 0..d {
2497 for j in 0..d {
2498 p[i][j][k] = m[i][j];
2499 }
2500 }
2501 }
2502 for x in 0..n {
2504 for y in 0..n {
2505 let k = pc[x][y];
2506 let m = count_matrix(x, y);
2507 for i in 0..d {
2508 for j in 0..d {
2509 if m[i][j] != p[i][j][k] {
2510 return None;
2511 }
2512 }
2513 }
2514 }
2515 }
2516 Some((d, p))
2517}
2518
2519pub fn coherent_rank(num_vars: usize, clauses: &[Vec<Lit>]) -> Option<usize> {
2523 coherent_configuration_constants(num_vars, clauses).map(|(d, _)| d)
2524}
2525
2526fn gf_simultaneous_eigenvalues(mmats: &[Vec<Vec<u64>>], d: usize, p: u64) -> Option<Vec<Vec<u64>>> {
2532 use crate::permgroup::{gf_mat_vec, gf_nullspace, mod_inv};
2533 let mut subspaces: Vec<Vec<Vec<u64>>> = vec![(0..d)
2534 .map(|i| {
2535 let mut e = vec![0u64; d];
2536 e[i] = 1;
2537 e
2538 })
2539 .collect()];
2540 for mi in mmats {
2541 if subspaces.iter().all(|s| s.len() == 1) {
2542 break;
2543 }
2544 let mut next: Vec<Vec<Vec<u64>>> = Vec::new();
2545 for s in &subspaces {
2546 if s.len() == 1 {
2547 next.push(s.clone());
2548 continue;
2549 }
2550 let bn = s.len();
2551 let mb: Vec<Vec<u64>> = s.iter().map(|b| gf_mat_vec(mi, b, p)).collect();
2552 let mut pieces: Vec<Vec<Vec<u64>>> = Vec::new();
2553 let mut covered = 0usize;
2554 for lam in 0..p {
2555 let mut rows = vec![vec![0u64; bn]; d];
2556 for k in 0..d {
2557 for (jj, sj) in s.iter().enumerate() {
2558 let shift = (lam as u128 * sj[k] as u128) % p as u128;
2559 rows[k][jj] = ((mb[jj][k] as u128 + p as u128 - shift) % p as u128) as u64;
2560 }
2561 }
2562 let ns = gf_nullspace(rows, bn, p);
2563 if ns.is_empty() {
2564 continue;
2565 }
2566 let eig: Vec<Vec<u64>> = ns
2567 .iter()
2568 .map(|c| {
2569 let mut x = vec![0u64; d];
2570 for (jj, &cj) in c.iter().enumerate() {
2571 if cj != 0 {
2572 for k in 0..d {
2573 x[k] = ((x[k] as u128 + cj as u128 * s[jj][k] as u128) % p as u128) as u64;
2574 }
2575 }
2576 }
2577 x
2578 })
2579 .collect();
2580 covered += eig.len();
2581 pieces.push(eig);
2582 if covered == bn {
2583 break;
2584 }
2585 }
2586 if covered == bn {
2587 next.extend(pieces);
2588 } else {
2589 next.push(s.clone());
2590 }
2591 }
2592 subspaces = next;
2593 }
2594 if subspaces.iter().any(|s| s.len() != 1) {
2595 return None; }
2597 Some(
2598 subspaces
2599 .iter()
2600 .map(|s| {
2601 let v = &s[0];
2602 let t = v.iter().position(|&x| x != 0).unwrap();
2603 let inv = mod_inv(v[t], p);
2604 mmats
2605 .iter()
2606 .map(|mi| {
2607 let mv = gf_mat_vec(mi, v, p);
2608 (mv[t] as u128 * inv as u128 % p as u128) as u64
2609 })
2610 .collect()
2611 })
2612 .collect(),
2613 )
2614}
2615
2616pub fn association_scheme_eigenmatrix(num_vars: usize, clauses: &[Vec<Lit>]) -> Option<(u64, Vec<Vec<u64>>)> {
2628 let (d, a) = coherent_configuration_constants(num_vars, clauses)?;
2629 if d == 0 {
2630 return None;
2631 }
2632 for i in 0..d {
2634 for j in 0..d {
2635 for k in 0..d {
2636 if a[i][j][k] != a[j][i][k] {
2637 return None;
2638 }
2639 }
2640 }
2641 }
2642 let valency: Vec<u128> = (0..d).map(|i| (0..d).map(|j| a[i][j][0]).sum()).collect();
2644 let mut tried = 0;
2645 let mut p = 2u64;
2646 while tried < 200 && p < 100_000 {
2647 if crate::permgroup::is_prime(p) {
2648 tried += 1;
2649 let mmats: Vec<Vec<Vec<u64>>> = (0..d)
2650 .map(|i| (0..d).map(|k| (0..d).map(|j| (a[i][j][k] % p as u128) as u64).collect()).collect())
2651 .collect();
2652 if let Some(rows) = gf_simultaneous_eigenvalues(&mmats, d, p) {
2653 let hom_ok = rows.iter().all(|row| {
2655 (0..d).all(|i| {
2656 (0..d).all(|j| {
2657 let lhs = row[i] as u128 * row[j] as u128 % p as u128;
2658 let rhs = (0..d)
2659 .map(|k| (a[i][j][k] % p as u128) * row[k] as u128 % p as u128)
2660 .sum::<u128>()
2661 % p as u128;
2662 lhs == rhs
2663 })
2664 })
2665 });
2666 let has_valency =
2667 rows.iter().any(|row| (0..d).all(|i| row[i] as u128 == valency[i] % p as u128));
2668 if hom_ok && has_valency {
2669 return Some((p, rows));
2670 }
2671 }
2672 }
2673 p += 1;
2674 }
2675 None
2676}
2677
2678pub fn association_scheme_multiplicities(num_vars: usize, clauses: &[Vec<Lit>]) -> Option<Vec<u128>> {
2689 let (d, a) = coherent_configuration_constants(num_vars, clauses)?;
2690 if d == 0 {
2691 return None;
2692 }
2693 for i in 0..d {
2694 for j in 0..d {
2695 for k in 0..d {
2696 if a[i][j][k] != a[j][i][k] {
2697 return None; }
2699 }
2700 }
2701 }
2702 let valency: Vec<u128> = (0..d).map(|i| (0..d).map(|j| a[i][j][0]).sum()).collect();
2703 let pc = two_wl_pair_colors(num_vars, clauses);
2705 let mut transpose = vec![usize::MAX; d];
2706 for x in 0..num_vars {
2707 for y in 0..num_vars {
2708 let i = pc[x][y];
2709 if transpose[i] == usize::MAX {
2710 transpose[i] = pc[y][x];
2711 }
2712 }
2713 }
2714 let n = num_vars as u128;
2715 let mut tried = 0;
2716 let mut p = 2u64;
2717 while tried < 300 && p < 1_000_000 {
2718 if crate::permgroup::is_prime(p) && p as u128 > n {
2720 tried += 1;
2721 let mmats: Vec<Vec<Vec<u64>>> = (0..d)
2722 .map(|i| (0..d).map(|k| (0..d).map(|j| (a[i][j][k] % p as u128) as u64).collect()).collect())
2723 .collect();
2724 if let Some(rows) = gf_simultaneous_eigenvalues(&mmats, d, p) {
2725 let mut mult = Vec::with_capacity(d);
2726 let mut ok = true;
2727 for row in &rows {
2728 let mut denom = 0u64;
2729 for i in 0..d {
2730 let ki = (valency[i] % p as u128) as u64;
2731 let term = (row[i] as u128 * row[transpose[i]] as u128 % p as u128) as u64;
2732 denom = ((denom as u128 + term as u128 * crate::permgroup::mod_inv(ki, p) as u128)
2733 % p as u128) as u64;
2734 }
2735 if denom == 0 {
2736 ok = false;
2737 break;
2738 }
2739 let m = (n % p as u128) * crate::permgroup::mod_inv(denom, p) as u128 % p as u128;
2740 if m == 0 || m > n {
2741 ok = false;
2742 break;
2743 }
2744 mult.push(m);
2745 }
2746 let trivial_ok = ok
2747 && rows.iter().zip(&mult).any(|(row, &m)| {
2748 m == 1 && (0..d).all(|i| row[i] as u128 == valency[i] % p as u128)
2749 });
2750 if ok && trivial_ok && mult.iter().sum::<u128>() == n {
2751 mult.sort_unstable();
2752 return Some(mult);
2753 }
2754 }
2755 }
2756 p += 1;
2757 }
2758 None
2759}
2760
2761pub fn three_wl_colors(num_vars: usize, clauses: &[Vec<Lit>]) -> Vec<Vec<Vec<usize>>> {
2771 let n = num_vars;
2772 let pc = two_wl_pair_colors(n, clauses);
2773 let at = |i: usize, j: usize, k: usize| (i * n + j) * n + k;
2774 let init: Vec<(usize, usize, usize)> = (0..n)
2775 .flat_map(|i| (0..n).flat_map(move |j| (0..n).map(move |k| (i, j, k))))
2776 .map(|(i, j, k)| (pc[i][j], pc[i][k], pc[j][k]))
2777 .collect();
2778 let mut color = rank_signatures(&init);
2779 loop {
2780 let mut sig: Vec<(usize, Vec<(usize, usize, usize)>)> = Vec::with_capacity(n * n * n);
2781 for i in 0..n {
2782 for j in 0..n {
2783 for k in 0..n {
2784 let mut nbr: Vec<(usize, usize, usize)> =
2785 (0..n).map(|w| (color[at(w, j, k)], color[at(i, w, k)], color[at(i, j, w)])).collect();
2786 nbr.sort_unstable();
2787 sig.push((color[at(i, j, k)], nbr));
2788 }
2789 }
2790 }
2791 let next = rank_signatures(&sig);
2792 if next == color {
2793 break;
2794 }
2795 color = next;
2796 }
2797 (0..n)
2798 .map(|i| (0..n).map(|j| (0..n).map(|k| color[at(i, j, k)]).collect()).collect())
2799 .collect()
2800}
2801
2802pub fn three_wl_fingerprint(num_vars: usize, clauses: &[Vec<Lit>]) -> Vec<usize> {
2805 let c = three_wl_colors(num_vars, clauses);
2806 let max = c.iter().flatten().flatten().copied().max().map_or(0, |m| m + 1);
2807 let mut sizes = vec![0usize; max];
2808 for &col in c.iter().flatten().flatten() {
2809 sizes[col] += 1;
2810 }
2811 sizes.sort_unstable();
2812 sizes
2813}
2814
2815fn formula_certificate(clauses: &[Vec<Lit>], coloring: &[usize]) -> Vec<Vec<(usize, bool)>> {
2819 let label = rank_signatures(coloring); let mut cls: Vec<Vec<(usize, bool)>> = clauses
2821 .iter()
2822 .map(|c| {
2823 let mut lits: Vec<(usize, bool)> =
2824 c.iter().map(|l| (label[l.var() as usize], l.is_positive())).collect();
2825 lits.sort_unstable();
2826 lits
2827 })
2828 .collect();
2829 cls.sort_unstable();
2830 cls
2831}
2832
2833fn ir_canonical(
2837 num_vars: usize,
2838 clauses: &[Vec<Lit>],
2839 colors: &[usize],
2840 nodes: &mut usize,
2841 cap: usize,
2842) -> Option<Vec<Vec<(usize, bool)>>> {
2843 *nodes += 1;
2844 if *nodes > cap {
2845 return None;
2846 }
2847 let refined = equitable_refine(num_vars, clauses, colors);
2848 let d = refined.iter().copied().max().map_or(0, |m| m + 1);
2849 let mut members: Vec<Vec<usize>> = vec![Vec::new(); d];
2850 for (v, &c) in refined.iter().enumerate() {
2851 members[c].push(v);
2852 }
2853 match (0..d).find(|&c| members[c].len() > 1) {
2854 None => Some(formula_certificate(clauses, &refined)), Some(c) => {
2856 let mut best: Option<Vec<Vec<(usize, bool)>>> = None;
2857 for &v in &members[c] {
2858 let mut nc = refined.clone();
2859 nc[v] = d; let leaf = ir_canonical(num_vars, clauses, &nc, nodes, cap)?;
2861 if best.as_ref().map_or(true, |b| leaf > *b) {
2862 best = Some(leaf);
2863 }
2864 }
2865 best
2866 }
2867 }
2868}
2869
2870pub fn canonical_form(num_vars: usize, clauses: &[Vec<Lit>]) -> Option<Vec<Vec<(usize, bool)>>> {
2877 let mut nodes = 0;
2878 ir_canonical(num_vars, clauses, &vec![0usize; num_vars], &mut nodes, 200_000)
2879}
2880
2881pub fn formulas_isomorphic(num_vars: usize, f: &[Vec<Lit>], g: &[Vec<Lit>]) -> Option<bool> {
2885 Some(canonical_form(num_vars, f)? == canonical_form(num_vars, g)?)
2886}
2887
2888fn is_declared_symmetry(num_vars: usize, clauses: &[Vec<Lit>], g: &[usize]) -> bool {
2893 if g.len() != num_vars {
2894 return false;
2895 }
2896 let mut seen = vec![false; num_vars];
2897 for &x in g {
2898 if x >= num_vars || seen[x] {
2899 return false; }
2901 seen[x] = true;
2902 }
2903 let clause_set: HashSet<Vec<(u32, bool)>> = clauses.iter().map(|c| canon_clause(c)).collect();
2904 let syntactic = clauses.iter().all(|c| clause_set.contains(&canon_clause(&apply_perm_to_clause(c, g))));
2905 syntactic
2906 || clauses.iter().all(|c| {
2907 let gc = apply_perm_to_clause(c, g);
2908 clause_set.contains(&canon_clause(&gc)) || clause_is_implied(num_vars, clauses, &gc)
2909 })
2910}
2911
2912pub fn solve_with_declared_symmetry(
2922 num_vars: usize,
2923 clauses: &[Vec<Lit>],
2924 declared: &[crate::permgroup::Perm],
2925) -> Solved {
2926 let mut gens = crate::sym_break::variable_automorphism_generators(num_vars, clauses).unwrap_or_default();
2927 for g in declared {
2928 if is_declared_symmetry(num_vars, clauses, g) {
2929 gens.push(g.clone());
2930 }
2931 }
2932 if gens.is_empty() {
2933 return solve_comprehensive(num_vars, clauses);
2934 }
2935 let bsgs = crate::permgroup::schreier_sims(num_vars, &gens);
2936 let to_litsym = |p: &[usize]| -> Vec<Lit> { (0..num_vars).map(|v| Lit::pos(p[v] as u32)).collect() };
2937 let group: Vec<Vec<Lit>> = match bsgs.elements(50_000) {
2938 Some(elts) => elts.iter().map(|p| to_litsym(p)).collect(),
2939 None => gens.iter().map(|p| to_litsym(p)).collect(),
2940 };
2941 let (sbp, total) = crate::sym_break::lex_leader_sbp_lit(num_vars, &group);
2942 let mut solver = Solver::new(total);
2943 for c in clauses {
2944 solver.add_clause(c.clone());
2945 }
2946 for c in &sbp {
2947 solver.add_clause(c.clone());
2948 }
2949 match solver.solve() {
2950 SolveResult::Sat(model) => {
2951 let projected: Vec<bool> = model[..num_vars].to_vec();
2952 if clauses.iter().all(|c| c.iter().any(|l| projected[l.var() as usize] == l.is_positive())) {
2953 Solved { answer: Answer::Sat(projected), via: Route::DeclaredSymmetry, proof: Vec::new(), conflicts: solver.conflicts() }
2954 } else {
2955 solve_comprehensive(num_vars, clauses) }
2957 }
2958 SolveResult::Unsat => {
2959 Solved { answer: Answer::Unsat, via: Route::DeclaredSymmetry, proof: Vec::new(), conflicts: solver.conflicts() }
2960 }
2961 }
2962}
2963
2964#[derive(Clone, Debug, PartialEq, Eq)]
2966pub struct SymmetricCount {
2967 pub representatives: Vec<Vec<bool>>,
2970 pub total_models: u128,
2973 pub exhaustive: bool,
2975}
2976
2977fn assignment_orbit(num_vars: usize, m: &[bool], gens: &[crate::permgroup::Perm], occurs: &[usize]) -> Vec<Vec<bool>> {
2980 let proj = |a: &[bool]| -> Vec<bool> { occurs.iter().map(|&v| a[v]).collect() };
2981 let mut seen: HashSet<Vec<bool>> = HashSet::from([proj(m)]);
2982 let mut out = vec![m.to_vec()];
2983 let mut i = 0;
2984 while i < out.len() {
2985 let cur = out[i].clone();
2986 i += 1;
2987 for g in gens {
2988 let mut pm = vec![false; num_vars];
2989 for v in 0..num_vars {
2990 pm[g[v]] = cur[v];
2991 }
2992 if seen.insert(proj(&pm)) {
2993 out.push(pm);
2994 }
2995 }
2996 }
2997 out
2998}
2999
3000pub fn models_up_to_symmetry(num_vars: usize, clauses: &[Vec<Lit>], cap: usize) -> SymmetricCount {
3009 let mut appears = vec![false; num_vars];
3010 for c in clauses {
3011 for l in c {
3012 appears[l.var() as usize] = true;
3013 }
3014 }
3015 let occurs: Vec<usize> = (0..num_vars).filter(|&v| appears[v]).collect();
3016 let gens = crate::sym_break::variable_automorphism_generators(num_vars, clauses).unwrap_or_default();
3017
3018 let mut working = clauses.to_vec();
3019 let mut representatives: Vec<Vec<bool>> = Vec::new();
3020 let mut total_models: u128 = 0;
3021 let mut exhaustive = true;
3022 loop {
3023 if representatives.len() >= cap {
3024 exhaustive = false;
3025 break;
3026 }
3027 match solve_comprehensive(num_vars, &working).answer {
3028 Answer::Unsat => break,
3029 Answer::Sat(m) => {
3030 let orbit = assignment_orbit(num_vars, &m, &gens, &occurs);
3031 total_models = total_models.saturating_add(orbit.len() as u128);
3032 representatives.push(m);
3033 for a in &orbit {
3034 working.push(occurs.iter().map(|&v| Lit::new(v as u32, !a[v])).collect());
3036 }
3037 }
3038 }
3039 }
3040 SymmetricCount { representatives, total_models, exhaustive }
3041}
3042
3043#[derive(Clone, Debug, PartialEq, Eq)]
3047pub struct SymmetryProfile {
3048 pub order: u128,
3050 pub generators: usize,
3052 pub num_orbits: usize,
3054 pub rank: usize,
3056 pub transitivity: usize,
3058 pub primitive: bool,
3060 pub blocks: Option<usize>,
3062 pub abelian: bool,
3064 pub solvable: Option<bool>,
3067 pub nilpotent: Option<bool>,
3070 pub derived_length: Option<usize>,
3073 pub nilpotency_class: Option<usize>,
3075 pub derived_order: u128,
3077 pub conjugacy_classes: Option<usize>,
3080 pub center_order: Option<u128>,
3082 pub exponent: Option<u128>,
3085 pub assignment_orbits: Option<u128>,
3088 pub abelianization: Option<(u128, u128)>,
3091 pub subgroups: Option<usize>,
3094 pub simple: Option<bool>,
3097 pub composition_factors: Option<Vec<u128>>,
3100 pub sylow: Option<Vec<(u128, usize)>>,
3103 pub real_classes: Option<usize>,
3106 pub rational_classes: Option<usize>,
3110 pub irreducible_degrees: Option<Vec<u128>>,
3114 pub frobenius_schur: Option<Vec<i8>>,
3118 pub isotypic_multiplicities: Option<Vec<u128>>,
3122 pub automorphism_order: Option<u128>,
3126 pub outer_automorphism_order: Option<u128>,
3129 pub coherent_rank: Option<usize>,
3135}
3136
3137pub fn symmetry_structure(num_vars: usize, clauses: &[Vec<Lit>]) -> SymmetryProfile {
3142 let gens = crate::sym_break::variable_automorphism_generators(num_vars, clauses).unwrap_or_default();
3143 let mut profile = profile_of_generators(num_vars, &gens);
3144 profile.coherent_rank = Some(coherent_rank(num_vars, clauses).unwrap_or_else(|| two_wl_pair_cells(num_vars, clauses)));
3147 profile
3148}
3149
3150fn profile_of_generators(num_vars: usize, gens: &[crate::permgroup::Perm]) -> SymmetryProfile {
3154 if gens.is_empty() {
3155 return SymmetryProfile {
3156 order: 1,
3157 generators: 0,
3158 num_orbits: num_vars,
3159 rank: 0,
3160 transitivity: 0,
3161 primitive: false,
3162 blocks: None,
3163 abelian: true, solvable: Some(true),
3165 nilpotent: Some(true),
3166 derived_length: Some(0),
3167 nilpotency_class: Some(0),
3168 derived_order: 1,
3169 conjugacy_classes: Some(1),
3170 center_order: Some(1),
3171 exponent: Some(1),
3172 assignment_orbits: Some(1u128 << num_vars.min(127)),
3173 abelianization: Some((1, 1)),
3174 subgroups: Some(1),
3175 simple: Some(false), composition_factors: Some(Vec::new()),
3177 sylow: Some(Vec::new()),
3178 irreducible_degrees: Some(vec![1]), frobenius_schur: Some(vec![1]), isotypic_multiplicities: Some(vec![num_vars as u128]),
3182 real_classes: Some(1),
3183 rational_classes: Some(1), automorphism_order: Some(1), outer_automorphism_order: Some(1),
3186 coherent_rank: None, };
3188 }
3189 let gens = gens.to_vec();
3190 let order = crate::permgroup::schreier_sims(num_vars, &gens).order();
3191 let num_orbits = crate::permgroup::orbits(num_vars, &gens).len();
3192 let rank = if num_vars <= 48 { crate::permgroup::rank(num_vars, &gens) } else { 0 };
3193 let transitivity =
3194 if num_vars <= 24 { crate::permgroup::transitivity_degree(num_vars, &gens, 3) } else { 0 };
3195 let primitive = crate::permgroup::is_primitive(num_vars, &gens);
3196 let blocks = crate::permgroup::minimal_block_system(num_vars, &gens).map(|b| b.len());
3197 let abelian = crate::permgroup::is_abelian(num_vars, &gens);
3198 let (solvable, nilpotent, derived_length, nilpotency_class, derived_order) = if num_vars <= 24 {
3201 let dl = crate::permgroup::derived_length(num_vars, &gens);
3202 let nc = crate::permgroup::nilpotency_class(num_vars, &gens);
3203 let d = crate::permgroup::derived_subgroup(num_vars, &gens);
3204 (Some(dl.is_some()), Some(nc.is_some()), dl, nc, crate::permgroup::schreier_sims(num_vars, &d).order())
3205 } else {
3206 (None, None, None, None, 0)
3207 };
3208 const ENUM_CAP: usize = 4096;
3210 let classes = crate::permgroup::conjugacy_classes(num_vars, &gens, ENUM_CAP);
3211 let conjugacy_classes = classes.as_ref().map(|c| c.len());
3212 let center_order = classes.map(|c| c.iter().filter(|cls| cls.len() == 1).count() as u128);
3213 let exponent = crate::permgroup::exponent(num_vars, &gens, ENUM_CAP);
3214 let assignment_orbits = crate::permgroup::polya_count(num_vars, &gens, 2, ENUM_CAP);
3215 let abelianization = crate::permgroup::abelianization(num_vars, &gens, ENUM_CAP);
3216 let subgroups = crate::permgroup::subgroup_count(num_vars, &gens, 256);
3218 let simple = crate::permgroup::is_simple(num_vars, &gens, ENUM_CAP);
3219 let composition_factors = crate::permgroup::composition_factor_orders(num_vars, &gens, 256);
3221 let sylow = crate::permgroup::sylow_counts(num_vars, &gens, 256);
3222 let real_classes = crate::permgroup::real_class_count(num_vars, &gens, ENUM_CAP);
3223 let rational_classes = crate::permgroup::rational_class_count(num_vars, &gens, ENUM_CAP);
3224 let ctable = crate::permgroup::character_table(num_vars, &gens, ENUM_CAP);
3227 let irreducible_degrees = ctable.as_ref().map(|t| t.degrees.clone());
3228 let frobenius_schur = ctable.as_ref().and_then(crate::permgroup::frobenius_schur_from_table);
3229 let isotypic_multiplicities =
3230 ctable.as_ref().and_then(|t| crate::permgroup::isotypic_from_table(num_vars, &gens, t));
3231 let automorphism_order = crate::permgroup::automorphism_group_order(num_vars, &gens, 256);
3233 let outer_automorphism_order = match (automorphism_order, center_order) {
3234 (Some(a), Some(c)) if c > 0 => Some(a / (order / c)), _ => None,
3236 };
3237 SymmetryProfile {
3238 order,
3239 generators: gens.len(),
3240 num_orbits,
3241 rank,
3242 transitivity,
3243 primitive,
3244 blocks,
3245 abelian,
3246 solvable,
3247 nilpotent,
3248 derived_length,
3249 nilpotency_class,
3250 derived_order,
3251 conjugacy_classes,
3252 center_order,
3253 exponent,
3254 assignment_orbits,
3255 abelianization,
3256 subgroups,
3257 simple,
3258 composition_factors,
3259 sylow,
3260 real_classes,
3261 rational_classes,
3262 irreducible_degrees,
3263 frobenius_schur,
3264 isotypic_multiplicities,
3265 automorphism_order,
3266 outer_automorphism_order,
3267 coherent_rank: None, }
3269}
3270
3271pub fn pb_symmetry_profile(num_vars: usize, constraints: &[crate::pseudo_boolean::PbConstraint]) -> SymmetryProfile {
3276 let gens = crate::pseudo_boolean::coeff_symmetry_generators(num_vars, constraints);
3277 profile_of_generators(num_vars, &gens)
3278}
3279
3280pub fn class_algebra_constants(num_vars: usize, clauses: &[Vec<Lit>]) -> Option<Vec<Vec<Vec<u128>>>> {
3284 let gens = crate::sym_break::variable_automorphism_generators(num_vars, clauses).unwrap_or_default();
3285 crate::permgroup::class_multiplication_coefficients(num_vars, &gens, 4096)
3286}
3287
3288pub fn character_table(num_vars: usize, clauses: &[Vec<Lit>]) -> Option<crate::permgroup::CharacterTable> {
3292 let gens = crate::sym_break::variable_automorphism_generators(num_vars, clauses).unwrap_or_default();
3293 crate::permgroup::character_table(num_vars, &gens, 4096)
3294}
3295
3296pub fn frobenius_schur_indicators(num_vars: usize, clauses: &[Vec<Lit>]) -> Option<Vec<i8>> {
3300 let gens = crate::sym_break::variable_automorphism_generators(num_vars, clauses).unwrap_or_default();
3301 crate::permgroup::frobenius_schur_indicators(num_vars, &gens, 4096)
3302}
3303
3304pub fn permutation_character(num_vars: usize, clauses: &[Vec<Lit>]) -> Option<Vec<u128>> {
3308 let gens = crate::sym_break::variable_automorphism_generators(num_vars, clauses).unwrap_or_default();
3309 crate::permgroup::permutation_character(num_vars, &gens, 4096)
3310}
3311
3312pub fn isotypic_multiplicities(num_vars: usize, clauses: &[Vec<Lit>]) -> Option<Vec<u128>> {
3316 let gens = crate::sym_break::variable_automorphism_generators(num_vars, clauses).unwrap_or_default();
3317 crate::permgroup::isotypic_multiplicities(num_vars, &gens, 4096)
3318}
3319
3320pub fn tensor_decomposition(num_vars: usize, clauses: &[Vec<Lit>]) -> Option<Vec<Vec<Vec<u128>>>> {
3324 let gens = crate::sym_break::variable_automorphism_generators(num_vars, clauses).unwrap_or_default();
3325 crate::permgroup::tensor_decomposition(num_vars, &gens, 4096)
3326}
3327
3328pub fn galois_class_orbits(num_vars: usize, clauses: &[Vec<Lit>]) -> Option<Vec<Vec<usize>>> {
3332 let gens = crate::sym_break::variable_automorphism_generators(num_vars, clauses).unwrap_or_default();
3333 crate::permgroup::galois_class_orbits(num_vars, &gens, 4096)
3334}
3335
3336pub fn table_of_marks(num_vars: usize, clauses: &[Vec<Lit>]) -> Option<(Vec<u128>, Vec<Vec<u128>>)> {
3340 let gens = crate::sym_break::variable_automorphism_generators(num_vars, clauses).unwrap_or_default();
3341 crate::permgroup::table_of_marks(num_vars, &gens, 256)
3342}
3343
3344pub fn burnside_ring_product(num_vars: usize, clauses: &[Vec<Lit>]) -> Option<Vec<Vec<Vec<i128>>>> {
3348 let gens = crate::sym_break::variable_automorphism_generators(num_vars, clauses).unwrap_or_default();
3349 crate::permgroup::burnside_ring_product(num_vars, &gens, 256)
3350}
3351
3352pub fn mobius_number(num_vars: usize, clauses: &[Vec<Lit>]) -> Option<i128> {
3355 let gens = crate::sym_break::variable_automorphism_generators(num_vars, clauses).unwrap_or_default();
3356 crate::permgroup::mobius_number(num_vars, &gens, 256)
3357}
3358
3359pub fn generating_tuple_count(num_vars: usize, clauses: &[Vec<Lit>], k: u32) -> Option<i128> {
3363 let gens = crate::sym_break::variable_automorphism_generators(num_vars, clauses).unwrap_or_default();
3364 crate::permgroup::generating_tuple_count(num_vars, &gens, 256, k)
3365}
3366
3367pub fn permutation_character_decomposition(
3372 num_vars: usize,
3373 clauses: &[Vec<Lit>],
3374) -> Option<(Vec<u128>, Vec<u128>, Vec<Vec<u128>>)> {
3375 let gens = crate::sym_break::variable_automorphism_generators(num_vars, clauses).unwrap_or_default();
3376 crate::permgroup::permutation_character_decomposition(num_vars, &gens, 256)
3377}
3378
3379pub fn automorphism_group_order(num_vars: usize, clauses: &[Vec<Lit>]) -> Option<u128> {
3382 let gens = crate::sym_break::variable_automorphism_generators(num_vars, clauses).unwrap_or_default();
3383 crate::permgroup::automorphism_group_order(num_vars, &gens, 256)
3384}
3385
3386pub fn assignment_weight_inventory(num_vars: usize, clauses: &[Vec<Lit>]) -> Option<Vec<u128>> {
3391 let gens = crate::sym_break::variable_automorphism_generators(num_vars, clauses).unwrap_or_default();
3392 crate::permgroup::pattern_inventory(num_vars, &gens, 4096)
3393}
3394
3395pub fn break_all_symmetry(num_vars: usize, clauses: &[Vec<Lit>]) -> Vec<Vec<Lit>> {
3405 let key = |a: Lit, b: Lit| -> (u32, bool, u32, bool) {
3406 let (x, y) = ((a.var(), a.is_positive()), (b.var(), b.is_positive()));
3407 if x <= y { (x.0, x.1, y.0, y.1) } else { (y.0, y.1, x.0, x.1) }
3408 };
3409 let mut combined = clauses.to_vec();
3410 let mut seen: HashSet<(u32, bool, u32, bool)> =
3411 combined.iter().filter(|c| c.len() == 2).map(|c| key(c[0], c[1])).collect();
3412 loop {
3413 let gens =
3414 crate::sym_break::variable_automorphism_generators(num_vars, &combined).unwrap_or_default();
3415 if gens.is_empty() {
3416 break; }
3418 let bsgs = crate::permgroup::schreier_sims(num_vars, &gens);
3419 let mut added = false;
3420 for orbit in crate::permgroup::orbits(num_vars, &gens) {
3424 if orbit.len() < 2 {
3425 continue;
3426 }
3427 let full = orbit.windows(2).all(|w| {
3428 let mut t: Vec<usize> = (0..num_vars).collect();
3429 t.swap(w[0], w[1]);
3430 bsgs.contains(&t)
3431 });
3432 if full {
3433 for w in orbit.windows(2) {
3434 let (a, b) = (Lit::neg(w[0] as u32), Lit::pos(w[1] as u32)); if seen.insert(key(a, b)) {
3436 combined.push(vec![a, b]);
3437 added = true;
3438 }
3439 }
3440 }
3441 }
3442 if !added {
3444 for g in &gens {
3445 let Some(v) = (0..num_vars).find(|&i| g[i] != i) else { continue };
3446 let (a, b) = (Lit::neg(v as u32), Lit::pos(g[v] as u32)); if seen.insert(key(a, b)) {
3448 combined.push(vec![a, b]);
3449 added = true;
3450 }
3451 }
3452 }
3453 if !added {
3454 break; }
3456 }
3457 combined
3458}
3459
3460pub fn break_all_symmetry_complete(num_vars: usize, clauses: &[Vec<Lit>]) -> (Vec<Vec<Lit>>, usize) {
3468 let gens = crate::sym_break::variable_automorphism_generators(num_vars, clauses).unwrap_or_default();
3469 if gens.is_empty() {
3470 return (clauses.to_vec(), num_vars);
3471 }
3472 let bsgs = crate::permgroup::schreier_sims(num_vars, &gens);
3473 let to_litsym = |p: &[usize]| -> Vec<Lit> { (0..num_vars).map(|v| Lit::pos(p[v] as u32)).collect() };
3474 let group: Vec<Vec<Lit>> = match bsgs.elements(50_000) {
3475 Some(elts) => elts.iter().map(|p| to_litsym(p)).collect(), None => {
3477 let mut g: Vec<Vec<Lit>> = gens.iter().map(|p| to_litsym(p)).collect();
3479 g.extend(bsgs.transversal_elements().iter().map(|p| to_litsym(p)));
3480 g
3481 }
3482 };
3483 let (sbp, total) = crate::sym_break::lex_leader_sbp_lit(num_vars, &group);
3484 let mut combined = clauses.to_vec();
3485 combined.extend(sbp);
3486 (combined, total)
3487}
3488
3489pub fn solve_by_symmetry_breaking(num_vars: usize, clauses: &[Vec<Lit>]) -> Solved {
3497 let broken = break_all_symmetry(num_vars, clauses);
3498 let inner = solve_comprehensive(num_vars, &broken);
3499 match inner.answer {
3500 Answer::Sat(model) => {
3501 if clauses.iter().all(|c| c.iter().any(|l| model[l.var() as usize] == l.is_positive())) {
3502 Solved { answer: Answer::Sat(model), via: inner.via, proof: inner.proof, conflicts: inner.conflicts }
3503 } else {
3504 solve_comprehensive(num_vars, clauses) }
3506 }
3507 Answer::Unsat => Solved { answer: Answer::Unsat, via: inner.via, proof: inner.proof, conflicts: inner.conflicts },
3508 }
3509}
3510
3511fn modp_route(num_vars: usize, clauses: &[Vec<Lit>]) -> Option<Solved> {
3517 use crate::modp::{self, ModpOutcome};
3518 let rec = modp::recover_from_cnf(num_vars, clauses)?;
3519
3520 let build_model = |assign: &[u64]| -> Option<Vec<bool>> {
3523 let mut model = vec![false; num_vars];
3524 for (g, group) in rec.groups.iter().enumerate() {
3525 if let Some(&bit) = group.get(*assign.get(g).unwrap_or(&0) as usize) {
3526 if (bit as usize) < model.len() {
3527 model[bit as usize] = true;
3528 }
3529 }
3530 }
3531 clauses
3532 .iter()
3533 .all(|c| c.iter().any(|l| model.get(l.var() as usize).copied().unwrap_or(false) == l.is_positive()))
3534 .then_some(model)
3535 };
3536
3537 if modp::is_prime(rec.modulus) {
3538 match modp::solve(&rec.equations, rec.num_vars, rec.modulus) {
3540 ModpOutcome::Unsat(combo) => {
3541 debug_assert!(
3542 modp::is_refutation(&rec.equations, rec.num_vars, rec.modulus, &combo),
3543 "the recovered GF(p) refutation must re-check"
3544 );
3545 Some(Solved::unsat(Route::ModP))
3546 }
3547 ModpOutcome::Sat(assign) => Some(Solved {
3548 answer: Answer::Sat(build_model(&assign)?),
3549 via: Route::ModP,
3550 proof: Vec::new(),
3551 conflicts: 0,
3552 }),
3553 }
3554 } else {
3555 use crate::modm::{self, ModmOutcome};
3557 match modm::solve(&rec.equations, rec.num_vars, rec.modulus)? {
3558 ModmOutcome::Unsat { modulus, combo } => {
3559 debug_assert!(
3560 modm::is_refutation(&rec.equations, rec.num_vars, modulus, &combo),
3561 "the recovered ℤ/m refutation must re-check"
3562 );
3563 Some(Solved::unsat(Route::ModM))
3564 }
3565 ModmOutcome::Sat(assign) => Some(Solved {
3566 answer: Answer::Sat(build_model(&assign)?),
3567 via: Route::ModM,
3568 proof: Vec::new(),
3569 conflicts: 0,
3570 }),
3571 }
3572 }
3573}
3574
3575pub fn mine_clauses(num_vars: usize, clauses: &[Vec<Lit>]) -> Vec<Vec<Lit>> {
3581 let mut seen: HashSet<Vec<i64>> = clauses.iter().map(|c| canon(c)).collect();
3582 let mut pool = Vec::new();
3583 let mut add = |bundle: Vec<Vec<Lit>>, pool: &mut Vec<Vec<Lit>>, seen: &mut HashSet<Vec<i64>>| {
3584 for c in bundle {
3585 if seen.insert(canon(&c)) {
3586 pool.push(c);
3587 }
3588 }
3589 };
3590 add(xor_gaussian_bundle(num_vars, clauses), &mut pool, &mut seen);
3591 add(failed_literal_bundle(num_vars, clauses), &mut pool, &mut seen);
3592 pool
3593}
3594
3595fn canon(c: &[Lit]) -> Vec<i64> {
3597 let mut k: Vec<i64> = c
3598 .iter()
3599 .map(|l| if l.is_positive() { l.var() as i64 + 1 } else { -(l.var() as i64 + 1) })
3600 .collect();
3601 k.sort_unstable();
3602 k.dedup();
3603 k
3604}
3605
3606fn xor_width() -> usize {
3608 std::env::var("LOGOS_XOR_WIDTH").ok().and_then(|s| s.parse().ok()).unwrap_or(3)
3609}
3610
3611fn xor_gaussian_bundle(num_vars: usize, clauses: &[Vec<Lit>]) -> Vec<Vec<Lit>> {
3613 let eqs = extract_xor(num_vars, clauses);
3614 if eqs.len() < 2 {
3615 return Vec::new();
3616 }
3617 IncXor::new(num_vars, &eqs).derived_clauses(xor_width())
3618}
3619
3620fn failed_literal_bundle(num_vars: usize, clauses: &[Vec<Lit>]) -> Vec<Vec<Lit>> {
3624 if num_vars > 5000 || clauses.len() > 50_000 {
3625 return Vec::new();
3626 }
3627 let mut out = Vec::new();
3628 for v in 0..num_vars {
3629 let neg = Lit::new(v as u32, false);
3630 let pos = Lit::new(v as u32, true);
3631 if crate::rup::is_rup(num_vars, clauses, std::slice::from_ref(&neg)) {
3632 out.push(vec![neg]);
3633 } else if crate::rup::is_rup(num_vars, clauses, std::slice::from_ref(&pos)) {
3634 out.push(vec![pos]);
3635 }
3636 }
3637 out
3638}
3639
3640fn as_two_sat(clauses: &[Vec<Lit>]) -> Option<Vec<(crate::twosat::Lit, crate::twosat::Lit)>> {
3642 let cvt = |l: &Lit| {
3643 if l.is_positive() {
3644 crate::twosat::Lit::pos(l.var() as usize)
3645 } else {
3646 crate::twosat::Lit::neg(l.var() as usize)
3647 }
3648 };
3649 let mut out = Vec::with_capacity(clauses.len());
3650 for c in clauses {
3651 match c.as_slice() {
3652 [a] => out.push((cvt(a), cvt(a))),
3653 [a, b] => out.push((cvt(a), cvt(b))),
3654 _ => return None,
3655 }
3656 }
3657 Some(out)
3658}
3659
3660fn as_horn(clauses: &[Vec<Lit>]) -> Option<Vec<crate::hornsat::HornClause>> {
3662 let mut out = Vec::with_capacity(clauses.len());
3663 for c in clauses {
3664 if c.is_empty() {
3665 return None;
3666 }
3667 let pos: Vec<usize> = c.iter().filter(|l| l.is_positive()).map(|l| l.var() as usize).collect();
3668 let neg: Vec<usize> = c.iter().filter(|l| !l.is_positive()).map(|l| l.var() as usize).collect();
3669 match pos.len() {
3670 0 => out.push(crate::hornsat::HornClause::goal(neg)),
3671 1 if neg.is_empty() => out.push(crate::hornsat::HornClause::fact(pos[0])),
3672 1 => out.push(crate::hornsat::HornClause::rule(neg, pos[0])),
3673 _ => return None,
3674 }
3675 }
3676 Some(out)
3677}
3678
3679fn cnf_to_expr(clauses: &[Vec<Lit>]) -> Option<ProofExpr> {
3682 let atom = |l: &Lit| {
3683 let a = ProofExpr::Atom(format!("v{}", l.var()));
3684 if l.is_positive() { a } else { ProofExpr::Not(Box::new(a)) }
3685 };
3686 let mut clause_exprs = Vec::with_capacity(clauses.len());
3687 for c in clauses {
3688 if c.is_empty() {
3689 return None;
3690 }
3691 let atoms: Vec<ProofExpr> = c.iter().map(&atom).collect();
3692 clause_exprs.push(balanced(atoms, &|a, b| ProofExpr::Or(Box::new(a), Box::new(b)))?);
3693 }
3694 balanced(clause_exprs, &|a, b| ProofExpr::And(Box::new(a), Box::new(b)))
3697}
3698
3699fn balanced(mut items: Vec<ProofExpr>, combine: &dyn Fn(ProofExpr, ProofExpr) -> ProofExpr) -> Option<ProofExpr> {
3701 if items.is_empty() {
3702 return None;
3703 }
3704 while items.len() > 1 {
3705 let mut next = Vec::with_capacity(items.len().div_ceil(2));
3706 let mut it = items.into_iter();
3707 while let Some(a) = it.next() {
3708 match it.next() {
3709 Some(b) => next.push(combine(a, b)),
3710 None => next.push(a),
3711 }
3712 }
3713 items = next;
3714 }
3715 items.into_iter().next()
3716}
3717
3718fn hybrid_xor(num_vars: usize, clauses: &[Vec<Lit>]) -> Option<Solved> {
3732 if num_vars == 0 {
3733 return None;
3734 }
3735 let eqs = extract_xor(num_vars, clauses);
3736 let mut xor_vars = HashSet::new();
3737 for e in &eqs {
3738 xor_vars.extend(e.vars.iter().copied());
3739 }
3740 if eqs.len() < 2 || xor_vars.len() * 2 < num_vars {
3742 return None;
3743 }
3744 let engine = IncXor::new(num_vars, &eqs);
3745 if !engine.is_active() {
3746 return None;
3747 }
3748 let witness = match crate::xorsat::solve(&eqs, num_vars) {
3750 XorOutcome::Unsat(_) => return Some(Solved::unsat(Route::HybridXor)),
3751 XorOutcome::Sat(w) => w,
3752 };
3753 let derived = engine.derived_clauses(xor_width());
3757 let mut solver = Solver::new(num_vars);
3758 for c in clauses {
3759 solver.add_clause(c.clone());
3760 }
3761 for c in derived {
3762 solver.add_clause(c);
3763 }
3764 if xor_seed() {
3765 solver.set_initial_phase(&witness);
3766 }
3767 let result = if xor_live() {
3768 let live = IncXor::new(num_vars, &eqs);
3773 if xor_kernel() {
3774 let decisions = live.decision_vars();
3775 solver.set_decision_vars(&decisions);
3776 }
3777 let mut theories: Vec<Box<dyn crate::cdcl::Theory>> = vec![Box::new(live)];
3778 solver.solve_with(&mut theories)
3779 } else {
3780 solver.solve()
3781 };
3782 match result {
3783 SolveResult::Sat(model) => Some(Solved {
3784 answer: Answer::Sat(model),
3785 via: Route::HybridXor,
3786 proof: Vec::new(),
3787 conflicts: solver.conflicts(),
3788 }),
3789 SolveResult::Unsat => {
3790 let proof = solver.learned().iter().map(|lc| ProofStep::Rup(lc.lits.clone())).collect();
3791 Some(Solved { answer: Answer::Unsat, via: Route::HybridXor, proof, conflicts: solver.conflicts() })
3792 }
3793 }
3794}
3795
3796fn fused_modular_solve(num_vars: usize, clauses: &[Vec<Lit>]) -> Option<Solved> {
3806 if num_vars == 0 {
3807 return None;
3808 }
3809 let eqs = extract_xor(num_vars, clauses);
3810 let amo = crate::lyapunov::recover_cardinality_substructure(num_vars, clauses);
3811 if eqs.is_empty() || amo.is_empty() {
3812 return None;
3813 }
3814 let mut solver = Solver::new(num_vars);
3821 for c in clauses {
3822 solver.add_clause(c.clone());
3823 }
3824 let mut theories: Vec<Box<dyn crate::cdcl::Theory>> = vec![
3825 Box::new(crate::xor_engine::XorEngine::new(num_vars, &eqs)),
3826 Box::new(crate::pseudo_boolean::CardinalityTheory::new(num_vars, &amo)),
3827 Box::new(crate::lyapunov::SymmetryTheory::new(num_vars, crate::lyapunov::fused_symmetry_group(num_vars, clauses))),
3828 ];
3829 match solver.solve_with(&mut theories) {
3830 SolveResult::Sat(model) => {
3831 clauses
3832 .iter()
3833 .all(|c| c.iter().any(|l| model[l.var() as usize] == l.is_positive()))
3834 .then_some(Solved {
3835 answer: Answer::Sat(model),
3836 via: Route::HybridXor,
3837 proof: Vec::new(),
3838 conflicts: solver.conflicts(),
3839 })
3840 }
3841 SolveResult::Unsat => {
3842 Some(Solved { answer: Answer::Unsat, via: Route::HybridXor, proof: Vec::new(), conflicts: solver.conflicts() })
3843 }
3844 }
3845}
3846
3847fn xor_live() -> bool {
3850 std::env::var("LOGOS_XOR_LIVE").map(|s| s != "0" && !s.is_empty()).unwrap_or(false)
3851}
3852
3853fn xor_kernel() -> bool {
3856 std::env::var("LOGOS_XOR_KERNEL").map(|s| s != "0" && !s.is_empty()).unwrap_or(true)
3857}
3858
3859fn xor_seed() -> bool {
3861 std::env::var("LOGOS_XOR_SEED").map(|s| s != "0" && !s.is_empty()).unwrap_or(true)
3862}
3863
3864#[cfg(test)]
3865mod tests {
3866 use super::*;
3867 use crate::families::{clique_coloring, php, tseitin_expander};
3868 use crate::rup::check_refutation;
3869
3870 #[test]
3871 fn pigeonhole_is_crushed_by_a_specialist_not_cdcl() {
3872 let (cnf, _) = php(20);
3875 let solved = solve_structured(cnf.num_vars, &cnf.clauses);
3876 assert!(matches!(solved.answer, Answer::Unsat));
3877 assert_ne!(solved.via, Route::Cdcl, "PHP must be crushed structurally, got CDCL");
3878 }
3879
3880 #[test]
3881 fn massive_pigeonhole_does_not_fall_to_search() {
3882 let (cnf, _) = php(50);
3885 let solved = solve_structured(cnf.num_vars, &cnf.clauses);
3886 assert!(matches!(solved.answer, Answer::Unsat));
3887 assert_ne!(solved.via, Route::Cdcl);
3888 }
3889
3890 #[test]
3891 fn clique_colouring_is_crushed_structurally() {
3892 let (cnf, _) = clique_coloring(8, 7);
3893 let solved = solve_structured(cnf.num_vars, &cnf.clauses);
3894 assert!(matches!(solved.answer, Answer::Unsat));
3895 assert_ne!(solved.via, Route::Cdcl, "clique-colouring must be crushed structurally");
3896 }
3897
3898 #[test]
3899 fn sparse_sat_is_certified_by_lll_not_search() {
3900 let cl = |vs: [u32; 4]| vs.iter().map(|&v| Lit::pos(v)).collect::<Vec<_>>();
3904 let clauses = vec![cl([0, 1, 2, 3]), cl([4, 5, 6, 7]), cl([8, 9, 10, 11]), cl([12, 13, 14, 15])];
3905 let solved = solve_structured(16, &clauses);
3906 assert_eq!(solved.via, Route::Lll, "a locally-sparse SAT formula must route to LLL");
3907 match &solved.answer {
3908 Answer::Sat(model) => assert!(
3909 clauses.iter().all(|c| c.iter().any(|l| model[l.var() as usize] == l.is_positive())),
3910 "the LLL/Moser–Tardos witness must satisfy every clause"
3911 ),
3912 Answer::Unsat => panic!("a satisfiable sparse formula must not be reported UNSAT"),
3913 }
3914 }
3915
3916 #[test]
3917 fn tseitin_parity_is_crushed_structurally() {
3918 let (_, cnf, _) = tseitin_expander(40, 7);
3919 let solved = solve_structured(cnf.num_vars, &cnf.clauses);
3920 assert!(matches!(solved.answer, Answer::Unsat));
3921 assert!(
3922 matches!(solved.via, Route::Parity | Route::Collapse),
3923 "Tseitin parity must go through the GF(2) route, got {:?}",
3924 solved.via
3925 );
3926 }
3927
3928 #[test]
3929 fn two_sat_is_decided_with_a_model() {
3930 let clauses = vec![
3932 vec![Lit::new(0, true), Lit::new(1, true)],
3933 vec![Lit::new(0, false), Lit::new(1, true)],
3934 vec![Lit::new(0, true), Lit::new(1, false)],
3935 ];
3936 let solved = solve_structured(2, &clauses);
3937 assert_eq!(solved.via, Route::TwoSat);
3938 match solved.answer {
3939 Answer::Sat(m) => {
3940 for c in &clauses {
3941 assert!(c.iter().any(|l| m[l.var() as usize] == l.is_positive()));
3942 }
3943 }
3944 Answer::Unsat => panic!("instance is SAT"),
3945 }
3946 }
3947
3948 #[test]
3949 fn horn_is_decided_with_its_least_model() {
3950 let clauses = vec![
3953 vec![Lit::new(0, true)],
3954 vec![Lit::new(1, true)],
3955 vec![Lit::new(0, false), Lit::new(1, false), Lit::new(2, true)],
3956 ];
3957 let solved = solve_structured(3, &clauses);
3958 assert_eq!(solved.via, Route::Horn);
3959 match solved.answer {
3960 Answer::Sat(m) => assert!(m[0] && m[1] && m[2]),
3961 Answer::Unsat => panic!("instance is SAT"),
3962 }
3963 }
3964
3965 #[test]
3966 fn unstructured_sat_returns_a_model_via_cdcl() {
3967 let clauses = vec![
3969 vec![Lit::new(0, true), Lit::new(1, true), Lit::new(2, true)],
3970 vec![Lit::new(0, false), Lit::new(1, true), Lit::new(2, false)],
3971 ];
3972 let solved = solve_structured(3, &clauses);
3973 match solved.answer {
3974 Answer::Sat(m) => {
3975 for c in &clauses {
3976 assert!(c.iter().any(|l| m[l.var() as usize] == l.is_positive()));
3977 }
3978 }
3979 Answer::Unsat => panic!("instance is SAT"),
3980 }
3981 }
3982
3983 #[test]
3984 fn cdcl_route_carries_a_valid_rup_certificate() {
3985 let clauses = vec![
3988 vec![Lit::new(0, true), Lit::new(1, true), Lit::new(2, true)],
3989 vec![Lit::new(0, true), Lit::new(1, true), Lit::new(2, false)],
3990 vec![Lit::new(0, false), Lit::new(1, false), Lit::new(2, true)],
3991 vec![Lit::new(0, false), Lit::new(1, false), Lit::new(2, false)],
3992 vec![Lit::new(0, true), Lit::new(1, false), Lit::new(2, true)],
3993 vec![Lit::new(0, false), Lit::new(1, true), Lit::new(2, false)],
3994 vec![Lit::new(0, true), Lit::new(1, false), Lit::new(2, false)],
3995 vec![Lit::new(0, false), Lit::new(1, true), Lit::new(2, true)],
3996 ];
3997 let solved = solve_structured(3, &clauses);
3998 assert!(matches!(solved.answer, Answer::Unsat));
3999 if solved.via == Route::Cdcl {
4000 let learned: Vec<Vec<Lit>> = solved.proof.iter().map(|s| s.clause().to_vec()).collect();
4001 assert!(check_refutation(3, &clauses, &learned));
4002 }
4003 }
4004
4005 fn xor_gadget(vars: &[u32], rhs: bool) -> Vec<Vec<Lit>> {
4007 let k = vars.len();
4008 let mut clauses = Vec::new();
4009 for mask in 0u32..(1 << k) {
4010 if ((mask.count_ones() % 2) == 1) != rhs {
4011 clauses.push((0..k).map(|i| Lit::new(vars[i], (mask >> i) & 1 == 0)).collect());
4012 }
4013 }
4014 clauses
4015 }
4016
4017 #[test]
4018 fn hybrid_xor_solves_an_xor_heavy_sat_instance_with_a_valid_model() {
4019 let mut clauses = xor_gadget(&[0, 1, 2], false);
4022 clauses.extend(xor_gadget(&[2, 3], true));
4023 clauses.push(vec![Lit::new(0, true)]);
4024 clauses.push(vec![Lit::new(1, true), Lit::new(3, true)]);
4025 let solved = solve_structured(4, &clauses);
4026 assert_eq!(solved.via, Route::HybridXor, "XOR-heavy SAT must take the hybrid route");
4027 match solved.answer {
4028 Answer::Sat(m) => {
4029 for c in &clauses {
4030 assert!(c.iter().any(|l| m[l.var() as usize] == l.is_positive()), "model fails {c:?}");
4031 }
4032 }
4033 Answer::Unsat => panic!("instance is SAT"),
4034 }
4035 }
4036
4037 #[test]
4038 fn fused_route_decides_a_mixed_parity_cardinality_instance() {
4039 let mut clauses: Vec<Vec<Lit>> = vec![
4044 vec![Lit::new(0, true), Lit::new(1, true), Lit::new(2, true)],
4045 vec![Lit::new(0, false), Lit::new(1, false)],
4046 vec![Lit::new(0, false), Lit::new(2, false)],
4047 vec![Lit::new(1, false), Lit::new(2, false)],
4048 ];
4049 for i in 0..3u32 {
4050 clauses.extend(xor_gadget(&[i, i + 3], false)); }
4052 clauses.extend(xor_gadget(&[3, 4, 5], false)); let solved = solve_comprehensive(6, &clauses);
4054 assert!(matches!(solved.answer, Answer::Unsat), "the mixed instance is UNSAT (via {:?})", solved.via);
4055 assert_eq!(solved.via, Route::HybridXor, "the fused parity+cardinality route must fire");
4056 }
4057
4058 #[test]
4059 fn xor_inconsistent_system_is_refuted_structurally() {
4060 let mut clauses = xor_gadget(&[0, 1], false);
4062 clauses.extend(xor_gadget(&[1, 2], false));
4063 clauses.extend(xor_gadget(&[0, 2], true));
4064 let solved = solve_structured(3, &clauses);
4065 assert!(matches!(solved.answer, Answer::Unsat));
4066 assert_ne!(solved.via, Route::Cdcl, "a contradictory linear system must collapse structurally");
4067 }
4068
4069 #[test]
4070 fn mod_p_tseitin_cnf_is_lifted_to_gf_p_not_left_to_cdcl() {
4071 for &p in &[3u64, 5] {
4076 let (_, cnf, _) = crate::families::mod_p_tseitin_expander(6, p, 0xC0FFEE);
4077 let solved = solve_structured(cnf.num_vars, &cnf.clauses);
4078 assert!(matches!(solved.answer, Answer::Unsat), "mod-{p} Tseitin is UNSAT");
4079 assert_eq!(solved.via, Route::ModP, "mod-{p} CNF must be lifted to the GF(p) route");
4080 assert_eq!(solved.conflicts, 0, "the GF(p) collapse spends no search");
4081 }
4082 }
4083
4084 #[test]
4085 fn the_gf_p_route_returns_a_verified_model_on_a_satisfiable_mod_p_cnf() {
4086 let p = 3u64;
4089 let (_, cnf, _) = crate::families::mod_p_consistent_onehot(6, p, 0xABCD);
4090 let solved = solve_structured(cnf.num_vars, &cnf.clauses);
4091 assert_eq!(solved.via, Route::ModP, "a consistent mod-p one-hot CNF must take the GF(p) route");
4092 match &solved.answer {
4093 Answer::Sat(m) => assert!(
4094 cnf.clauses.iter().all(|c| c.iter().any(|l| m[l.var() as usize] == l.is_positive())),
4095 "the GF(p) model must satisfy every clause"
4096 ),
4097 Answer::Unsat => panic!("a consistent mod-p system must be SAT"),
4098 }
4099 }
4100
4101 #[test]
4102 fn the_gf_p_route_never_misfires_on_unstructured_or_non_linear_cnf() {
4103 let rnd = crate::families::random_3sat(30, 120, 0x5EED);
4107 let rnd_via = solve_structured(rnd.num_vars, &rnd.clauses).via;
4108 assert_ne!(rnd_via, Route::ModP);
4109 assert_ne!(rnd_via, Route::ModM, "random must not be misrouted to the composite lift either");
4110 let (php_cnf, _) = php(6);
4111 let php_via = solve_structured(php_cnf.num_vars, &php_cnf.clauses).via;
4112 assert_ne!(php_via, Route::ModP);
4113 assert_ne!(php_via, Route::ModM);
4114 }
4115
4116 #[test]
4117 fn the_gf_p_route_agrees_with_boolean_brute_force_on_tiny_instances() {
4118 for (cnf, want_sat) in [
4122 (crate::families::mod_p_tseitin_expander(4, 3, 1).1, false),
4123 (crate::families::mod_p_consistent_onehot(4, 3, 1).1, true),
4124 ] {
4125 let solved = solve_structured(cnf.num_vars, &cnf.clauses);
4126 assert_eq!(solved.via, Route::ModP, "a tiny mod-3 instance must take the GF(p) route");
4127 let brute = (0u64..(1u64 << cnf.num_vars)).any(|code| {
4128 let asg: Vec<bool> = (0..cnf.num_vars).map(|i| (code >> i) & 1 == 1).collect();
4129 cnf.clauses.iter().all(|c| c.iter().any(|l| asg[l.var() as usize] == l.is_positive()))
4130 });
4131 assert_eq!(matches!(solved.answer, Answer::Sat(_)), brute, "GF(p) verdict must match brute force");
4132 assert_eq!(brute, want_sat, "family verdict sanity");
4133 }
4134 }
4135
4136 #[test]
4137 fn composite_modulus_onehot_cnf_is_lifted_to_zmod_m_not_left_to_cdcl() {
4138 let (_, cnf, _) = crate::families::mod_p_tseitin_expander(6, 6, 0xC0FFEE);
4142 let solved = solve_structured(cnf.num_vars, &cnf.clauses);
4143 assert!(matches!(solved.answer, Answer::Unsat), "mod-6 Tseitin is UNSAT");
4144 assert_eq!(solved.via, Route::ModM, "a composite mod-6 CNF must be lifted to the ℤ/m route");
4145 assert_eq!(solved.conflicts, 0, "the ℤ/m collapse spends no search");
4146 }
4147
4148 #[test]
4149 fn the_zmod_m_route_returns_a_verified_model_on_a_satisfiable_composite_cnf() {
4150 let (_, cnf, _) = crate::families::mod_p_consistent_onehot(6, 6, 0xABCD);
4151 let solved = solve_structured(cnf.num_vars, &cnf.clauses);
4152 assert_eq!(solved.via, Route::ModM, "a consistent composite one-hot CNF must take the ℤ/m route");
4153 match &solved.answer {
4154 Answer::Sat(m) => assert!(
4155 cnf.clauses.iter().all(|c| c.iter().any(|l| m[l.var() as usize] == l.is_positive())),
4156 "the ℤ/m model must satisfy every clause"
4157 ),
4158 Answer::Unsat => panic!("a consistent composite system must be SAT"),
4159 }
4160 }
4161
4162 #[test]
4163 fn the_sos_route_is_sound_in_the_dispatcher() {
4164 fn sm(s: &mut u64) -> u64 {
4169 *s = s.wrapping_add(0x9E37_79B9_7F4A_7C15);
4170 let mut z = *s;
4171 z = (z ^ (z >> 30)).wrapping_mul(0xBF58_476D_1CE4_E5B9);
4172 z ^ (z >> 31)
4173 }
4174 fn brute_sat(nv: usize, cl: &[Vec<Lit>]) -> bool {
4175 (0u64..(1u64 << nv))
4176 .any(|x| cl.iter().all(|c| c.iter().any(|l| ((x >> l.var()) & 1 != 0) == l.is_positive())))
4177 }
4178 let mut state = 0x5005_7777u64;
4179 for _ in 0..120 {
4180 let nv = 4usize;
4181 let m = 6 + (sm(&mut state) % 8) as usize;
4182 let mut cl: Vec<Vec<Lit>> = Vec::new();
4183 for _ in 0..m {
4184 let mut vs: Vec<u32> = Vec::new();
4185 while vs.len() < 3 {
4186 let v = (sm(&mut state) % nv as u64) as u32;
4187 if !vs.contains(&v) {
4188 vs.push(v);
4189 }
4190 }
4191 cl.push(vs.iter().map(|&v| Lit::new(v, sm(&mut state) % 2 == 0)).collect());
4192 }
4193 let solved = solve_structured(nv, &cl);
4194 let sat = brute_sat(nv, &cl);
4195 if solved.via == Route::Sos {
4196 assert!(matches!(solved.answer, Answer::Unsat), "the SoS route only ever refutes");
4197 assert!(!sat, "the SoS route must never fire on a satisfiable instance: {cl:?}");
4198 }
4199 if sat {
4200 assert_ne!(solved.via, Route::Sos, "a satisfiable instance must not be routed to SoS");
4201 }
4202 }
4203 }
4204
4205 #[test]
4206 fn solve_comprehensive_matches_brute_force() {
4207 fn sm(s: &mut u64) -> u64 {
4211 *s = s.wrapping_add(0x9E37_79B9_7F4A_7C15);
4212 let mut z = *s;
4213 z = (z ^ (z >> 30)).wrapping_mul(0xBF58_476D_1CE4_E5B9);
4214 z ^ (z >> 31)
4215 }
4216 fn brute_sat(nv: usize, cl: &[Vec<Lit>]) -> bool {
4217 (0u64..(1u64 << nv))
4218 .any(|x| cl.iter().all(|c| c.iter().any(|l| ((x >> l.var()) & 1 != 0) == l.is_positive())))
4219 }
4220 let mut state = 0xC0DE_5A1Du64;
4221 for _ in 0..80 {
4222 let nv = 3 + (sm(&mut state) % 3) as usize; let m = 2 + (sm(&mut state) % 10) as usize;
4224 let mut cl: Vec<Vec<Lit>> = Vec::new();
4225 for _ in 0..m {
4226 let mut c = Vec::new();
4227 for v in 0..nv {
4228 if sm(&mut state) % 2 == 0 {
4229 c.push(Lit::new(v as u32, sm(&mut state) % 2 == 0));
4230 }
4231 }
4232 if !c.is_empty() {
4233 cl.push(c);
4234 }
4235 }
4236 if cl.is_empty() {
4237 continue;
4238 }
4239 let solved = solve_comprehensive(nv, &cl);
4240 assert_eq!(
4241 matches!(solved.answer, Answer::Sat(_)),
4242 brute_sat(nv, &cl),
4243 "solve_comprehensive verdict must match brute force via {:?}: {cl:?}",
4244 solved.via
4245 );
4246 if let Answer::Sat(m) = &solved.answer {
4247 assert!(
4248 cl.iter().all(|c| c.iter().any(|l| m[l.var() as usize] == l.is_positive())),
4249 "a reported model must satisfy every clause: {cl:?}"
4250 );
4251 }
4252 }
4253 }
4254
4255 #[test]
4256 fn the_symmetry_break_route_solves_a_symmetric_instance() {
4257 let (cnf, _) = crate::families::clique_coloring(3, 3);
4261 let s = symmetry_break_solve(cnf.num_vars, &cnf.clauses)
4262 .expect("clique colouring has a usable, phase-free symmetry group");
4263 assert_eq!(s.via, Route::SymmetryBreak);
4264 match s.answer {
4265 Answer::Sat(m) => assert!(
4266 cnf.clauses.iter().all(|c| c.iter().any(|l| m[l.var() as usize] == l.is_positive())),
4267 "the symmetry-break route returns a valid model"
4268 ),
4269 Answer::Unsat => panic!("clique_coloring(3,3) is SAT"),
4270 }
4271 }
4272
4273 #[test]
4274 fn dynamic_sel_refutes_a_symmetric_instance_in_search() {
4275 let (cnf, _) = crate::families::php(5);
4280 let solved =
4281 dynamic_sel(cnf.num_vars, &cnf.clauses).expect("PHP is symmetric — dynamic SEL engages");
4282 assert_eq!(solved.via, Route::Sel);
4283 assert!(matches!(solved.answer, Answer::Unsat), "PHP(5) is UNSAT");
4284 assert!(!solved.proof.is_empty(), "SEL returns a refutation proof");
4285 }
4286
4287 #[test]
4288 fn orbital_branch_collapses_symmetric_branches_and_is_correct() {
4289 let (sat_cnf, _) = crate::families::clique_coloring(3, 3);
4293 let s = orbital_branch_solve(sat_cnf.num_vars, &sat_cnf.clauses)
4294 .expect("a large variable orbit drives orbital branching");
4295 assert_eq!(s.via, Route::OrbitalBranch);
4296 match &s.answer {
4297 Answer::Sat(m) => assert!(
4298 sat_cnf.clauses.iter().all(|c| c.iter().any(|l| m[l.var() as usize] == l.is_positive())),
4299 "orbital branching returns a valid model"
4300 ),
4301 Answer::Unsat => panic!("clique_coloring(3,3) is SAT"),
4302 }
4303
4304 let (unsat_cnf, _) = crate::families::clique_coloring(4, 3);
4307 let u = orbital_branch_solve(unsat_cnf.num_vars, &unsat_cnf.clauses)
4308 .expect("a large variable orbit drives orbital branching");
4309 assert_eq!(u.via, Route::OrbitalBranch);
4310 assert!(matches!(u.answer, Answer::Unsat), "clique_coloring(4,3) is UNSAT");
4311
4312 let (big_cnf, _) = crate::families::clique_coloring(4, 4);
4316 let big = orbital_branch_solve(big_cnf.num_vars, &big_cnf.clauses)
4317 .expect("recursive orbital branching engages on the larger grid");
4318 assert_eq!(big.via, Route::OrbitalBranch);
4319 match &big.answer {
4320 Answer::Sat(m) => assert!(
4321 big_cnf.clauses.iter().all(|c| c.iter().any(|l| m[l.var() as usize] == l.is_positive())),
4322 "the recursive orbital model is valid"
4323 ),
4324 Answer::Unsat => panic!("clique_coloring(4,4) is SAT"),
4325 }
4326
4327 for (cnf, _) in [
4329 crate::families::clique_coloring(3, 3),
4330 crate::families::clique_coloring(4, 3),
4331 crate::families::clique_coloring(4, 4),
4332 ] {
4333 let nv = cnf.num_vars;
4334 let brute = (0u64..(1u64 << nv)).any(|x| {
4335 let a: Vec<bool> = (0..nv).map(|i| (x >> i) & 1 == 1).collect();
4336 cnf.clauses.iter().all(|c| c.iter().any(|l| a[l.var() as usize] == l.is_positive()))
4337 });
4338 let got = orbital_branch_solve(nv, &cnf.clauses).expect("orbital fires");
4339 assert_eq!(
4340 matches!(got.answer, Answer::Sat(_)),
4341 brute,
4342 "orbital-branch verdict matches brute force (nv={nv})"
4343 );
4344 }
4345 }
4346
4347 #[test]
4348 fn solve_by_symmetry_breaking_matches_brute_force() {
4349 let instances = [
4350 crate::families::clique_coloring(3, 3), crate::families::clique_coloring(4, 3), crate::families::clique_coloring(4, 4), ];
4354 for (cnf, _) in instances {
4355 let nv = cnf.num_vars;
4356 let brute = (0u64..(1u64 << nv)).any(|x| {
4357 let a: Vec<bool> = (0..nv).map(|i| (x >> i) & 1 == 1).collect();
4358 cnf.clauses.iter().all(|c| c.iter().any(|l| a[l.var() as usize] == l.is_positive()))
4359 });
4360 let solved = solve_by_symmetry_breaking(nv, &cnf.clauses);
4361 assert_eq!(matches!(solved.answer, Answer::Sat(_)), brute, "break-then-solve matches brute (nv={nv})");
4362 if let Answer::Sat(m) = &solved.answer {
4363 assert!(
4364 cnf.clauses.iter().all(|c| c.iter().any(|l| m[l.var() as usize] == l.is_positive())),
4365 "the projected model satisfies the original formula"
4366 );
4367 }
4368 }
4369 }
4370
4371 #[test]
4372 fn break_all_symmetry_complete_leaves_one_model_per_orbit() {
4373 let count_original = |total: usize, cl: &[Vec<Lit>], nv: usize| -> usize {
4376 let mut working = cl.to_vec();
4377 let mut count = 0;
4378 loop {
4379 match solve_comprehensive(total, &working).answer {
4380 Answer::Unsat => break,
4381 Answer::Sat(m) => {
4382 count += 1;
4383 working.push((0..nv).map(|v| Lit::new(v as u32, !m[v])).collect());
4384 }
4385 }
4386 }
4387 count
4388 };
4389 let n = |v| Lit::new(v, false);
4390
4391 let amo = vec![vec![n(0), n(1)], vec![n(0), n(2)], vec![n(1), n(2)]];
4393 let orbits_amo = models_up_to_symmetry(3, &amo, 1000).representatives.len();
4394 let (b1, t1) = break_all_symmetry_complete(3, &amo);
4395 assert_eq!(count_original(t1, &b1, 3), orbits_amo, "one model per orbit (at-most-1-of-3)");
4396
4397 let (cnf, _) = crate::families::clique_coloring(3, 3);
4399 let orbits_clq = models_up_to_symmetry(cnf.num_vars, &cnf.clauses, 1000).representatives.len();
4400 let (b2, t2) = break_all_symmetry_complete(cnf.num_vars, &cnf.clauses);
4401 assert_eq!(orbits_clq, 1, "clique(3,3)'s colourings form a single orbit");
4402 assert_eq!(count_original(t2, &b2, cnf.num_vars), 1, "complete breaking leaves exactly one model (clique)");
4403
4404 let asym = vec![vec![Lit::new(0, true)], vec![n(1), Lit::new(2, true)]];
4406 let (b3, t3) = break_all_symmetry_complete(3, &asym);
4407 assert_eq!((b3.len(), t3), (asym.len(), 3), "no symmetry ⇒ no breaks");
4408 }
4409
4410 #[test]
4411 fn break_all_symmetry_runs_to_a_fixpoint_soundly() {
4412 let (cnf, _) = crate::families::clique_coloring(3, 3);
4415 let before = symmetry_structure(cnf.num_vars, &cnf.clauses).order;
4416 let broken = break_all_symmetry(cnf.num_vars, &cnf.clauses);
4417 let after = symmetry_structure(cnf.num_vars, &broken).order;
4418 assert!(after < before, "the breaker reduced the symmetry group: {before} → {after}");
4419
4420 let orig = solve_comprehensive(cnf.num_vars, &cnf.clauses).answer;
4422 let brk = solve_comprehensive(cnf.num_vars, &broken).answer;
4423 assert_eq!(matches!(orig, Answer::Sat(_)), matches!(brk, Answer::Sat(_)), "breaking preserves the verdict");
4424 if let Answer::Sat(m) = &brk {
4425 assert!(
4426 cnf.clauses.iter().all(|c| c.iter().any(|l| m[l.var() as usize] == l.is_positive())),
4427 "the broken-formula model is a genuine model of the original"
4428 );
4429 }
4430
4431 let twice = break_all_symmetry(cnf.num_vars, &broken);
4433 assert_eq!(twice.len(), broken.len(), "already at the fixpoint — re-breaking is a no-op");
4434
4435 let asym = vec![vec![Lit::new(0, true)], vec![Lit::new(1, false), Lit::new(2, true)]];
4437 assert_eq!(break_all_symmetry(3, &asym).len(), asym.len(), "no symmetry ⇒ no breaks");
4438 }
4439
4440 #[test]
4441 fn class_algebra_constants_wrapper_has_the_right_shape() {
4442 let (cnf, _) = crate::families::clique_coloring(3, 3);
4443 let k = symmetry_structure(cnf.num_vars, &cnf.clauses).conjugacy_classes.unwrap(); let a = class_algebra_constants(cnf.num_vars, &cnf.clauses).expect("enumerable group");
4445 assert_eq!(a.len(), k, "the class-algebra tensor is k × k × k");
4446 assert!(a.iter().all(|m| m.len() == k && m.iter().all(|r| r.len() == k)));
4447 }
4448
4449 #[test]
4450 fn character_table_wrapper_is_the_grid_groups_table() {
4451 let (cnf, _) = crate::families::clique_coloring(3, 3);
4454 let t = character_table(cnf.num_vars, &cnf.clauses).expect("enumerable group");
4455 assert_eq!(t.degrees, vec![1, 1, 1, 1, 2, 2, 2, 2, 4], "S₃×S₃ irreducible degrees");
4456 assert_eq!(t.degrees.iter().map(|d| d * d).sum::<u128>(), 36, "Σ dᵢ² = |S₃×S₃|");
4457 assert_eq!(t.values.len(), t.degrees.len(), "one character per irreducible");
4458 assert!(t.values.iter().all(|row| row.len() == t.class_sizes.len()), "a value per conjugacy class");
4459 assert!(t.values.iter().any(|row| row.iter().all(|&x| x == 1)), "the trivial character is present");
4460 }
4461
4462 #[test]
4463 fn frobenius_schur_wrapper_reports_a_real_grid_group() {
4464 let (cnf, _) = crate::families::clique_coloring(3, 3);
4466 let fs = frobenius_schur_indicators(cnf.num_vars, &cnf.clauses).expect("enumerable group");
4467 assert_eq!(fs, vec![1; 9], "S₃×S₃: nine real irreducibles");
4468 }
4469
4470 #[test]
4471 fn isotypic_decomposition_wrapper_bridges_action_and_representation() {
4472 let (cnf, _) = crate::families::clique_coloring(3, 3);
4475 let iso = isotypic_multiplicities(cnf.num_vars, &cnf.clauses).expect("enumerable group");
4476 let degs = symmetry_structure(cnf.num_vars, &cnf.clauses).irreducible_degrees.unwrap();
4477 assert_eq!(iso.iter().zip(°s).map(|(m, d)| m * d).sum::<u128>(), 9, "Σ m·d = 9 cells");
4478 let pi = permutation_character(cnf.num_vars, &cnf.clauses).expect("enumerable group");
4480 assert!(pi.contains(&9), "the identity class fixes all 9 variables");
4481 }
4482
4483 #[test]
4484 fn automorphism_group_wrapper_measures_the_symmetry_of_the_symmetry() {
4485 let (cnf, _) = crate::families::clique_coloring(3, 3);
4487 assert_eq!(
4488 automorphism_group_order(cnf.num_vars, &cnf.clauses),
4489 Some(72),
4490 "|Aut(S₃×S₃)| = 72"
4491 );
4492 }
4493
4494 #[test]
4495 fn table_of_marks_wrapper_classifies_a_grid_groups_g_sets() {
4496 let (cnf, _) = crate::families::clique_coloring(3, 3);
4499 let (orders, marks) = table_of_marks(cnf.num_vars, &cnf.clauses).expect("subgroup lattice in range");
4500 let k = orders.len();
4501 assert_eq!(*orders.last().unwrap(), 36, "the whole group S₃×S₃ has order 36");
4502 assert_eq!(marks[0][0], 36, "m(1, 1) = [G:1] = |G| = 36 (the regular action)");
4503 for j in 0..k {
4504 assert_eq!(marks[0][j], 36 / orders[j], "m(1, H_j) = [G : H_j]");
4505 assert_eq!(marks[j][k - 1], 1, "every subgroup fixes the one coset of G");
4506 }
4507 }
4508
4509 #[test]
4510 fn galois_class_orbits_wrapper_partitions_a_rational_grid_group() {
4511 let (cnf, _) = crate::families::clique_coloring(3, 3);
4513 let orbits = galois_class_orbits(cnf.num_vars, &cnf.clauses).expect("enumerable group");
4514 assert_eq!(orbits.len(), 9, "S₃×S₃ has 9 conjugacy classes");
4515 assert!(orbits.iter().all(|o| o.len() == 1), "all rational ⇒ every orbit is a singleton");
4516 let prof = symmetry_structure(cnf.num_vars, &cnf.clauses);
4517 assert_eq!(prof.rational_classes, Some(9));
4518 }
4519
4520 #[test]
4521 fn tensor_decomposition_wrapper_is_a_valid_fusion_ring() {
4522 let (cnf, _) = crate::families::clique_coloring(3, 3);
4525 let degs = symmetry_structure(cnf.num_vars, &cnf.clauses).irreducible_degrees.unwrap();
4526 let n = tensor_decomposition(cnf.num_vars, &cnf.clauses).expect("enumerable group");
4527 let k = degs.len();
4528 assert_eq!(n.len(), k, "a k×k×k fusion tensor");
4529 for i in 0..k {
4530 for j in 0..k {
4531 assert_eq!(
4532 (0..k).map(|c| n[i][j][c] * degs[c]).sum::<u128>(),
4533 degs[i] * degs[j],
4534 "dim(χ_i ⊗ χ_j) = d_i·d_j"
4535 );
4536 }
4537 }
4538 }
4539
4540 #[test]
4541 fn equivalence_symmetry_matches_brute_force_and_reduces() {
4542 let p = |v: u32| Lit::new(v, true);
4543 let nl = |v: u32| Lit::new(v, false);
4544 let sat = |m: &[bool], cls: &[Vec<Lit>]| {
4545 cls.iter().all(|c| c.iter().any(|l| m[l.var() as usize] == l.is_positive()))
4546 };
4547 let brute_equiv = |nv: usize, f: &[Vec<Lit>], s: &[Vec<Lit>]| -> bool {
4548 (0u32..(1u32 << nv)).all(|x| {
4549 let a: Vec<bool> = (0..nv).map(|i| (x >> i) & 1 == 1).collect();
4550 sat(&a, f) == sat(&a, s)
4551 })
4552 };
4553
4554 let amo: Vec<Vec<Lit>> =
4557 (0..4u32).flat_map(|i| ((i + 1)..4).map(move |j| vec![nl(i), nl(j)])).collect();
4558 assert_eq!(amo.len(), 6);
4559 let gens = common_automorphism_generators(4, &amo, &amo);
4560 assert!(!gens.is_empty(), "at-most-one-of-4 has a nontrivial common symmetry group");
4561 let (reps, naive) = equivalence_check_counts(4, &amo, &amo);
4562 assert!(reps < naive, "the common symmetry must reduce the work: {reps} < {naive}");
4563 assert_eq!(equivalent_modulo_symmetry(4, &amo, &amo), EquivVerdict::Equivalent);
4564
4565 let f2 = vec![vec![p(0), p(1)], vec![nl(0), p(1)]];
4567 let mut s2 = f2.clone();
4568 s2.push(vec![p(1)]);
4569 assert!(brute_equiv(2, &f2, &s2), "sanity: the resolvent makes them equivalent");
4570 assert_eq!(equivalent_modulo_symmetry(2, &f2, &s2), EquivVerdict::Equivalent);
4571
4572 let f3 = vec![vec![p(0), p(1)], vec![nl(0), nl(1)]];
4574 let s3 = vec![vec![p(0), p(1)]];
4575 match equivalent_modulo_symmetry(2, &f3, &s3) {
4576 EquivVerdict::Differ(m) => assert_ne!(sat(&m, &f3), sat(&m, &s3), "witness must distinguish"),
4577 EquivVerdict::Equivalent => panic!("f3 and s3 are NOT equivalent"),
4578 }
4579
4580 let fa = vec![vec![p(0), p(1)]];
4582 let sa = vec![vec![p(0), p(1)], vec![p(1), p(2)]];
4583 let (r, t) = equivalence_check_counts(3, &fa, &sa);
4584 assert_eq!(r, t, "no common symmetry ⇒ one check per clause");
4585
4586 fn xs(s: &mut u64) -> u64 {
4588 *s ^= *s << 13;
4589 *s ^= *s >> 7;
4590 *s ^= *s << 17;
4591 *s
4592 }
4593 let nv = 4usize;
4594 let mk = |s: &mut u64| -> Vec<Vec<Lit>> {
4595 let m = (xs(s) % 5) as usize; (0..m)
4597 .map(|_| {
4598 let w = 1 + (xs(s) % 2) as usize; (0..w).map(|_| Lit::new((xs(s) % nv as u64) as u32, xs(s) & 1 == 0)).collect()
4600 })
4601 .collect()
4602 };
4603 let mut seed = 0x1234_5678_9abc_def0u64;
4604 for _ in 0..400 {
4605 let f = mk(&mut seed);
4606 let s = mk(&mut seed);
4607 let want = brute_equiv(nv, &f, &s);
4608 match equivalent_modulo_symmetry(nv, &f, &s) {
4609 EquivVerdict::Equivalent => {
4610 assert!(want, "claimed equivalent but brute says differ: F={f:?} S={s:?}")
4611 }
4612 EquivVerdict::Differ(m) => {
4613 assert!(!want, "claimed differ but brute says equivalent: F={f:?} S={s:?}");
4614 assert_ne!(sat(&m, &f), sat(&m, &s), "witness must distinguish F and S");
4615 }
4616 }
4617 }
4618 }
4619
4620 #[test]
4621 fn optimization_symmetry_matches_brute_force_and_reduces() {
4622 let p = |v: u32| Lit::new(v, true);
4623 let sat = |m: &[bool], cls: &[Vec<Lit>]| {
4624 cls.iter().all(|c| c.iter().any(|l| m[l.var() as usize] == l.is_positive()))
4625 };
4626 let brute_min = |nv: usize, f: &[Vec<Lit>], w: &[i64]| -> Option<i64> {
4627 (0u32..(1u32 << nv))
4628 .filter_map(|x| {
4629 let a: Vec<bool> = (0..nv).map(|i| (x >> i) & 1 == 1).collect();
4630 sat(&a, f).then(|| (0..nv).filter(|&i| a[i]).map(|i| w[i]).sum::<i64>())
4631 })
4632 .min()
4633 };
4634
4635 let amo1 = vec![vec![p(0), p(1), p(2), p(3)]];
4639 let w1 = vec![1i64; 4];
4640 let (opt, m) = optimize_modulo_symmetry(4, &amo1, &w1).expect("F is satisfiable");
4641 assert_eq!(opt, 1, "minimum is one variable true");
4642 assert!(sat(&m, &amo1), "witness satisfies F");
4643 assert_eq!(m.iter().filter(|&&b| b).count(), 1, "witness has weight 1");
4644 let (with, without) = optimize_enumeration_counts(4, &amo1, &w1);
4645 assert!(with < without, "symmetry must shrink the enumeration: {with} < {without}");
4646
4647 assert_eq!(optimize_modulo_symmetry(2, &[vec![p(0)], vec![Lit::new(0, false)]], &[1, 1]), None);
4649
4650 let w_distinct = vec![1i64, 2, 3, 4];
4653 assert!(optimization_symmetry_generators(4, &amo1, &w_distinct).is_empty(), "distinct weights ⇒ no sym");
4654 let (wa, wo) = optimize_enumeration_counts(4, &amo1, &w_distinct);
4655 assert_eq!(wa, wo, "no usable symmetry ⇒ no reduction");
4656
4657 fn xs(s: &mut u64) -> u64 {
4660 *s ^= *s << 13;
4661 *s ^= *s >> 7;
4662 *s ^= *s << 17;
4663 *s
4664 }
4665 let nv = 4usize;
4666 let mut seed = 0xC0FFEE_1234_5678u64;
4667 for _ in 0..400 {
4668 let m = (xs(&mut seed) % 5) as usize;
4669 let f: Vec<Vec<Lit>> = (0..m)
4670 .map(|_| {
4671 let wclause = 1 + (xs(&mut seed) % 2) as usize;
4672 (0..wclause).map(|_| Lit::new((xs(&mut seed) % nv as u64) as u32, xs(&mut seed) & 1 == 0)).collect()
4673 })
4674 .collect();
4675 let weights: Vec<i64> = (0..nv).map(|_| (xs(&mut seed) % 5) as i64 - 2).collect();
4677 let want = brute_min(nv, &f, &weights);
4678 match optimize_modulo_symmetry(nv, &f, &weights) {
4679 None => assert!(want.is_none(), "claimed UNSAT but a model exists: F={f:?}"),
4680 Some((opt, wit)) => {
4681 assert_eq!(Some(opt), want, "optimum must match brute force: F={f:?} w={weights:?}");
4682 assert!(sat(&wit, &f), "witness must satisfy F");
4683 let ww: i64 = (0..nv).filter(|&i| wit[i]).map(|i| weights[i]).sum();
4684 assert_eq!(ww, opt, "witness must achieve the optimum");
4685 }
4686 }
4687 }
4688 }
4689
4690 #[test]
4691 fn fractional_automorphism_is_a_doubly_stochastic_commuting_relaxation() {
4692 let edge = |a: u32, b: u32| vec![Lit::new(a, true), Lit::new(b, true)];
4693
4694 let (php, _) = crate::families::php(4);
4697 let (clq, _) = crate::families::clique_coloring(3, 3);
4698 let c6: Vec<Vec<Lit>> = (0..6).map(|i| edge(i, (i + 1) % 6)).collect();
4699 for (nv, cl) in [(php.num_vars, php.clauses.clone()), (clq.num_vars, clq.clauses.clone()), (6, c6.clone())] {
4700 let part = fractional_automorphism(nv, &cl);
4701 assert!(is_fractional_automorphism(nv, &cl, &part), "the equitable partition commutes with A");
4702 let cells = part.iter().copied().max().map_or(0, |m| m + 1);
4704 assert!(cells < nv, "a non-discrete partition ⇒ a genuine (non-permutation) fractional automorphism");
4705 let gens = crate::sym_break::variable_automorphism_generators(nv, &cl).unwrap_or_default();
4707 for orbit in crate::permgroup::orbits(nv, &gens) {
4708 assert!(orbit.iter().all(|&v| part[v] == part[orbit[0]]), "orbit ⊆ fractional-automorphism cell");
4709 }
4710 }
4711
4712 let (nv, _) = (clq.num_vars, ());
4714 assert!(is_fractional_automorphism(nv, &clq.clauses, &(0..nv).collect::<Vec<_>>()), "identity is a fractional automorphism");
4715
4716 let p4 = vec![edge(0, 1), edge(1, 2), edge(2, 3)];
4719 assert!(!is_fractional_automorphism(4, &p4, &[0, 0, 1, 1]), "a non-equitable partition is rejected");
4720 assert!(is_fractional_automorphism(4, &p4, &[0, 1, 1, 0]), "the reflection partition is equitable");
4721 assert_eq!(fractional_automorphism(4, &p4), vec![0, 1, 1, 0], "P₄'s coarsest equitable partition is the reflection");
4722
4723 fn xs(s: &mut u64) -> u64 {
4725 *s ^= *s << 13;
4726 *s ^= *s >> 7;
4727 *s ^= *s << 17;
4728 *s
4729 }
4730 let n = 5usize;
4731 let mut seed = 0x0FAC_0000_1234_9999u64;
4732 for _ in 0..200 {
4733 let m = (xs(&mut seed) % 6) as usize;
4734 let cl: Vec<Vec<Lit>> = (0..m)
4735 .map(|_| {
4736 let w = 1 + (xs(&mut seed) % 3) as usize;
4737 (0..w).map(|_| Lit::new((xs(&mut seed) % n as u64) as u32, xs(&mut seed) & 1 == 0)).collect()
4738 })
4739 .collect();
4740 let part = fractional_automorphism(n, &cl);
4741 assert!(is_fractional_automorphism(n, &cl, &part), "canonical partition must always commute: {cl:?}");
4742 }
4743 }
4744
4745 #[test]
4746 fn color_refinement_over_approximates_the_orbit_partition() {
4747 let p = |v: u32| Lit::new(v, true);
4748
4749 let (php, _) = crate::families::php(4);
4751 assert_eq!(color_refinement_cells(php.num_vars, &php.clauses), 1, "PHP(4) variables are all alike");
4752 let (clq, _) = crate::families::clique_coloring(3, 3);
4753 assert_eq!(color_refinement_cells(clq.num_vars, &clq.clauses), 1, "clique(3,3) variables are all alike");
4754
4755 let f = vec![vec![p(0)], vec![p(1), p(2)]]; let cells = color_refinement(3, &f);
4758 assert_ne!(cells[0], cells[1], "the unit variable is distinguished from the binary pair");
4759 assert_eq!(cells[1], cells[2], "x1 and x2 are interchangeable");
4760 assert_eq!(provably_asymmetric_variables(3, &f), vec![0], "x0 is provably fixed by every automorphism");
4761 for g in crate::sym_break::variable_automorphism_generators(3, &f).unwrap_or_default() {
4763 assert_eq!(g[0], 0, "an automorphism must fix the provably-asymmetric variable");
4764 }
4765
4766 let check = |nv: usize, cl: &[Vec<Lit>]| {
4769 let gens = crate::sym_break::variable_automorphism_generators(nv, cl).unwrap_or_default();
4770 let orbits = crate::permgroup::orbits(nv, &gens);
4771 let cells = color_refinement(nv, cl);
4772 for orbit in &orbits {
4773 let c0 = cells[orbit[0]];
4774 assert!(orbit.iter().all(|&v| cells[v] == c0), "orbit {orbit:?} must be monochromatic: {cells:?}");
4775 }
4776 assert!(
4777 color_refinement_cells(nv, cl) <= orbits.len(),
4778 "the equitable partition is coarser than the orbit partition"
4779 );
4780 };
4781 check(php.num_vars, &php.clauses);
4782 check(clq.num_vars, &clq.clauses);
4783 check(3, &f);
4784
4785 fn xs(s: &mut u64) -> u64 {
4786 *s ^= *s << 13;
4787 *s ^= *s >> 7;
4788 *s ^= *s << 17;
4789 *s
4790 }
4791 let nv = 5usize;
4792 let mut seed = 0xA5A5_1234_DEAD_BEEFu64;
4793 for _ in 0..200 {
4794 let m = (xs(&mut seed) % 6) as usize;
4795 let cl: Vec<Vec<Lit>> = (0..m)
4796 .map(|_| {
4797 let w = 1 + (xs(&mut seed) % 3) as usize;
4798 (0..w).map(|_| Lit::new((xs(&mut seed) % nv as u64) as u32, xs(&mut seed) & 1 == 0)).collect()
4799 })
4800 .collect();
4801 check(nv, &cl);
4802 }
4803 }
4804
4805 #[test]
4806 fn two_wl_over_approximates_orbitals_and_beats_one_wl() {
4807 let edge = |a: u32, b: u32| vec![Lit::new(a, true), Lit::new(b, true)]; let c6 = vec![edge(0, 1), edge(1, 2), edge(2, 3), edge(3, 4), edge(4, 5), edge(5, 0)];
4812 let two_tri = vec![edge(0, 1), edge(1, 2), edge(0, 2), edge(3, 4), edge(4, 5), edge(3, 5)];
4813 assert_eq!(color_refinement_cells(6, &c6), 1, "1-WL: C₆ is one cell");
4814 assert_eq!(color_refinement_cells(6, &two_tri), 1, "1-WL: 2·C₃ is one cell — same as C₆");
4815 assert_ne!(
4816 two_wl_fingerprint(6, &c6),
4817 two_wl_fingerprint(6, &two_tri),
4818 "2-WL SEPARATES C₆ from 2·C₃ where 1-WL cannot"
4819 );
4820
4821 let diag_refines_1wl = |nv: usize, cl: &[Vec<Lit>]| {
4823 let wl1 = color_refinement(nv, cl);
4824 let pc = two_wl_pair_colors(nv, cl);
4825 for a in 0..nv {
4826 for b in 0..nv {
4827 if pc[a][a] == pc[b][b] {
4828 assert_eq!(wl1[a], wl1[b], "2-WL diagonal must refine 1-WL");
4829 }
4830 }
4831 }
4832 };
4833 diag_refines_1wl(6, &c6);
4834 diag_refines_1wl(6, &two_tri);
4835
4836 let check = |nv: usize, cl: &[Vec<Lit>]| {
4839 let gens = crate::sym_break::variable_automorphism_generators(nv, cl).unwrap_or_default();
4840 let orbitals = crate::permgroup::orbitals(nv, &gens);
4841 let pc = two_wl_pair_colors(nv, cl);
4842 for orbital in &orbitals {
4843 let (i0, j0) = orbital[0];
4844 let c0 = pc[i0][j0];
4845 assert!(orbital.iter().all(|&(i, j)| pc[i][j] == c0), "orbital must be monochromatic");
4846 }
4847 assert!(two_wl_pair_cells(nv, cl) <= orbitals.len(), "pair-cells ≤ orbitals");
4848 };
4849 let (php, _) = crate::families::php(4);
4850 let (clq, _) = crate::families::clique_coloring(3, 3);
4851 check(php.num_vars, &php.clauses);
4852 check(clq.num_vars, &clq.clauses);
4853 check(6, &c6);
4854 check(6, &two_tri);
4855 assert_eq!(color_refinement_cells(clq.num_vars, &clq.clauses), 1);
4857 assert!(two_wl_pair_cells(clq.num_vars, &clq.clauses) >= 4, "2-WL sees the 4 orbitals of the grid");
4858
4859 fn xs(s: &mut u64) -> u64 {
4860 *s ^= *s << 13;
4861 *s ^= *s >> 7;
4862 *s ^= *s << 17;
4863 *s
4864 }
4865 let nv = 5usize;
4866 let mut seed = 0x2B0C_1A7E_55AA_F00Du64;
4867 for _ in 0..120 {
4868 let m = (xs(&mut seed) % 6) as usize;
4869 let cl: Vec<Vec<Lit>> = (0..m)
4870 .map(|_| {
4871 let w = 1 + (xs(&mut seed) % 3) as usize;
4872 (0..w).map(|_| Lit::new((xs(&mut seed) % nv as u64) as u32, xs(&mut seed) & 1 == 0)).collect()
4873 })
4874 .collect();
4875 check(nv, &cl);
4876 }
4877 }
4878
4879 #[test]
4880 fn association_scheme_multiplicities_are_the_eigenspace_dimensions() {
4881 let edge = |a: u32, b: u32| vec![Lit::new(a, true), Lit::new(b, true)];
4882 let (clq, _) = crate::families::clique_coloring(3, 3);
4883 let c6: Vec<Vec<Lit>> = (0..6).map(|i| edge(i, (i + 1) % 6)).collect();
4884
4885 assert_eq!(
4888 association_scheme_multiplicities(clq.num_vars, &clq.clauses),
4889 Some(vec![1, 2, 2, 4]),
4890 "clique(3,3): eigenspace dimensions = S₃×S₃ constituent degrees"
4891 );
4892
4893 for (nv, cl) in [(clq.num_vars, clq.clauses.clone()), (6, c6.clone())] {
4895 let m = association_scheme_multiplicities(nv, &cl).expect("commutative scheme has multiplicities");
4896 assert_eq!(m.iter().sum::<u128>(), nv as u128, "Σ multiplicities = number of vertices");
4897 assert!(m.iter().all(|&x| x >= 1), "each eigenspace is non-empty");
4898 assert_eq!(m[0], 1, "the smallest (trivial) eigenspace has dimension 1");
4899 assert_eq!(m.len(), coherent_rank(nv, &cl).unwrap(), "one multiplicity per eigenspace");
4901 }
4902 }
4903
4904 #[test]
4905 fn association_scheme_eigenmatrix_is_the_scheme_character_table() {
4906 let edge = |a: u32, b: u32| vec![Lit::new(a, true), Lit::new(b, true)];
4907 let (clq, _) = crate::families::clique_coloring(3, 3);
4908 let c6: Vec<Vec<Lit>> = (0..6).map(|i| edge(i, (i + 1) % 6)).collect();
4909
4910 assert_eq!(coherent_rank(clq.num_vars, &clq.clauses), Some(4), "clique(3,3): 4 relations");
4913
4914 for (nv, cl) in [(clq.num_vars, clq.clauses.clone()), (6, c6.clone())] {
4915 let d = coherent_rank(nv, &cl).unwrap();
4916 let (p, pm) = association_scheme_eigenmatrix(nv, &cl).expect("a commutative scheme has an eigenmatrix");
4917 assert_eq!(pm.len(), d, "P has one row per common eigenspace (d × d)");
4918 assert!(pm.iter().all(|r| r.len() == d));
4919
4920 let (_, a) = coherent_configuration_constants(nv, &cl).unwrap();
4923 for row in &pm {
4924 for i in 0..d {
4925 for j in 0..d {
4926 let lhs = row[i] as u128 * row[j] as u128 % p as u128;
4927 let rhs = (0..d)
4928 .map(|k| (a[i][j][k] % p as u128) * row[k] as u128 % p as u128)
4929 .sum::<u128>()
4930 % p as u128;
4931 assert_eq!(lhs, rhs, "row must be an algebra homomorphism");
4932 }
4933 }
4934 }
4935
4936 let valency: Vec<u128> = (0..d).map(|i| (0..d).map(|j| a[i][j][0]).sum()).collect();
4939 assert_eq!(valency.iter().sum::<u128>(), nv as u128, "Σ valencies = number of vertices");
4940 assert!(valency.contains(&1), "the diagonal relation has valency 1");
4941 assert!(
4942 pm.iter().any(|row| (0..d).all(|i| row[i] as u128 == valency[i] % p as u128)),
4943 "the valency vector is a row of P (the trivial eigenspace)"
4944 );
4945 }
4946 }
4947
4948 #[test]
4949 fn coherent_configuration_is_a_genuine_association_scheme() {
4950 let edge = |a: u32, b: u32| vec![Lit::new(a, true), Lit::new(b, true)];
4951
4952 let (php, _) = crate::families::php(4);
4956 let (clq, _) = crate::families::clique_coloring(3, 3);
4957 let c6 = vec![edge(0, 1), edge(1, 2), edge(2, 3), edge(3, 4), edge(4, 5), edge(5, 0)];
4958
4959 let check = |nv: usize, cl: &[Vec<Lit>]| {
4960 let (d, p) = coherent_configuration_constants(nv, cl).expect("2-WL is coherent");
4961 assert_eq!(d, two_wl_pair_cells(nv, cl), "rank = number of basis relations");
4962 for k in 0..d {
4964 let total: u128 = (0..d).flat_map(|i| (0..d).map(move |j| (i, j))).map(|(i, j)| p[i][j][k]).sum();
4965 assert_eq!(total, nv as u128, "Σ_ij p[i][j][k] counts all n intermediate points");
4966 }
4967 let pc = two_wl_pair_colors(nv, cl);
4969 let mut transpose = vec![usize::MAX; d];
4970 for i in 0..nv {
4971 for j in 0..nv {
4972 let (r, rt) = (pc[i][j], pc[j][i]);
4973 if transpose[r] == usize::MAX {
4974 transpose[r] = rt;
4975 } else {
4976 assert_eq!(transpose[r], rt, "R_r^T must be a single relation");
4977 }
4978 }
4979 }
4980 d
4981 };
4982 check(php.num_vars, &php.clauses);
4983 let dclq = check(clq.num_vars, &clq.clauses);
4984 check(6, &c6);
4985
4986 assert_eq!(dclq, 4, "the rook's graph scheme has 4 relations");
4990 let clq_gens = crate::sym_break::variable_automorphism_generators(clq.num_vars, &clq.clauses).unwrap();
4991 assert_eq!(dclq, crate::permgroup::orbitals(clq.num_vars, &clq_gens).len(), "Schurian: relations = orbitals");
4992
4993 let pc6 = two_wl_pair_colors(6, &c6);
4997 let (_d6, p6) = coherent_configuration_constants(6, &c6).unwrap();
4998 let adj = pc6[0][1];
4999 let dist2 = pc6[0][2];
5000 assert_ne!(adj, dist2, "2-WL separates adjacency from distance-2 in C₆");
5001 assert_eq!(p6[adj][adj][dist2], 1, "C₆: vertices at distance 2 share exactly one common neighbour");
5002
5003 fn xs(s: &mut u64) -> u64 {
5004 *s ^= *s << 13;
5005 *s ^= *s >> 7;
5006 *s ^= *s << 17;
5007 *s
5008 }
5009 let nv = 5usize;
5010 let mut seed = 0x0C0E_4E17_C0FF_EE00u64;
5011 for _ in 0..100 {
5012 let m = (xs(&mut seed) % 6) as usize;
5013 let cl: Vec<Vec<Lit>> = (0..m)
5014 .map(|_| {
5015 let w = 1 + (xs(&mut seed) % 3) as usize;
5016 (0..w).map(|_| Lit::new((xs(&mut seed) % nv as u64) as u32, xs(&mut seed) & 1 == 0)).collect()
5017 })
5018 .collect();
5019 assert!(coherent_configuration_constants(nv, &cl).is_some(), "2-WL must always be coherent");
5021 }
5022 }
5023
5024 #[test]
5025 fn three_wl_over_approximates_3_orbits_and_beats_two_wl() {
5026 let edge = |a: usize, b: usize| vec![Lit::new(a as u32, true), Lit::new(b as u32, true)];
5027
5028 let cayley = |conn: &[(i32, i32)]| -> Vec<Vec<Lit>> {
5030 let idx = |r: i32, c: i32| (((r.rem_euclid(4)) * 4 + c.rem_euclid(4)) as usize);
5031 let mut edges = std::collections::BTreeSet::new();
5032 for r in 0..4 {
5033 for c in 0..4 {
5034 for &(dr, dc) in conn {
5035 let (a, b) = (idx(r, c), idx(r + dr, c + dc));
5036 if a < b {
5037 edges.insert((a, b));
5038 }
5039 }
5040 }
5041 }
5042 edges.into_iter().map(|(a, b)| edge(a, b)).collect()
5043 };
5044 let rook = cayley(&[(1, 0), (2, 0), (3, 0), (0, 1), (0, 2), (0, 3)]);
5046 let shrikhande = cayley(&[(1, 0), (3, 0), (0, 1), (0, 3), (1, 1), (3, 3)]);
5048
5049 assert_eq!(
5052 two_wl_fingerprint(16, &rook),
5053 two_wl_fingerprint(16, &shrikhande),
5054 "2-WL cannot separate two SRG(16,6,2,2) graphs"
5055 );
5056 assert_ne!(
5057 three_wl_fingerprint(16, &rook),
5058 three_wl_fingerprint(16, &shrikhande),
5059 "3-WL SEPARATES the rook's graph from the Shrikhande graph"
5060 );
5061
5062 let check = |nv: usize, cl: &[Vec<Lit>]| {
5064 let gens = crate::sym_break::variable_automorphism_generators(nv, cl).unwrap_or_default();
5065 let tw = three_wl_colors(nv, cl);
5066 for orbit in crate::permgroup::orbits_on_tuples(nv, &gens, 3) {
5067 let t0 = &orbit[0];
5068 let c0 = tw[t0[0]][t0[1]][t0[2]];
5069 assert!(orbit.iter().all(|t| tw[t[0]][t[1]][t[2]] == c0), "3-orbit must be monochromatic");
5070 }
5071 };
5072 let (clq, _) = crate::families::clique_coloring(3, 3);
5073 let c6: Vec<Vec<Lit>> = (0..6).map(|i| edge(i, (i + 1) % 6)).collect();
5074 check(clq.num_vars, &clq.clauses);
5075 check(6, &c6);
5076
5077 fn xs(s: &mut u64) -> u64 {
5078 *s ^= *s << 13;
5079 *s ^= *s >> 7;
5080 *s ^= *s << 17;
5081 *s
5082 }
5083 let nv = 5usize;
5084 let mut seed = 0x33C0_FFEE_0033_0033u64;
5085 for _ in 0..60 {
5086 let m = (xs(&mut seed) % 6) as usize;
5087 let cl: Vec<Vec<Lit>> = (0..m)
5088 .map(|_| {
5089 let w = 1 + (xs(&mut seed) % 3) as usize;
5090 (0..w).map(|_| Lit::new((xs(&mut seed) % nv as u64) as u32, xs(&mut seed) & 1 == 0)).collect()
5091 })
5092 .collect();
5093 check(nv, &cl);
5094 }
5095 }
5096
5097 #[test]
5098 fn canonical_form_decides_formula_isomorphism() {
5099 let edge = |a: usize, b: usize| vec![Lit::new(a as u32, true), Lit::new(b as u32, true)];
5100 let relabel = |cl: &[Vec<Lit>], perm: &[usize]| -> Vec<Vec<Lit>> {
5101 cl.iter()
5102 .map(|c| c.iter().map(|l| Lit::new(perm[l.var() as usize] as u32, l.is_positive())).collect())
5103 .collect()
5104 };
5105
5106 let c6: Vec<Vec<Lit>> = (0..6).map(|i| edge(i, (i + 1) % 6)).collect();
5109 let perm = [3usize, 5, 0, 2, 4, 1];
5110 assert_eq!(
5111 canonical_form(6, &c6),
5112 canonical_form(6, &relabel(&c6, &perm)),
5113 "isomorphic formulas share a canonical form"
5114 );
5115 assert_eq!(formulas_isomorphic(6, &c6, &relabel(&c6, &perm)), Some(true));
5116
5117 let two_tri = vec![edge(0, 1), edge(1, 2), edge(0, 2), edge(3, 4), edge(4, 5), edge(3, 5)];
5119 assert_eq!(color_refinement_cells(6, &c6), color_refinement_cells(6, &two_tri), "1-WL cannot tell them apart");
5120 assert_eq!(formulas_isomorphic(6, &c6, &two_tri), Some(false), "but canonical form CAN");
5121 assert_ne!(canonical_form(6, &c6), canonical_form(6, &two_tri));
5122
5123 let path4 = vec![edge(0, 1), edge(1, 2), edge(2, 3)];
5125 let star4 = vec![edge(0, 1), edge(0, 2), edge(0, 3)];
5126 assert_eq!(formulas_isomorphic(4, &path4, &star4), Some(false));
5127
5128 fn xs(s: &mut u64) -> u64 {
5131 *s ^= *s << 13;
5132 *s ^= *s >> 7;
5133 *s ^= *s << 17;
5134 *s
5135 }
5136 let nv = 6usize;
5137 let mut seed = 0xCA90_F00D_1234_5678u64;
5138 for _ in 0..120 {
5139 let m = (xs(&mut seed) % 7) as usize;
5140 let f: Vec<Vec<Lit>> = (0..m)
5141 .map(|_| {
5142 let w = 1 + (xs(&mut seed) % 2) as usize;
5143 (0..w).map(|_| Lit::new((xs(&mut seed) % nv as u64) as u32, xs(&mut seed) & 1 == 0)).collect()
5144 })
5145 .collect();
5146 let mut perm: Vec<usize> = (0..nv).collect();
5148 for i in (1..nv).rev() {
5149 let j = (xs(&mut seed) % (i as u64 + 1)) as usize;
5150 perm.swap(i, j);
5151 }
5152 let fp = relabel(&f, &perm);
5153 assert_eq!(canonical_form(nv, &f), canonical_form(nv, &fp), "F ≅ π(F): F={f:?} perm={perm:?}");
5154 assert_eq!(formulas_isomorphic(nv, &f, &fp), Some(true));
5155 }
5156 }
5157
5158 #[test]
5159 fn weighted_model_count_is_exact_and_symmetry_accelerated() {
5160 let p = |v: u32| Lit::new(v, true);
5161 let nl = |v: u32| Lit::new(v, false);
5162 let sat = |m: &[bool], cls: &[Vec<Lit>]| {
5163 cls.iter().all(|c| c.iter().any(|l| m[l.var() as usize] == l.is_positive()))
5164 };
5165 let brute = |nv: usize, f: &[Vec<Lit>], w: &[(i64, i64)]| -> i128 {
5166 (0u32..(1u32 << nv))
5167 .filter_map(|x| {
5168 let a: Vec<bool> = (0..nv).map(|i| (x >> i) & 1 == 1).collect();
5169 sat(&a, f).then(|| (0..nv).map(|i| if a[i] { w[i].1 as i128 } else { w[i].0 as i128 }).product::<i128>())
5170 })
5171 .sum()
5172 };
5173
5174 let amo = vec![vec![p(0), p(1), p(2)]]; let ones = vec![(1i64, 1i64); 3];
5177 assert_eq!(weighted_model_count(3, &amo, &ones), 7, "unit weights ⇒ #models");
5178 assert_eq!(weighted_model_count(3, &amo, &ones), brute(3, &amo, &ones));
5179
5180 let (solves, models) = weighted_model_count_solve_counts(3, &amo);
5183 assert_eq!(models, 7, "7 models of at-least-one-of-3");
5184 assert!(solves < models, "symmetry must reduce the solves: {solves} < {models}");
5185
5186 let w_sym = vec![(2i64, 3i64); 3];
5188 assert_eq!(weighted_model_count(3, &amo, &w_sym), brute(3, &amo, &w_sym));
5189
5190 assert_eq!(weighted_model_count(2, &[vec![p(0)], vec![nl(0)]], &[(1, 1), (1, 1)]), 0);
5192
5193 fn xs(s: &mut u64) -> u64 {
5197 *s ^= *s << 13;
5198 *s ^= *s >> 7;
5199 *s ^= *s << 17;
5200 *s
5201 }
5202 let nv = 4usize;
5203 let mut seed = 0x5EED_4321_FACE_0001u64;
5204 for _ in 0..200 {
5205 let m = (xs(&mut seed) % 5) as usize;
5206 let f: Vec<Vec<Lit>> = (0..m)
5207 .map(|_| {
5208 let wd = 1 + (xs(&mut seed) % 2) as usize;
5209 (0..wd).map(|_| Lit::new((xs(&mut seed) % nv as u64) as u32, xs(&mut seed) & 1 == 0)).collect()
5210 })
5211 .collect();
5212 let w: Vec<(i64, i64)> = (0..nv).map(|_| ((xs(&mut seed) % 4) as i64, (xs(&mut seed) % 4) as i64)).collect();
5213 assert_eq!(weighted_model_count(nv, &f, &w), brute(nv, &f, &w), "F={f:?} w={w:?}");
5214 }
5215 }
5216
5217 #[test]
5218 fn assignment_weight_inventory_splits_orbits_by_weight() {
5219 let (cnf, _) = crate::families::clique_coloring(3, 3);
5220 let inv = assignment_weight_inventory(cnf.num_vars, &cnf.clauses).expect("enumerable group");
5221 assert_eq!(inv.len(), 10, "weights 0..=9");
5222 assert_eq!(inv.iter().sum::<u128>(), 36, "sums to the assignment-orbit count (36 binary 3×3 matrices)");
5223 assert_eq!(inv[0], 1, "one all-false assignment");
5224 assert_eq!(inv[1], 1, "all single-one matrices are row/column equivalent");
5225 assert_eq!(inv[9], 1, "one all-true assignment");
5226 assert_eq!(
5228 Some(inv.iter().sum::<u128>()),
5229 symmetry_structure(cnf.num_vars, &cnf.clauses).assignment_orbits,
5230 "the inventory sums to the profile's assignment_orbits"
5231 );
5232
5233 let asym = vec![vec![Lit::new(0, true)], vec![Lit::new(1, false), Lit::new(2, true)]];
5235 assert_eq!(assignment_weight_inventory(3, &asym), Some(vec![1, 3, 3, 1]), "no symmetry ⇒ C(3,w)");
5236 }
5237
5238 #[test]
5239 fn pb_coefficient_symmetry_profiles_through_the_same_ladder() {
5240 use crate::pseudo_boolean::PbConstraint;
5241 let c = PbConstraint::new_weighted(&[(0, 3, true), (1, 3, true), (2, 3, true), (3, 5, true)], 6);
5244 let prof = pb_symmetry_profile(4, &[c]);
5245 assert_eq!(prof.order, 6, "S₃ on the three weight-3 variables");
5246 assert_eq!(prof.num_orbits, 2, "two orbits: {{x0,x1,x2}} and the fixed point x3");
5247 assert!(!prof.abelian, "S₃ is non-abelian");
5248 assert_eq!(prof.solvable, Some(true), "S₃ is solvable");
5249 assert_eq!(prof.coherent_rank, None, "the coefficient profile has no clauses ⇒ no scheme rank");
5250
5251 let distinct = PbConstraint::new_weighted(&[(0, 1, true), (1, 2, true), (2, 3, true)], 3);
5253 assert_eq!(pb_symmetry_profile(3, &[distinct]).order, 1, "distinct weights ⇒ trivial group");
5254 }
5255
5256 #[test]
5257 fn symmetry_structure_profiles_the_variable_group() {
5258 let p = |v| Lit::new(v, true);
5259 let n = |v| Lit::new(v, false);
5260
5261 let exactly1 = vec![
5263 vec![p(0), p(1), p(2)],
5264 vec![n(0), n(1)], vec![n(0), n(2)], vec![n(1), n(2)],
5265 ];
5266 let prof = symmetry_structure(3, &exactly1);
5267 assert_eq!(prof.order, 6, "|S₃| = 6");
5268 assert_eq!(prof.num_orbits, 1, "transitive on the 3 cells");
5269 assert_eq!(prof.rank, 2, "S₃ is 2-transitive ⇒ rank 2");
5270 assert_eq!(prof.coherent_rank, Some(2), "coherent (scheme) rank matches the orbital rank here");
5271 assert!(prof.coherent_rank.unwrap() <= prof.rank, "coherent rank ≤ orbital rank");
5272 assert_eq!(prof.transitivity, 3, "S₃ is 3-transitive on 3 points");
5273 assert!(prof.primitive, "S₃ on 3 points is primitive");
5274 assert_eq!(prof.blocks, None, "a primitive group has no block system");
5275 assert!(!prof.abelian, "S₃ is non-abelian");
5276 assert_eq!(prof.solvable, Some(true), "S₃ is solvable");
5277 assert_eq!(prof.nilpotent, Some(false), "S₃ is solvable but NOT nilpotent");
5278 assert_eq!(prof.derived_length, Some(2), "S₃ has derived length 2");
5279 assert_eq!(prof.nilpotency_class, None, "S₃ is not nilpotent ⇒ no nilpotency class");
5280 assert_eq!(prof.derived_order, 3, "[S₃,S₃] = A₃ has order 3");
5281 assert_eq!(prof.conjugacy_classes, Some(3), "S₃ has 3 conjugacy classes (= 3 irreps)");
5282 assert_eq!(prof.center_order, Some(1), "S₃ has a trivial centre");
5283 assert_eq!(prof.exponent, Some(6), "S₃ has exponent 6 (lcm of orders 1,2,3)");
5284 assert_eq!(prof.subgroups, Some(6), "S₃ has 6 subgroups");
5285 assert_eq!(prof.simple, Some(false), "S₃ is not simple (A₃ is normal)");
5286 assert_eq!(prof.composition_factors, Some(vec![2, 3]), "S₃ = C₂, C₃");
5287 assert_eq!(prof.sylow, Some(vec![(2, 3), (3, 1)]), "S₃: 3 Sylow-2, 1 Sylow-3");
5288 assert_eq!(prof.real_classes, Some(3), "S₃: all 3 classes (= irreps) are real");
5289 assert_eq!(prof.rational_classes, Some(3), "S₃ is rational: all 3 classes rational");
5290 assert_eq!(prof.automorphism_order, Some(6), "|Aut(S₃)| = 6 (S₃ is complete)");
5291 assert_eq!(prof.outer_automorphism_order, Some(1), "Out(S₃) = 1");
5292 assert_eq!(prof.irreducible_degrees, Some(vec![1, 1, 2]), "S₃ irreps: trivial, sign, 2-dim standard");
5293 assert_eq!(prof.frobenius_schur, Some(vec![1, 1, 1]), "S₃ is totally real ⇒ all indicators +1");
5294 {
5295 let iso = prof.isotypic_multiplicities.as_ref().expect("S₃ isotypic decomposition");
5298 let degs = prof.irreducible_degrees.as_ref().unwrap();
5299 assert_eq!(iso.iter().zip(degs).map(|(m, d)| m * d).sum::<u128>(), 3, "Σ m·d = 3 variables");
5300 assert_eq!(iso.iter().map(|m| m * m).sum::<u128>(), prof.rank as u128, "Σ m² = rank");
5301 }
5302
5303 let (clique, _) = crate::families::clique_coloring(3, 3);
5307 let cp = symmetry_structure(clique.num_vars, &clique.clauses);
5308 assert_eq!(cp.order, 36, "|S₃ × S₃| = 36");
5309 assert_eq!(cp.num_orbits, 1, "transitive on the 9 cells");
5310 assert_eq!(cp.rank, 4, "the grid action has rank 4");
5311 assert_eq!(cp.coherent_rank, Some(4), "clique(3,3): the coherent scheme has 4 relations");
5312 assert_eq!(cp.transitivity, 1, "transitive but not 2-transitive");
5313 assert!(!cp.primitive, "the grid action is imprimitive");
5314 assert!(cp.blocks.is_some(), "rows/columns form a block system");
5315 assert!(!cp.abelian, "S₃ × S₃ is non-abelian");
5316 assert_eq!(cp.solvable, Some(true), "S₃ × S₃ is solvable");
5317 assert_eq!(cp.nilpotent, Some(false), "S₃ × S₃ is not nilpotent (S₃ isn't)");
5318 assert_eq!(cp.derived_order, 9, "[S₃×S₃, S₃×S₃] = A₃ × A₃ has order 9");
5319 assert_eq!(cp.conjugacy_classes, Some(9), "S₃×S₃ has 3·3 = 9 conjugacy classes");
5320 assert_eq!(cp.center_order, Some(1), "S₃×S₃ has a trivial centre");
5321 assert_eq!(cp.rational_classes, Some(9), "S₃×S₃ is rational: all 9 classes rational");
5322 assert_eq!(cp.automorphism_order, Some(72), "|Aut(S₃×S₃)| = 72");
5324 assert_eq!(cp.outer_automorphism_order, Some(2), "Out(S₃×S₃) = C₂ (factor swap)");
5325 assert_eq!(cp.assignment_orbits, Some(36), "2⁹ assignments up to S₃×S₃ = 36 binary 3×3 matrices");
5326 assert_eq!(cp.abelianization, Some((4, 2)), "(S₃×S₃)ᵃᵇ = C₂×C₂ (order 4, exponent 2)");
5327 assert!(cp.subgroups.is_some(), "the S₃×S₃ subgroup lattice is computed");
5328 assert_eq!(cp.simple, Some(false), "S₃×S₃ is not simple");
5329 assert_eq!(cp.composition_factors, Some(vec![2, 2, 3, 3]), "S₃×S₃ = C₂², C₃² (product 36)");
5330 assert_eq!(cp.sylow, Some(vec![(2, 9), (3, 1)]), "S₃×S₃: 3² = 9 Sylow-2, 1 Sylow-3");
5331 assert_eq!(
5334 cp.irreducible_degrees,
5335 Some(vec![1, 1, 1, 1, 2, 2, 2, 2, 4]),
5336 "S₃×S₃ irreps = products of the S₃ irreps"
5337 );
5338 assert_eq!(
5339 cp.frobenius_schur,
5340 Some(vec![1, 1, 1, 1, 1, 1, 1, 1, 1]),
5341 "S₃×S₃ is totally real ⇒ all nine indicators +1"
5342 );
5343 {
5344 let iso = cp.isotypic_multiplicities.as_ref().expect("S₃×S₃ isotypic decomposition");
5346 let degs = cp.irreducible_degrees.as_ref().unwrap();
5347 assert_eq!(iso.iter().zip(degs).map(|(m, d)| m * d).sum::<u128>(), 9, "Σ m·d = 9 cells");
5348 assert_eq!(iso.iter().map(|m| m * m).sum::<u128>(), cp.rank as u128, "⟨π,π⟩ = rank = 4");
5349 }
5350
5351 let asym = vec![vec![p(0)], vec![n(1), p(2)]];
5353 let ap = symmetry_structure(3, &asym);
5354 assert_eq!(ap.order, 1, "no symmetry ⇒ trivial group");
5355 assert!(ap.coherent_rank.is_some(), "the scheme rank is always computed from the clauses");
5356 assert_eq!(ap.irreducible_degrees, Some(vec![1]), "trivial group: one trivial irreducible");
5357 assert_eq!(ap.frobenius_schur, Some(vec![1]), "trivial group: its character is real");
5358 assert_eq!(
5359 ap.isotypic_multiplicities,
5360 Some(vec![3]),
5361 "trivial group on 3 vars: the perm rep is 3 copies of the trivial irreducible"
5362 );
5363 assert_eq!(ap.rational_classes, Some(1), "trivial group: its one class is rational");
5364 assert_eq!(ap.automorphism_order, Some(1), "trivial group: Aut is trivial");
5365 assert_eq!(ap.outer_automorphism_order, Some(1), "trivial group: Out is trivial");
5366 }
5367
5368 #[test]
5369 fn models_up_to_symmetry_enumerates_orbits_and_counts_exactly() {
5370 let p = |v| Lit::new(v, true);
5371 let n = |v| Lit::new(v, false);
5372
5373 let oracle = |nv: usize, cl: &[Vec<Lit>]| -> (u128, usize) {
5375 let models: Vec<Vec<bool>> = (0u64..(1u64 << nv))
5376 .filter_map(|x| {
5377 let a: Vec<bool> = (0..nv).map(|i| (x >> i) & 1 == 1).collect();
5378 cl.iter().all(|c| c.iter().any(|l| a[l.var() as usize] == l.is_positive())).then_some(a)
5379 })
5380 .collect();
5381 let gens = crate::sym_break::variable_automorphism_generators(nv, cl).unwrap_or_default();
5382 let model_set: std::collections::HashSet<Vec<bool>> = models.iter().cloned().collect();
5383 let mut seen = std::collections::HashSet::new();
5384 let mut orbits = 0;
5385 for m in &models {
5386 if seen.contains(m) {
5387 continue;
5388 }
5389 orbits += 1;
5390 let mut stack = vec![m.clone()];
5391 while let Some(cur) = stack.pop() {
5392 if !seen.insert(cur.clone()) {
5393 continue;
5394 }
5395 for g in &gens {
5396 let mut pm = vec![false; nv];
5397 for v in 0..nv {
5398 pm[g[v]] = cur[v];
5399 }
5400 if model_set.contains(&pm) && !seen.contains(&pm) {
5401 stack.push(pm);
5402 }
5403 }
5404 }
5405 }
5406 (models.len() as u128, orbits)
5407 };
5408
5409 let exactly1 = vec![
5411 vec![p(0), p(1), p(2)],
5412 vec![n(0), n(1)], vec![n(0), n(2)], vec![n(1), n(2)],
5413 ];
5414 let atmost1 = vec![vec![n(0), n(1)], vec![n(0), n(2)], vec![n(1), n(2)]];
5416
5417 for cl in [&exactly1, &atmost1] {
5418 let (m_exact, m_orbits) = oracle(3, cl);
5419 let sc = models_up_to_symmetry(3, cl, 1000);
5420 assert!(sc.exhaustive, "the small instance is enumerated to exhaustion");
5421 assert_eq!(sc.total_models, m_exact, "exact model count = sum of orbit sizes");
5422 assert_eq!(sc.representatives.len(), m_orbits, "one representative per orbit");
5423 if let Some(burnside) = crate::sym_break::count_models_modulo_symmetry(3, cl) {
5425 assert_eq!(sc.representatives.len(), burnside, "enumeration agrees with Burnside");
5426 }
5427 for r in &sc.representatives {
5429 assert!(cl.iter().all(|c| c.iter().any(|l| r[l.var() as usize] == l.is_positive())), "valid model");
5430 }
5431 let distinct: std::collections::HashSet<&Vec<bool>> = sc.representatives.iter().collect();
5432 assert_eq!(distinct.len(), sc.representatives.len(), "representatives are distinct");
5433 }
5434
5435 assert_eq!(models_up_to_symmetry(3, &exactly1, 1000).total_models, 3);
5437 assert_eq!(models_up_to_symmetry(3, &exactly1, 1000).representatives.len(), 1);
5438 assert_eq!(models_up_to_symmetry(3, &atmost1, 1000).total_models, 4);
5439 assert_eq!(models_up_to_symmetry(3, &atmost1, 1000).representatives.len(), 2);
5440 }
5441
5442 #[test]
5443 fn declared_symmetry_is_verified_then_broken() {
5444 let p = |v| Lit::new(v, true);
5445 let brute = |cl: &[Vec<Lit>], nv: usize| {
5446 (0u64..(1u64 << nv)).any(|x| {
5447 let a: Vec<bool> = (0..nv).map(|i| (x >> i) & 1 == 1).collect();
5448 cl.iter().all(|c| c.iter().any(|l| a[l.var() as usize] == l.is_positive()))
5449 })
5450 };
5451
5452 let (cnf, _) = crate::families::clique_coloring(3, 3);
5455 let nv = cnf.num_vars;
5456 let mut vswap: Vec<usize> = (0..nv).collect();
5457 for c in 0..3 {
5458 vswap.swap(c, 3 + c);
5459 }
5460 assert!(is_declared_symmetry(nv, &cnf.clauses, &vswap), "a vertex swap is a genuine clique symmetry");
5461 let s = solve_with_declared_symmetry(nv, &cnf.clauses, &[vswap]);
5462 assert_eq!(s.via, Route::DeclaredSymmetry);
5463 match &s.answer {
5464 Answer::Sat(m) => assert!(cnf.clauses.iter().all(|c| c.iter().any(|l| m[l.var() as usize] == l.is_positive()))),
5465 Answer::Unsat => panic!("clique_coloring(3,3) is SAT"),
5466 }
5467
5468 let mut bogus: Vec<usize> = (0..nv).collect();
5471 bogus.swap(0, 5); assert!(!is_declared_symmetry(nv, &cnf.clauses, &bogus), "a non-symmetry must be rejected");
5473 let wb = solve_with_declared_symmetry(nv, &cnf.clauses, &[bogus]);
5474 assert!(matches!(wb.answer, Answer::Sat(_)), "a bogus declaration must not corrupt the SAT verdict");
5475 if let Answer::Sat(m) = &wb.answer {
5476 assert!(cnf.clauses.iter().all(|c| c.iter().any(|l| m[l.var() as usize] == l.is_positive())));
5477 }
5478
5479 let f = vec![vec![p(0), p(2)], vec![p(1), p(2)], vec![p(0), p(2), p(3)]];
5481 let mut ab: Vec<usize> = (0..4).collect();
5482 ab.swap(0, 1);
5483 assert!(is_declared_symmetry(4, &f, &ab), "a↔b is a semantic symmetry, verified by implication");
5484 let sem = solve_with_declared_symmetry(4, &f, &[ab]);
5485 assert_eq!(sem.via, Route::DeclaredSymmetry);
5486 assert_eq!(matches!(sem.answer, Answer::Sat(_)), brute(&f, 4), "declared-symmetry verdict matches brute force");
5487
5488 assert!(!is_declared_symmetry(4, &f, &[0usize, 1]), "a wrong-length permutation is rejected");
5490 let mf = solve_with_declared_symmetry(4, &f, &[vec![0usize, 1]]);
5491 assert_eq!(
5492 matches!(mf.answer, Answer::Sat(_)),
5493 matches!(solve_comprehensive(4, &f).answer, Answer::Sat(_)),
5494 "a malformed declaration is dropped, verdict unchanged"
5495 );
5496 }
5497
5498 #[test]
5499 fn almost_symmetry_breaks_a_near_miss_conditionally() {
5500 let p = |v| Lit::new(v, true);
5501 let brute = |cl: &[Vec<Lit>], nv: usize| {
5502 (0u64..(1u64 << nv)).any(|x| {
5503 let a: Vec<bool> = (0..nv).map(|i| (x >> i) & 1 == 1).collect();
5504 cl.iter().all(|c| c.iter().any(|l| a[l.var() as usize] == l.is_positive()))
5505 })
5506 };
5507 let f = vec![vec![p(0), p(2)], vec![p(1), p(2)], vec![p(0), p(3)]];
5510
5511 let (sem, _) = semantic_symmetry_pairs(4, &f);
5513 assert!(!sem.contains(&(0, 1)), "a,b is not a SEMANTIC symmetry here: {sem:?}");
5514
5515 let almost = almost_symmetry_pairs(4, &f, 2);
5517 assert!(
5518 almost.iter().any(|(a, b, imgs)| *a == 0 && *b == 1 && imgs.len() == 1),
5519 "a↔b breaks exactly one clause: {almost:?}"
5520 );
5521
5522 let s = almost_symmetry_solve(4, &f).expect("an almost-symmetry is detected and conditionally broken");
5524 assert_eq!(s.via, Route::AlmostSymmetry);
5525 assert_eq!(matches!(s.answer, Answer::Sat(_)), brute(&f, 4), "almost-symmetry verdict matches brute force");
5526 if let Answer::Sat(m) = &s.answer {
5527 assert!(f.iter().all(|c| c.iter().any(|l| m[l.var() as usize] == l.is_positive())), "valid model");
5528 }
5529
5530 let mut un = f.clone();
5532 un.extend([
5533 vec![Lit::new(0, false)],
5534 vec![Lit::new(1, false)],
5535 vec![Lit::new(2, false)],
5536 vec![Lit::new(3, false)],
5537 ]);
5538 let u = almost_symmetry_solve(4, &un).expect("almost-symmetry still detected");
5539 assert_eq!(u.via, Route::AlmostSymmetry);
5540 assert!(matches!(u.answer, Answer::Unsat), "all variables off makes (a∨x) UNSAT");
5541 assert_eq!(matches!(u.answer, Answer::Sat(_)), brute(&un, 4), "UNSAT verdict matches brute force");
5542 }
5543
5544 #[test]
5545 fn semantic_symmetry_breaks_a_non_syntactic_interchange() {
5546 let p = |v| Lit::new(v, true);
5547 let f = vec![vec![p(0), p(2)], vec![p(1), p(2)], vec![p(0), p(2), p(3)]];
5551
5552 let (pairs, non_syntactic) = semantic_symmetry_pairs(4, &f);
5554 assert!(pairs.contains(&(0, 1)) && non_syntactic, "a,b are a semantic, non-syntactic symmetry: {pairs:?}");
5555
5556 let canon_set = |swap: bool| -> std::collections::HashSet<Vec<(u32, bool)>> {
5558 f.iter()
5559 .map(|c| {
5560 let mut k: Vec<(u32, bool)> = c
5561 .iter()
5562 .map(|l| {
5563 let v = l.var() as usize;
5564 let nv = if swap && v == 0 { 1 } else if swap && v == 1 { 0 } else { v };
5565 (nv as u32, l.is_positive())
5566 })
5567 .collect();
5568 k.sort_unstable();
5569 k
5570 })
5571 .collect()
5572 };
5573 assert_ne!(canon_set(true), canon_set(false), "the a↔b swap changes the clause set — not syntactic");
5574
5575 let s = semantic_symmetry_solve(4, &f).expect("a semantic symmetry is detected and broken");
5577 assert_eq!(s.via, Route::SemanticSymmetry);
5578 let brute = (0u64..16).any(|x| {
5579 let a: Vec<bool> = (0..4).map(|i| (x >> i) & 1 == 1).collect();
5580 f.iter().all(|c| c.iter().any(|l| a[l.var() as usize] == l.is_positive()))
5581 });
5582 assert_eq!(matches!(s.answer, Answer::Sat(_)), brute, "semantic-symmetry verdict matches brute force");
5583 if let Answer::Sat(m) = &s.answer {
5584 assert!(f.iter().all(|c| c.iter().any(|l| m[l.var() as usize] == l.is_positive())), "valid model");
5585 }
5586
5587 let syntactic = vec![vec![p(0), p(2)], vec![p(1), p(2)]];
5590 assert!(
5591 semantic_symmetry_solve(3, &syntactic).is_none(),
5592 "a purely syntactic symmetry is left to the syntactic route"
5593 );
5594 }
5595
5596 #[test]
5597 fn nested_block_tower_breaks_multidimensional_symmetry() {
5598 let p = |v| Lit::new(v, true);
5599 let brute = |nv: usize, cl: &[Vec<Lit>]| -> bool {
5600 (0u64..(1u64 << nv)).any(|x| {
5601 let a: Vec<bool> = (0..nv).map(|i| (x >> i) & 1 == 1).collect();
5602 cl.iter().all(|c| c.iter().any(|l| a[l.var() as usize] == l.is_positive()))
5603 })
5604 };
5605
5606 let (sat, _) = crate::families::clique_coloring(3, 3);
5608 let s = nested_symmetry_solve(sat.num_vars, &sat.clauses).expect("a grid symmetry has a block system");
5609 assert_eq!(s.via, Route::NestedSymmetry);
5610 match &s.answer {
5611 Answer::Sat(m) => assert!(sat.clauses.iter().all(|c| c.iter().any(|l| m[l.var() as usize] == l.is_positive()))),
5612 Answer::Unsat => panic!("clique_coloring(3,3) is SAT"),
5613 }
5614 assert_eq!(matches!(s.answer, Answer::Sat(_)), brute(sat.num_vars, &sat.clauses), "verdict matches brute");
5615
5616 let (unsat, _) = crate::families::clique_coloring(4, 3);
5618 let u = nested_symmetry_solve(unsat.num_vars, &unsat.clauses).expect("a grid symmetry has a block system");
5619 assert_eq!(u.via, Route::NestedSymmetry);
5620 assert!(matches!(u.answer, Answer::Unsat), "clique_coloring(4,3) is UNSAT");
5621 assert_eq!(matches!(u.answer, Answer::Sat(_)), brute(unsat.num_vars, &unsat.clauses), "verdict matches brute");
5622
5623 let mut cube: Vec<Vec<Lit>> = Vec::new();
5627 for v in 0u32..8 {
5628 for b in 0..3 {
5629 let w = v ^ (1 << b);
5630 if v < w {
5631 cube.push(vec![p(v), p(w)]);
5632 }
5633 }
5634 }
5635 let c = nested_symmetry_solve(8, &cube).expect("the cube's nested block tower engages");
5636 assert_eq!(c.via, Route::NestedSymmetry);
5637 match &c.answer {
5638 Answer::Sat(m) => assert!(cube.iter().all(|cl| cl.iter().any(|l| m[l.var() as usize] == l.is_positive()))),
5639 Answer::Unsat => panic!("covering every cube edge is SAT (e.g. all true)"),
5640 }
5641 assert_eq!(matches!(c.answer, Answer::Sat(_)), brute(8, &cube), "the nested-tower verdict matches brute force");
5642 }
5643
5644 #[test]
5645 fn symmetry_revealed_by_simplification_is_unlocked_and_broken() {
5646 let p = |v| Lit::new(v, true);
5647 let n = |v| Lit::new(v, false);
5648 let unlock = vec![vec![p(0)], vec![p(1), p(2), n(0)], vec![p(1), p(3)]];
5652 let s = symmetry_via_simplification_solve(4, &unlock).expect("simplification unlocks symmetry");
5653 assert_eq!(s.via, Route::SymmetrySimplify);
5654 match &s.answer {
5655 Answer::Sat(m) => {
5656 assert!(unlock.iter().all(|c| c.iter().any(|l| m[l.var() as usize] == l.is_positive())));
5657 assert!(m[0], "the forced literal x0 is re-applied to the model");
5658 }
5659 Answer::Unsat => panic!("the instance is SAT"),
5660 }
5661 let brute = (0u64..16).any(|x| {
5662 let a: Vec<bool> = (0..4).map(|i| (x >> i) & 1 == 1).collect();
5663 unlock.iter().all(|c| c.iter().any(|l| a[l.var() as usize] == l.is_positive()))
5664 });
5665 assert_eq!(matches!(s.answer, Answer::Sat(_)), brute, "verdict matches brute force");
5666
5667 let already = vec![vec![p(0)], vec![p(1), p(2)], vec![p(1), p(3)]];
5669 assert!(
5670 symmetry_via_simplification_solve(4, &already).is_none(),
5671 "symmetry already present on the raw formula ⟹ nothing unlocked"
5672 );
5673
5674 let conflict = vec![vec![p(0)], vec![p(1)], vec![n(0), n(1)]];
5676 let u = symmetry_via_simplification_solve(2, &conflict).expect("BCP reaches a conflict");
5677 assert_eq!(u.via, Route::SymmetrySimplify);
5678 assert!(matches!(u.answer, Answer::Unsat), "x0 ∧ x1 ∧ ¬(x0∧x1) is UNSAT");
5679 }
5680
5681 #[test]
5682 fn symmetric_binary_inference_learns_implication_orbits() {
5683 let p = |v| Lit::new(v, true);
5684 let n = |v| Lit::new(v, false);
5685 let chain = vec![
5688 vec![n(0), p(3)], vec![n(1), p(3)], vec![n(2), p(3)], vec![n(3), p(4)], ];
5691 let s = symmetric_binary_inference_solve(5, &chain)
5692 .expect("a derived implication orbit is learned");
5693 assert_eq!(s.via, Route::SymmetricBinary);
5694 match &s.answer {
5695 Answer::Sat(m) => assert!(
5696 chain.iter().all(|c| c.iter().any(|l| m[l.var() as usize] == l.is_positive())),
5697 "the strengthened formula yields a valid model"
5698 ),
5699 Answer::Unsat => panic!("the chain is SAT"),
5700 }
5701 let brute = (0u64..32).any(|x| {
5703 let a: Vec<bool> = (0..5).map(|i| (x >> i) & 1 == 1).collect();
5704 chain.iter().all(|c| c.iter().any(|l| a[l.var() as usize] == l.is_positive()))
5705 });
5706 assert_eq!(matches!(s.answer, Answer::Sat(_)), brute, "binary-inference verdict matches brute force");
5707
5708 let direct = vec![vec![n(0), p(2)], vec![n(1), p(2)]]; assert!(
5712 symmetric_binary_inference_solve(3, &direct).is_none(),
5713 "no new implication to learn ⟹ declines"
5714 );
5715 }
5716
5717 #[test]
5718 fn symmetric_component_decomposition_solves_copies_once() {
5719 let p = |v| Lit::new(v, true);
5720 let n = |v| Lit::new(v, false);
5721 let sat = vec![vec![p(0), p(1)], vec![p(2), p(3)]];
5724 let s = symmetric_component_solve(4, &sat).expect("two symmetric components decompose");
5725 assert_eq!(s.via, Route::SymmetricComponent);
5726 match &s.answer {
5727 Answer::Sat(m) => assert!(
5728 sat.iter().all(|c| c.iter().any(|l| m[l.var() as usize] == l.is_positive())),
5729 "the assembled model is valid"
5730 ),
5731 Answer::Unsat => panic!("two copies of (x∨y) is SAT"),
5732 }
5733
5734 let unsat = vec![
5738 vec![p(0)], vec![p(1)], vec![n(0), n(1)],
5739 vec![p(2)], vec![p(3)], vec![n(2), n(3)],
5740 ];
5741 let u = symmetric_component_solve(4, &unsat).expect("two symmetric components decompose");
5742 assert_eq!(u.via, Route::SymmetricComponent);
5743 assert!(matches!(u.answer, Answer::Unsat), "an UNSAT component makes F UNSAT");
5744
5745 for cl in [&sat, &unsat] {
5747 let brute = (0u64..16).any(|x| {
5748 let a: Vec<bool> = (0..4).map(|i| (x >> i) & 1 == 1).collect();
5749 cl.iter().all(|c| c.iter().any(|l| a[l.var() as usize] == l.is_positive()))
5750 });
5751 let got = symmetric_component_solve(4, cl).expect("decomposition fires");
5752 assert_eq!(
5753 matches!(got.answer, Answer::Sat(_)),
5754 brute,
5755 "component-decomposition verdict matches brute force"
5756 );
5757 }
5758
5759 let (clique, _) = crate::families::clique_coloring(3, 3);
5761 assert!(
5762 symmetric_component_solve(clique.num_vars, &clique.clauses).is_none(),
5763 "a single component is not decomposable"
5764 );
5765 }
5766
5767 #[test]
5768 fn plain_component_decomposition_solves_asymmetric_independent_parts() {
5769 let p = |v| Lit::new(v, true);
5770 let n = |v| Lit::new(v, false);
5771 let sat = vec![vec![p(0), p(1)], vec![p(2), p(3)], vec![n(2), n(3)]];
5775 assert!(symmetric_component_solve(4, &sat).is_none(), "asymmetric components: the symmetric route declines");
5776 let s = solve_by_components(4, &sat);
5777 assert_eq!(s.via, Route::Component);
5778 match &s.answer {
5779 Answer::Sat(m) => assert!(
5780 sat.iter().all(|c| c.iter().any(|l| m[l.var() as usize] == l.is_positive())),
5781 "the assembled model satisfies every clause"
5782 ),
5783 Answer::Unsat => panic!("both components are satisfiable, so F is SAT"),
5784 }
5785
5786 let unsat = vec![vec![p(0), p(1)], vec![p(2)], vec![n(2)]];
5788 let u = solve_by_components(3, &unsat);
5789 assert_eq!(u.via, Route::Component);
5790 assert!(matches!(u.answer, Answer::Unsat), "an UNSAT component makes F UNSAT");
5791
5792 let single = vec![vec![p(0), p(1)], vec![n(0), p(1)]];
5794 assert_ne!(solve_by_components(2, &single).via, Route::Component, "one component is not decomposable");
5795
5796 for (nv, cl) in [(4usize, &sat), (3, &unsat)] {
5798 let brute = (0u64..(1 << nv)).any(|x| {
5799 let a: Vec<bool> = (0..nv).map(|i| (x >> i) & 1 == 1).collect();
5800 cl.iter().all(|c| c.iter().any(|l| a[l.var() as usize] == l.is_positive()))
5801 });
5802 assert_eq!(matches!(solve_by_components(nv, cl).answer, Answer::Sat(_)), brute, "matches brute force");
5803 }
5804 }
5805
5806 #[test]
5807 fn symmetry_propagation_breaks_during_search_and_is_correct() {
5808 let (sat, _) = crate::families::clique_coloring(3, 3);
5811 let s = symmetry_propagate_solve(sat.num_vars, &sat.clauses)
5812 .expect("a phase-free variable symmetry drives the propagator");
5813 assert_eq!(s.via, Route::SymmetryPropagate);
5814 match &s.answer {
5815 Answer::Sat(m) => assert!(
5816 sat.clauses.iter().all(|c| c.iter().any(|l| m[l.var() as usize] == l.is_positive())),
5817 "the propagator returns a valid model"
5818 ),
5819 Answer::Unsat => panic!("clique_coloring(3,3) is SAT"),
5820 }
5821
5822 let (unsat, _) = crate::families::clique_coloring(4, 3);
5825 let u = symmetry_propagate_solve(unsat.num_vars, &unsat.clauses).expect("variable symmetry");
5826 assert_eq!(u.via, Route::SymmetryPropagate);
5827 assert!(matches!(u.answer, Answer::Unsat), "clique_coloring(4,3) is UNSAT");
5828
5829 for (cnf, _) in [crate::families::clique_coloring(3, 3), crate::families::clique_coloring(4, 3)] {
5831 let nv = cnf.num_vars;
5832 let brute = (0u64..(1u64 << nv)).any(|x| {
5833 let a: Vec<bool> = (0..nv).map(|i| (x >> i) & 1 == 1).collect();
5834 cnf.clauses.iter().all(|c| c.iter().any(|l| a[l.var() as usize] == l.is_positive()))
5835 });
5836 let got = symmetry_propagate_solve(nv, &cnf.clauses).expect("propagator fires");
5837 assert_eq!(
5838 matches!(got.answer, Answer::Sat(_)),
5839 brute,
5840 "symmetry-propagation verdict matches brute force (nv={nv})"
5841 );
5842 }
5843 }
5844
5845 #[test]
5846 fn orbit_weight_quotient_collapses_a_full_symmetric_instance() {
5847 let p = |v| Lit::new(v, true);
5848 let at_least_2 = vec![vec![p(0), p(1)], vec![p(0), p(2)], vec![p(1), p(2)]];
5850 let s = orbit_weight_quotient_solve(3, &at_least_2)
5851 .expect("a full symmetric group collapses to weight classes");
5852 assert_eq!(s.via, Route::OrbitWeightQuotient);
5853 match &s.answer {
5854 Answer::Sat(m) => {
5855 assert!(at_least_2.iter().all(|c| c.iter().any(|l| m[l.var() as usize] == l.is_positive())));
5856 assert!(m.iter().filter(|&&b| b).count() >= 2, "the witness has weight ≥ 2");
5857 }
5858 Answer::Unsat => panic!("at-least-2 of 3 is SAT"),
5859 }
5860
5861 let subsets3 = [[0u32, 1, 2], [0, 1, 3], [0, 2, 3], [1, 2, 3]];
5866 let pairs = [[0u32, 1], [0, 2], [0, 3], [1, 2], [1, 3], [2, 3]];
5867 let mut card: Vec<Vec<Lit>> = Vec::new();
5868 for sub in subsets3 {
5869 card.push(sub.iter().map(|&v| Lit::new(v, true)).collect()); }
5871 for pr in pairs {
5872 card.push(pr.iter().map(|&v| Lit::new(v, false)).collect()); }
5874 let u = orbit_weight_quotient_solve(4, &card).expect("S₄ is the full symmetric group on the orbit");
5875 assert_eq!(u.via, Route::OrbitWeightQuotient);
5876 assert!(matches!(u.answer, Answer::Unsat), "≥3 and ≤1 true is unsatisfiable");
5877
5878 for (nv, cl) in [(3usize, &at_least_2), (4, &card)] {
5880 let brute = (0u64..(1u64 << nv)).any(|x| {
5881 let a: Vec<bool> = (0..nv).map(|i| (x >> i) & 1 == 1).collect();
5882 cl.iter().all(|c| c.iter().any(|l| a[l.var() as usize] == l.is_positive()))
5883 });
5884 let got = orbit_weight_quotient_solve(nv, cl).expect("quotient fires");
5885 assert_eq!(
5886 matches!(got.answer, Answer::Sat(_)),
5887 brute,
5888 "orbit-weight-quotient verdict matches brute force (nv={nv})"
5889 );
5890 }
5891
5892 let (clique, _) = crate::families::clique_coloring(3, 3);
5896 assert!(
5897 orbit_weight_quotient_solve(clique.num_vars, &clique.clauses).is_none(),
5898 "a product symmetry that is not the full symmetric group is not a weight quotient"
5899 );
5900 }
5901
5902 #[test]
5903 fn symmetric_probe_infers_a_whole_orbit_from_one_failed_literal() {
5904 let y = |b| Lit::new(3, b);
5905 let nx = |v| Lit::new(v, false);
5906 let base: Vec<Vec<Lit>> =
5908 (0u32..3).flat_map(|v| [vec![nx(v), y(true)], vec![nx(v), y(false)]]).collect();
5909
5910 let s = symmetric_probe_solve(4, &base).expect("a symmetric failed literal engages the probe");
5913 assert_eq!(s.via, Route::SymmetricProbe);
5914 match &s.answer {
5915 Answer::Sat(m) => {
5916 assert!(base.iter().all(|c| c.iter().any(|l| m[l.var() as usize] == l.is_positive())));
5917 assert!(!m[0] && !m[1] && !m[2], "the whole orbit was inferred false from one probe");
5918 }
5919 Answer::Unsat => panic!("the base instance is SAT"),
5920 }
5921
5922 let mut unsat = base.clone();
5924 unsat.push(vec![Lit::new(0, true), Lit::new(1, true), Lit::new(2, true)]);
5925 let u = symmetric_probe_solve(4, &unsat).expect("the probe engages");
5926 assert_eq!(u.via, Route::SymmetricProbe);
5927 assert!(matches!(u.answer, Answer::Unsat), "forcing the orbit false refutes the cardinality clause");
5928
5929 for cl in [&base, &unsat] {
5931 let brute = (0u64..16).any(|x| {
5932 let a: Vec<bool> = (0..4).map(|i| (x >> i) & 1 == 1).collect();
5933 cl.iter().all(|c| c.iter().any(|l| a[l.var() as usize] == l.is_positive()))
5934 });
5935 let got = symmetric_probe_solve(4, cl).expect("probe fires");
5936 assert_eq!(
5937 matches!(got.answer, Answer::Sat(_)),
5938 brute,
5939 "symmetric-probe verdict matches brute force"
5940 );
5941 }
5942 }
5943
5944 #[test]
5945 fn local_symmetry_solve_exploits_branch_symmetry_and_is_correct() {
5946 let f = vec![
5950 vec![Lit::new(0, false), Lit::new(1, true), Lit::new(2, true)], vec![Lit::new(0, false), Lit::new(1, false), Lit::new(2, false)], vec![Lit::new(0, true), Lit::new(1, true)], ];
5954 let brute = (0u64..8).any(|x| {
5955 let a: Vec<bool> = (0..3).map(|i| (x >> i) & 1 == 1).collect();
5956 f.iter().all(|c| c.iter().any(|l| a[l.var() as usize] == l.is_positive()))
5957 });
5958 let solved = local_symmetry_solve(3, &f).expect("a branch reveals local symmetry");
5959 assert_eq!(solved.via, Route::LocalSymmetry);
5960 assert_eq!(matches!(solved.answer, Answer::Sat(_)), brute, "local-symmetry verdict matches brute force");
5961 if let Answer::Sat(m) = &solved.answer {
5962 assert!(
5963 f.iter().all(|c| c.iter().any(|l| m[l.var() as usize] == l.is_positive())),
5964 "the model from a local-symmetry branch satisfies F"
5965 );
5966 }
5967 }
5968
5969 #[test]
5970 fn symmetry_breaking_scales_to_a_large_group_via_partial_breaking() {
5971 let (cnf, _) = crate::families::clique_coloring(6, 6);
5975 let s = symmetry_break_solve(cnf.num_vars, &cnf.clauses)
5976 .expect("a large phase-free symmetry group still drives partial breaking");
5977 assert_eq!(s.via, Route::SymmetryBreak);
5978 match s.answer {
5979 Answer::Sat(m) => assert!(
5980 cnf.clauses.iter().all(|c| c.iter().any(|l| m[l.var() as usize] == l.is_positive())),
5981 "partial breaking returns a valid model"
5982 ),
5983 Answer::Unsat => panic!("clique_coloring(6,6) is SAT"),
5984 }
5985 }
5986
5987 #[test]
5988 fn the_composite_lift_verdict_matches_the_supplied_equations() {
5989 use crate::modm::{solve as modm_solve, ModmOutcome};
5995 for (eqs, cnf, want) in [
5996 crate::families::mod_p_tseitin_expander(6, 6, 7),
5997 crate::families::mod_p_consistent_onehot(6, 6, 7),
5998 ] {
5999 let solved = solve_structured(cnf.num_vars, &cnf.clauses);
6000 assert_eq!(solved.via, Route::ModM, "a composite instance must take the ℤ/m route");
6001 let num_gf_vars = cnf.num_vars / 6; let supplied_unsat = matches!(modm_solve(&eqs, num_gf_vars, 6), Some(ModmOutcome::Unsat { .. }));
6003 assert_eq!(
6004 matches!(solved.answer, Answer::Unsat),
6005 supplied_unsat,
6006 "the lifted-CNF verdict must match modm::solve on the supplied equations"
6007 );
6008 assert_eq!(
6009 matches!(solved.answer, Answer::Unsat),
6010 matches!(want, crate::families::ExpectedVerdict::Unsat),
6011 "and the family's declared expectation"
6012 );
6013 }
6014 }
6015
6016 #[test]
6017 fn mine_clauses_derives_an_implied_unit_via_probing() {
6018 let clauses = vec![vec![Lit::new(0, true)], vec![Lit::new(0, false), Lit::new(1, true)]];
6020 let mined = mine_clauses(2, &clauses);
6021 assert!(
6022 mined.iter().any(|c| c.len() == 1 && c[0].var() == 1 && c[0].is_positive()),
6023 "expected mined implied unit b; got {mined:?}"
6024 );
6025 }
6026
6027 #[test]
6028 fn every_mined_clause_is_implied() {
6029 let clauses = vec![
6031 xor_gadget(&[0, 1, 2], false),
6032 vec![vec![Lit::new(0, true)]],
6033 vec![vec![Lit::new(1, true)]],
6034 ]
6035 .concat();
6036 let n = 3;
6037 let mined = mine_clauses(n, &clauses);
6038 assert!(!mined.is_empty(), "this instance has implied structure to mine");
6039 for mask in 0u32..(1 << n) {
6040 let asg: Vec<bool> = (0..n).map(|v| (mask >> v) & 1 == 1).collect();
6041 let is_model = clauses.iter().all(|c| c.iter().any(|l| asg[l.var() as usize] == l.is_positive()));
6042 if is_model {
6043 for mc in &mined {
6044 assert!(
6045 mc.iter().any(|l| asg[l.var() as usize] == l.is_positive()),
6046 "mined clause {mc:?} is not implied (fails model {asg:?})"
6047 );
6048 }
6049 }
6050 }
6051 }
6052
6053 #[test]
6064 fn exact_cover_lift_crushes_modular_counting_and_the_chessboard() {
6065 for n in [7usize, 9, 11] {
6067 let (cnf, _) = crate::families::mod_counting(n, 2);
6068 let s = solve_structured(cnf.num_vars, &cnf.clauses);
6069 assert!(matches!(s.answer, Answer::Unsat), "Count_2({n}) is UNSAT");
6070 assert_eq!(s.via, Route::ExactCover, "Count_2({n}): the exact-cover lift fires");
6071 assert_eq!(s.conflicts, 0, "Count_2({n}): zero search");
6072 }
6073 for (n, q) in [(7usize, 3usize), (8, 3), (6, 5), (7, 5)] {
6075 let (cnf, _) = crate::families::mod_counting(n, q);
6076 let s = solve_structured(cnf.num_vars, &cnf.clauses);
6077 assert!(matches!(s.answer, Answer::Unsat), "Count_{q}({n}) is UNSAT");
6078 assert_eq!(s.via, Route::ExactCover, "Count_{q}({n}): the exact-cover lift fires");
6079 }
6080 let (cb, _) = crate::families::mutilated_chessboard(4);
6083 let s = solve_structured(cb.num_vars, &cb.clauses);
6084 assert!(matches!(s.answer, Answer::Unsat), "chessboard(4) is UNSAT");
6085 assert_eq!(s.conflicts, 0, "chessboard(4): a specialist decides — zero search");
6086 assert_ne!(s.via, Route::Cdcl, "chessboard(4): never the fallback");
6087 let (sat6, _) = crate::families::mod_counting(6, 3);
6089 let s = solve_structured(sat6.num_vars, &sat6.clauses);
6090 match s.answer {
6091 Answer::Sat(model) => {
6092 assert!(
6093 sat6.clauses.iter().all(|c| c.iter().any(|l| model[l.var() as usize] == l.is_positive())),
6094 "Count_3(6): the SAT model re-checks"
6095 );
6096 }
6097 Answer::Unsat => panic!("Count_3(6) is satisfiable — the lift must decline"),
6098 }
6099 }
6100
6101 #[test]
6110 #[ignore = "scale measurement — symmetry-arsenal wall time on Ramsey; run explicitly"]
6111 fn ramsey_symmetric_attack_is_measured() {
6112 for (s, t, n) in [(3usize, 3usize, 6usize), (3, 4, 9)] {
6113 let (cnf, _) = crate::families::ramsey(s, t, n);
6114 let t0 = std::time::Instant::now();
6115 let fast = solve_structured(cnf.num_vars, &cnf.clauses);
6116 let fast_ms = t0.elapsed().as_millis();
6117 assert!(matches!(fast.answer, Answer::Unsat), "ramsey({s},{t};{n}) is UNSAT");
6118 let t1 = std::time::Instant::now();
6119 let full = solve_comprehensive(cnf.num_vars, &cnf.clauses);
6120 let full_ms = t1.elapsed().as_millis();
6121 assert!(matches!(full.answer, Answer::Unsat), "ramsey({s},{t};{n}) is UNSAT (arsenal)");
6122 eprintln!(
6123 "RAMSEY | ({s},{t};{n}) [{} vars]: fast={:?} {}ms {} conflicts | arsenal={:?} {}ms {} conflicts",
6124 cnf.num_vars, fast.via, fast_ms, fast.conflicts, full.via, full_ms, full.conflicts
6125 );
6126 }
6127 }
6128}