use std::collections::HashMap;
use std::collections::HashSet;
use crate::cdcl::{BudgetedResult, Lit, SolveResult, Solver};
use crate::lyapunov::{auto_collapse, extract_xor, AutoCollapse};
use crate::proof::ProofStep;
use crate::xor_engine::IncXor;
use crate::xorsat::XorOutcome;
use crate::ProofExpr;
#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub enum Route {
TwoSat,
Horn,
Lll,
Pigeonhole,
CuttingPlanes,
Parity,
ExactCover,
ModP,
ModM,
Collapse,
HybridXor,
Sos,
Nullstellensatz,
SymmetryBreak,
NestedSymmetry,
Sel,
LocalSymmetry,
OrbitalBranch,
SymmetricProbe,
SymmetricBinary,
OrbitWeightQuotient,
SymmetryPropagate,
SymmetricComponent,
SymmetrySimplify,
SemanticSymmetry,
AlmostSymmetry,
DeclaredSymmetry,
RecursiveBreak,
Incompressible,
Component,
BoundedVarElim,
EquivLit,
TreeWidth,
Cdcl,
}
#[derive(Clone, Debug)]
pub enum Answer {
Sat(Vec<bool>),
Unsat,
}
#[derive(Clone, Debug)]
pub struct Solved {
pub answer: Answer,
pub via: Route,
pub proof: Vec<ProofStep>,
pub conflicts: u64,
}
impl Solved {
fn unsat(via: Route) -> Self {
Solved { answer: Answer::Unsat, via, proof: Vec::new(), conflicts: 0 }
}
}
pub fn solve_structured(num_vars: usize, clauses: &[Vec<Lit>]) -> Solved {
structured_prefix(num_vars, clauses).unwrap_or_else(|| cdcl_fallback(num_vars, clauses))
}
pub fn structured_prefix(num_vars: usize, clauses: &[Vec<Lit>]) -> Option<Solved> {
if let Some(binary) = as_two_sat(clauses) {
return Some(match crate::twosat::solve(&binary, num_vars) {
crate::twosat::TwoSatOutcome::Sat(model) => {
Solved { answer: Answer::Sat(model), via: Route::TwoSat, proof: Vec::new(), conflicts: 0 }
}
crate::twosat::TwoSatOutcome::Unsat(_) => Solved::unsat(Route::TwoSat),
});
}
if let Some(horn) = as_horn(clauses) {
return Some(match crate::hornsat::solve(&horn, num_vars) {
crate::hornsat::HornOutcome::Sat(model) => {
Solved { answer: Answer::Sat(model), via: Route::Horn, proof: Vec::new(), conflicts: 0 }
}
crate::hornsat::HornOutcome::Unsat(_) => Solved::unsat(Route::Horn),
});
}
if !clauses.is_empty() && crate::lll::lll_certifies_sat(clauses).is_some() {
let budget = 1000 + 64 * clauses.len();
if let Some(model) = crate::lll::moser_tardos_witness(num_vars, clauses, 0x10C0_5EED_C0DE_F00D, budget)
{
if clauses
.iter()
.all(|c| c.iter().any(|l| model.get(l.var() as usize).copied().unwrap_or(false) == l.is_positive()))
{
return Some(Solved { answer: Answer::Sat(model), via: Route::Lll, proof: Vec::new(), conflicts: 0 });
}
}
}
if let Some(expr) = cnf_to_expr(clauses) {
if crate::pigeonhole::decide_pigeonhole_unsat(&expr) {
return Some(Solved::unsat(Route::Pigeonhole));
}
if crate::pseudo_boolean::refute_clausal(&expr) {
return Some(Solved::unsat(Route::CuttingPlanes));
}
if crate::xorsat::refute_via_parity(&expr) {
return Some(Solved::unsat(Route::Parity));
}
}
if let Some(solved) = exact_cover_route(num_vars, clauses) {
return Some(solved);
}
if let Some(solved) = modp_route(num_vars, clauses) {
return Some(solved);
}
match auto_collapse(num_vars, clauses) {
AutoCollapse::None => {}
_ => return Some(Solved::unsat(Route::Collapse)),
}
if let Some(solved) = hybrid_xor(num_vars, clauses) {
return Some(solved);
}
if num_vars <= 6 && crate::sos::sos_refutes(num_vars, clauses) {
return Some(Solved::unsat(Route::Sos));
}
if num_vars <= 12 {
for d in 2..=num_vars.min(3) {
if crate::polycalc::nullstellensatz_refutes(num_vars, clauses, d) {
return Some(Solved::unsat(Route::Nullstellensatz));
}
}
}
None
}
fn exact_cover_route(num_vars: usize, clauses: &[Vec<Lit>]) -> Option<Solved> {
use std::collections::HashSet;
let mut amo: HashSet<(u32, u32)> = HashSet::new();
for c in clauses {
if c.len() == 2 && c.iter().all(|l| !l.is_positive()) {
let (a, b) = (c[0].var(), c[1].var());
amo.insert((a.min(b), a.max(b)));
}
}
if amo.is_empty() {
return None;
}
let mut groups: Vec<Vec<u32>> = Vec::new();
for c in clauses {
if c.len() < 2 || !c.iter().all(|l| l.is_positive()) {
continue;
}
let mut g: Vec<u32> = c.iter().map(|l| l.var()).collect();
g.sort_unstable();
g.dedup();
if g.len() != c.len() {
continue;
}
let full_amo = (0..g.len())
.all(|i| (i + 1..g.len()).all(|j| amo.contains(&(g[i], g[j]))));
if full_amo {
groups.push(g);
}
}
if groups.len() < 2 {
return None; }
let eqs: Vec<crate::xorsat::XorEquation> = groups
.iter()
.map(|g| crate::xorsat::XorEquation::new(g.iter().map(|&v| v as usize).collect::<Vec<_>>(), true))
.collect();
if let crate::xorsat::XorOutcome::Unsat(refutation) = crate::xorsat::solve(&eqs, num_vars) {
if crate::xorsat::is_refutation(&eqs, num_vars, &refutation) {
return Some(Solved::unsat(Route::ExactCover));
}
}
for p in [3u64, 5] {
let meqs: Vec<crate::modp::ModpEquation> = groups
.iter()
.map(|g| {
crate::modp::ModpEquation::new(
g.iter().map(|&v| (v as usize, 1u64)).collect::<Vec<_>>(),
1,
)
})
.collect();
if let crate::modp::ModpOutcome::Unsat(combo) = crate::modp::solve(&meqs, num_vars, p) {
if crate::modp::is_refutation(&meqs, num_vars, p, &combo) {
return Some(Solved::unsat(Route::ExactCover));
}
}
}
None
}
fn cdcl_fallback(num_vars: usize, clauses: &[Vec<Lit>]) -> Solved {
let mut solver = Solver::new(num_vars);
for c in clauses {
solver.add_clause(c.clone());
}
for c in mine_clauses(num_vars, clauses) {
solver.add_clause(c);
}
match solver.solve() {
SolveResult::Sat(model) => {
Solved { answer: Answer::Sat(model), via: Route::Cdcl, proof: Vec::new(), conflicts: solver.conflicts() }
}
SolveResult::Unsat => {
let proof = solver.learned().iter().map(|lc| ProofStep::Rup(lc.lits.clone())).collect();
Solved { answer: Answer::Unsat, via: Route::Cdcl, proof, conflicts: solver.conflicts() }
}
}
}
pub fn solve_comprehensive(num_vars: usize, clauses: &[Vec<Lit>]) -> Solved {
if let Some(s) = structured_prefix(num_vars, clauses) {
return s;
}
if let crate::inprocess::EquivResult::Unsat(steps) = crate::inprocess::equivalent_literal_scc(num_vars, clauses) {
return Solved { answer: Answer::Unsat, via: Route::EquivLit, proof: steps, conflicts: 0 };
}
let (reduced, steps) = crate::inprocess::bve(num_vars, clauses);
if reduced.iter().any(|c| c.is_empty()) {
return Solved { answer: Answer::Unsat, via: Route::BoundedVarElim, proof: steps, conflicts: 0 };
}
if let Some(steps) = crate::inprocess::bucket_elimination_refute(num_vars, clauses, 12) {
return Solved { answer: Answer::Unsat, via: Route::TreeWidth, proof: steps, conflicts: 0 };
}
if crate::ait::incompressibility_gate(num_vars, clauses).is_some() {
let mut solved = cdcl_fallback(num_vars, clauses);
solved.via = Route::Incompressible;
return solved;
}
if let Some(s) = symmetric_component_solve(num_vars, clauses) {
return s;
}
if let Some(s) = symmetry_via_simplification_solve(num_vars, clauses) {
return s;
}
if let Some(s) = orbit_weight_quotient_solve(num_vars, clauses) {
return s;
}
if num_vars <= 16 {
for d in 2..=num_vars.min(3) {
if crate::polycalc::nullstellensatz_refutes(num_vars, clauses, d) {
return Solved::unsat(Route::Nullstellensatz);
}
}
}
if let Some(s) = dynamic_sel(num_vars, clauses) {
return s;
}
if let Some(s) = symmetric_probe_solve(num_vars, clauses) {
return s;
}
if let Some(s) = symmetric_binary_inference_solve(num_vars, clauses) {
return s;
}
if let Some(s) = nested_symmetry_solve(num_vars, clauses) {
return s;
}
if let Some(s) = orbital_branch_solve(num_vars, clauses) {
return s;
}
if let Some(s) = symmetry_propagate_solve(num_vars, clauses) {
return s;
}
if let Some(s) = symmetry_break_solve(num_vars, clauses) {
return s;
}
if let Some(s) = local_symmetry_solve(num_vars, clauses) {
return s;
}
if let Some(s) = semantic_symmetry_solve(num_vars, clauses) {
return s;
}
if let Some(s) = almost_symmetry_solve(num_vars, clauses) {
return s;
}
if let Some(s) = recursive_break_solve(num_vars, clauses) {
return s;
}
if let Some(s) = fused_modular_solve(num_vars, clauses) {
return s;
}
match crate::affine::affine_canonicalize(num_vars, clauses) {
crate::affine::AffineCanon::Refuted(drat) => {
let proof = drat.map(|res| res.into_iter().map(ProofStep::Rup).collect()).unwrap_or_default();
return Solved { answer: Answer::Unsat, via: Route::Parity, proof, conflicts: 0 };
}
crate::affine::AffineCanon::Canonical(canon) => {
let sub = cdcl_fallback(canon.num_vars, &canon.clauses);
return match sub.answer {
Answer::Unsat => Solved { answer: Answer::Unsat, via: sub.via, proof: Vec::new(), conflicts: sub.conflicts },
Answer::Sat(model) => {
let lifted = canon.lift(&model);
if clauses.iter().all(|c| c.iter().any(|l| lifted[l.var() as usize] == l.is_positive())) {
Solved { answer: Answer::Sat(lifted), via: sub.via, proof: Vec::new(), conflicts: sub.conflicts }
} else {
cdcl_fallback(num_vars, clauses) }
}
};
}
crate::affine::AffineCanon::Unchanged => {}
}
match crate::affine_gfp::affine_p_canonicalize(num_vars, clauses) {
crate::affine_gfp::AffinePCanon::Refuted(drat) => {
let proof = drat.map(|res| res.into_iter().map(ProofStep::Rup).collect()).unwrap_or_default();
return Solved { answer: Answer::Unsat, via: Route::ModP, proof, conflicts: 0 };
}
crate::affine_gfp::AffinePCanon::Canonical(canon) => {
let sub = cdcl_fallback(canon.num_vars, &canon.clauses);
return match sub.answer {
Answer::Unsat => Solved { answer: Answer::Unsat, via: sub.via, proof: Vec::new(), conflicts: sub.conflicts },
Answer::Sat(model) => {
let lifted = canon.lift(&model);
if clauses.iter().all(|c| c.iter().any(|l| lifted[l.var() as usize] == l.is_positive())) {
Solved { answer: Answer::Sat(lifted), via: sub.via, proof: Vec::new(), conflicts: sub.conflicts }
} else {
cdcl_fallback(num_vars, clauses) }
}
};
}
crate::affine_gfp::AffinePCanon::Unchanged => {}
}
match crate::affine_gfp::affine_m_canonicalize(num_vars, clauses) {
crate::affine_gfp::AffinePCanon::Refuted(drat) => {
let proof = drat.map(|res| res.into_iter().map(ProofStep::Rup).collect()).unwrap_or_default();
return Solved { answer: Answer::Unsat, via: Route::ModM, proof, conflicts: 0 };
}
crate::affine_gfp::AffinePCanon::Canonical(canon) => {
let sub = cdcl_fallback(canon.num_vars, &canon.clauses);
return match sub.answer {
Answer::Unsat => Solved { answer: Answer::Unsat, via: sub.via, proof: Vec::new(), conflicts: sub.conflicts },
Answer::Sat(model) => {
let lifted = canon.lift(&model);
if clauses.iter().all(|c| c.iter().any(|l| lifted[l.var() as usize] == l.is_positive())) {
Solved { answer: Answer::Sat(lifted), via: sub.via, proof: Vec::new(), conflicts: sub.conflicts }
} else {
cdcl_fallback(num_vars, clauses) }
}
};
}
crate::affine_gfp::AffinePCanon::Unchanged => {}
}
if let Some(s) = component_solve(num_vars, clauses) {
return s;
}
cdcl_fallback(num_vars, clauses)
}
fn recursive_break_solve(num_vars: usize, clauses: &[Vec<Lit>]) -> Option<Solved> {
if num_vars == 0 || num_vars > 64 {
return None;
}
let broken = break_all_symmetry(num_vars, clauses);
if broken.len() == clauses.len() {
return None; }
let mut solver = Solver::new(num_vars);
for c in &broken {
solver.add_clause(c.clone());
}
match solver.solve() {
SolveResult::Sat(model) => {
let projected: Vec<bool> = model[..num_vars].to_vec();
clauses
.iter()
.all(|c| c.iter().any(|l| projected[l.var() as usize] == l.is_positive()))
.then_some(Solved {
answer: Answer::Sat(projected),
via: Route::RecursiveBreak,
proof: Vec::new(),
conflicts: solver.conflicts(),
})
}
SolveResult::Unsat => {
Some(Solved { answer: Answer::Unsat, via: Route::RecursiveBreak, proof: Vec::new(), conflicts: solver.conflicts() })
}
}
}
fn local_symmetry_solve(num_vars: usize, clauses: &[Vec<Lit>]) -> Option<Solved> {
if num_vars == 0 || num_vars > 24 {
return None;
}
let fixed_gens = |lit: Lit| -> Vec<Vec<Lit>> {
let v = lit.var() as usize;
crate::sym_break::conditional_symmetry_generators(num_vars, clauses, &[lit])
.into_iter()
.filter(|img| img[v] == Lit::pos(v as u32))
.collect()
};
let mut best: Option<usize> = None;
let mut best_score = 0usize;
for v in 0..num_vars {
let score = fixed_gens(Lit::pos(v as u32)).len() + fixed_gens(Lit::neg(v as u32)).len();
if score > best_score {
best_score = score;
best = Some(v);
}
}
let v = best?;
let mut conflicts = 0u64;
for polarity in [false, true] {
let lit = Lit::new(v as u32, polarity);
let (sbp, total) = crate::sym_break::lex_leader_sbp_lit(num_vars, &fixed_gens(lit));
let mut solver = Solver::new(total.max(num_vars));
for c in clauses {
solver.add_clause(c.clone());
}
solver.add_clause(vec![lit]); for c in &sbp {
solver.add_clause(c.clone());
}
match solver.solve() {
SolveResult::Sat(model) => {
return Some(Solved {
answer: Answer::Sat(model[..num_vars].to_vec()),
via: Route::LocalSymmetry,
proof: Vec::new(),
conflicts: conflicts + solver.conflicts(),
});
}
SolveResult::Unsat => conflicts += solver.conflicts(),
}
}
Some(Solved { answer: Answer::Unsat, via: Route::LocalSymmetry, proof: Vec::new(), conflicts })
}
fn dynamic_sel(num_vars: usize, clauses: &[Vec<Lit>]) -> Option<Solved> {
use crate::sym_dynamic::{sel_refute, SelOutcome};
if num_vars > 64 || crate::sym_break::literal_automorphism_generators(num_vars, clauses).is_empty() {
return None;
}
match sel_refute(num_vars, clauses) {
SelOutcome::Unsat { steps, conflicts, .. } => {
Some(Solved { answer: Answer::Unsat, via: Route::Sel, proof: steps, conflicts })
}
SelOutcome::Sat(model) => {
Some(Solved { answer: Answer::Sat(model), via: Route::Sel, proof: Vec::new(), conflicts: 0 })
}
SelOutcome::Unknown { .. } => None,
}
}
fn symmetry_break_solve(num_vars: usize, clauses: &[Vec<Lit>]) -> Option<Solved> {
if num_vars > 64 {
return None; }
let gens = crate::sym_break::literal_automorphism_generators(num_vars, clauses);
if gens.is_empty() {
return None; }
let point_gens: Vec<_> =
gens.iter().map(|s| crate::sym_break::litsym_to_points(s, num_vars)).collect();
let bsgs = crate::permgroup::schreier_sims(2 * num_vars, &point_gens);
if bsgs.order() <= 1 {
return None;
}
let (sbp, total) = match bsgs.elements(50_000) {
Some(pts) => crate::sym_break::lex_leader_sbp_lit(
num_vars,
&pts.iter().map(|p| crate::sym_break::litsym_from_points(p, num_vars)).collect::<Vec<_>>(),
),
None => crate::sym_break::hierarchical_break(num_vars, clauses).unwrap_or_else(|| {
let mut s = gens;
s.extend(
bsgs.transversal_elements().iter().map(|p| crate::sym_break::litsym_from_points(p, num_vars)),
);
crate::sym_break::lex_leader_sbp_lit(num_vars, &s)
}),
};
let mut solver = Solver::new(total);
for c in clauses {
solver.add_clause(c.clone());
}
for c in &sbp {
solver.add_clause(c.clone());
}
match solver.solve() {
SolveResult::Sat(model) => {
let projected: Vec<bool> = model[..num_vars].to_vec();
clauses
.iter()
.all(|c| c.iter().any(|l| projected[l.var() as usize] == l.is_positive()))
.then_some(Solved {
answer: Answer::Sat(projected),
via: Route::SymmetryBreak,
proof: Vec::new(),
conflicts: solver.conflicts(),
})
}
SolveResult::Unsat => Some(Solved::unsat(Route::SymmetryBreak)),
}
}
fn orbital_branch_solve(num_vars: usize, clauses: &[Vec<Lit>]) -> Option<Solved> {
if num_vars == 0 || num_vars > 64 {
return None;
}
let gens = crate::sym_break::variable_automorphism_generators(num_vars, clauses)?;
if gens.is_empty() {
return None;
}
if !crate::permgroup::orbits(num_vars, &gens).iter().any(|o| o.len() >= 3) {
return None;
}
let mut conflicts = 0u64;
let mut budget = 1024u64; let answer = orbital_node(num_vars, clauses, &gens, &mut Vec::new(), &mut budget, &mut conflicts)?;
Some(Solved { answer, via: Route::OrbitalBranch, proof: Vec::new(), conflicts })
}
fn orbital_node(
num_vars: usize,
clauses: &[Vec<Lit>],
gens: &[crate::permgroup::Perm],
committed: &mut Vec<Lit>,
budget: &mut u64,
conflicts: &mut u64,
) -> Option<Answer> {
let checked = |m: Vec<bool>| -> Option<Answer> {
clauses
.iter()
.all(|c| c.iter().any(|l| m[l.var() as usize] == l.is_positive()))
.then_some(Answer::Sat(m))
};
let committed_vars: HashSet<usize> = committed.iter().map(|l| l.var() as usize).collect();
let live: Vec<crate::permgroup::Perm> = if committed_vars.is_empty() {
gens.to_vec()
} else {
gens.iter().filter(|g| committed_vars.iter().all(|&v| g[v] == v)).cloned().collect()
};
let orbit = (*budget > 0)
.then(|| {
crate::permgroup::orbits(num_vars, &live)
.into_iter()
.filter(|o| o.len() >= 2 && o.iter().all(|v| !committed_vars.contains(v)))
.max_by_key(|o| o.len())
})
.flatten();
let orbit = match orbit {
Some(o) => o,
None => return solve_residual(num_vars, clauses, committed, conflicts), };
*budget -= 1;
let rep = orbit[0];
committed.push(Lit::pos(rep as u32));
let a = orbital_node(num_vars, clauses, gens, committed, budget, conflicts);
committed.pop();
match a {
Some(Answer::Sat(m)) => return checked(m),
None => return None, Some(Answer::Unsat) => {}
}
let n0 = committed.len();
committed.extend(orbit.iter().map(|&v| Lit::neg(v as u32)));
let b = orbital_node(num_vars, clauses, gens, committed, budget, conflicts);
committed.truncate(n0);
match b {
Some(Answer::Sat(m)) => checked(m),
Some(Answer::Unsat) => Some(Answer::Unsat), None => None,
}
}
fn solve_residual(
num_vars: usize,
clauses: &[Vec<Lit>],
committed: &[Lit],
conflicts: &mut u64,
) -> Option<Answer> {
let mut s = Solver::new(num_vars);
for c in clauses {
s.add_clause(c.clone());
}
for &l in committed {
s.add_clause(vec![l]);
}
let r = s.solve();
*conflicts += s.conflicts();
Some(match r {
SolveResult::Sat(model) => Answer::Sat(model[..num_vars].to_vec()),
SolveResult::Unsat => Answer::Unsat,
})
}
fn symmetric_probe_solve(num_vars: usize, clauses: &[Vec<Lit>]) -> Option<Solved> {
if num_vars == 0 || num_vars > 64 {
return None;
}
let gens = crate::sym_break::literal_automorphism_generators(num_vars, clauses);
if gens.is_empty() {
return None;
}
let point_gens: Vec<_> =
gens.iter().map(|s| crate::sym_break::litsym_to_points(s, num_vars)).collect();
let lit_orbits = crate::permgroup::orbits(2 * num_vars, &point_gens);
let point_to_lit = |p: usize| Lit::new((p / 2) as u32, p % 2 == 0);
const PROBE_BUDGET: u64 = 200;
let probe_fails = |lit: Lit| -> bool {
let mut s = Solver::new(num_vars);
for c in clauses {
s.add_clause(c.clone());
}
s.add_clause(vec![lit]);
matches!(s.solve_budgeted(PROBE_BUDGET), BudgetedResult::Unsat)
};
let mut forced: Vec<Lit> = Vec::new();
for orbit in &lit_orbits {
if orbit.len() < 2 {
continue;
}
if probe_fails(point_to_lit(orbit[0])) {
forced.extend(orbit.iter().map(|&p| point_to_lit(p).negated()));
}
}
if forced.is_empty() {
return None; }
let mut solver = Solver::new(num_vars);
for c in clauses {
solver.add_clause(c.clone());
}
for &l in &forced {
solver.add_clause(vec![l]);
}
let r = solver.solve();
let conflicts = solver.conflicts();
match r {
SolveResult::Sat(model) => {
let projected: Vec<bool> = model[..num_vars].to_vec();
clauses
.iter()
.all(|c| c.iter().any(|l| projected[l.var() as usize] == l.is_positive()))
.then_some(Solved {
answer: Answer::Sat(projected),
via: Route::SymmetricProbe,
proof: Vec::new(),
conflicts,
})
}
SolveResult::Unsat => {
Some(Solved { answer: Answer::Unsat, via: Route::SymmetricProbe, proof: Vec::new(), conflicts })
}
}
}
fn bcp_forced(num_vars: usize, clauses: &[Vec<Lit>], assume: Lit) -> Option<Vec<Lit>> {
let mut val: Vec<Option<bool>> = vec![None; num_vars];
val[assume.var() as usize] = Some(assume.is_positive());
let mut forced = vec![assume];
loop {
let mut changed = false;
for c in clauses {
let mut sat = false;
let mut unassigned: Option<Lit> = None;
let mut count = 0;
for &l in c {
match val[l.var() as usize] {
Some(b) if b == l.is_positive() => {
sat = true;
break;
}
Some(_) => {}
None => {
count += 1;
unassigned = Some(l);
}
}
}
if sat {
continue;
}
if count == 0 {
return None; }
if count == 1 {
let u = unassigned.unwrap();
val[u.var() as usize] = Some(u.is_positive());
forced.push(u);
changed = true;
}
}
if !changed {
break;
}
}
Some(forced)
}
fn symmetric_binary_inference_solve(num_vars: usize, clauses: &[Vec<Lit>]) -> Option<Solved> {
if num_vars == 0 || num_vars > 64 {
return None;
}
let gens = crate::sym_break::variable_automorphism_generators(num_vars, clauses)?;
if gens.is_empty() {
return None;
}
let key2 = |a: Lit, b: Lit| -> [(u32, bool); 2] {
let mut k = [(a.var(), a.is_positive()), (b.var(), b.is_positive())];
k.sort_unstable();
k
};
let lit_apply = |g: &[usize], l: Lit| Lit::new(g[l.var() as usize] as u32, l.is_positive());
let mut seen: HashSet<[(u32, bool); 2]> =
clauses.iter().filter(|c| c.len() == 2).map(|c| key2(c[0], c[1])).collect();
const CAP: usize = 4096;
let mut new_bins: Vec<Vec<Lit>> = Vec::new();
'outer: for orbit in crate::permgroup::orbits(num_vars, &gens) {
let v = orbit[0];
for pol in [false, true] {
let lit = Lit::new(v as u32, pol);
let Some(forced) = bcp_forced(num_vars, clauses, lit) else {
continue; };
for &m in &forced {
if m.var() == lit.var() {
continue;
}
let mut local: HashSet<[(u32, bool); 2]> = HashSet::new();
let mut stack = vec![(lit.negated(), m)];
while let Some((a, b)) = stack.pop() {
if a.var() == b.var() {
continue;
}
let k = key2(a, b);
if !local.insert(k) {
continue;
}
if seen.insert(k) {
new_bins.push(vec![a, b]);
if new_bins.len() >= CAP {
break 'outer;
}
}
for g in &gens {
stack.push((lit_apply(g, a), lit_apply(g, b)));
}
}
}
}
}
if new_bins.is_empty() {
return None; }
let mut solver = Solver::new(num_vars);
for c in clauses {
solver.add_clause(c.clone());
}
for c in &new_bins {
solver.add_clause(c.clone());
}
let r = solver.solve();
let conflicts = solver.conflicts();
match r {
SolveResult::Sat(model) => {
let projected: Vec<bool> = model[..num_vars].to_vec();
clauses
.iter()
.all(|c| c.iter().any(|l| projected[l.var() as usize] == l.is_positive()))
.then_some(Solved {
answer: Answer::Sat(projected),
via: Route::SymmetricBinary,
proof: Vec::new(),
conflicts,
})
}
SolveResult::Unsat => {
Some(Solved { answer: Answer::Unsat, via: Route::SymmetricBinary, proof: Vec::new(), conflicts })
}
}
}
fn orbit_weight_quotient_solve(num_vars: usize, clauses: &[Vec<Lit>]) -> Option<Solved> {
if num_vars == 0 || num_vars > 64 {
return None;
}
let gens = crate::sym_break::variable_automorphism_generators(num_vars, clauses)?;
if gens.is_empty() {
return None;
}
let orbits = crate::permgroup::orbits(num_vars, &gens);
let bsgs = crate::permgroup::schreier_sims(num_vars, &gens);
for orbit in &orbits {
for w in orbit.windows(2) {
let mut t: Vec<usize> = (0..num_vars).collect();
t.swap(w[0], w[1]);
if !bsgs.contains(&t) {
return None; }
}
}
let mut num_reps: u128 = 1;
for o in &orbits {
num_reps = num_reps.saturating_mul(o.len() as u128 + 1);
}
if num_reps > 200_000 || num_reps >= (1u128 << num_vars) {
return None;
}
let dims: Vec<usize> = orbits.iter().map(|o| o.len() + 1).collect();
let total = num_reps as usize;
let satisfies = |a: &[bool]| -> bool {
clauses.iter().all(|c| c.iter().any(|l| a[l.var() as usize] == l.is_positive()))
};
for idx in 0..total {
let mut rem = idx;
let mut assign = vec![false; num_vars];
for (oi, orbit) in orbits.iter().enumerate() {
let w = rem % dims[oi];
rem /= dims[oi];
for &v in orbit.iter().take(w) {
assign[v] = true;
}
}
if satisfies(&assign) {
return Some(Solved {
answer: Answer::Sat(assign),
via: Route::OrbitWeightQuotient,
proof: Vec::new(),
conflicts: 0,
});
}
}
Some(Solved::unsat(Route::OrbitWeightQuotient))
}
struct LexLeaderTheory {
num_vars: usize,
generators: Vec<crate::permgroup::Perm>,
}
impl crate::cdcl::Theory for LexLeaderTheory {
fn propagate(&mut self, trail: &[Lit]) -> Vec<Vec<Lit>> {
let mut val: Vec<Option<bool>> = vec![None; self.num_vars];
for &l in trail {
let v = l.var() as usize;
if v < self.num_vars {
val[v] = Some(l.is_positive());
}
}
let actionable = |c: &[Lit]| -> bool {
let mut unassigned = 0;
for &lit in c {
match val[lit.var() as usize] {
Some(b) if b == lit.is_positive() => return false, Some(_) => {}
None => unassigned += 1,
}
}
unassigned <= 1
};
let mut out: Vec<Vec<Lit>> = Vec::new();
for g in &self.generators {
let mut prefix: Vec<Lit> = Vec::new();
for j in 0..self.num_vars {
let k = g[j];
if k == j {
continue; }
match (val[j], val[k]) {
(Some(a), Some(b)) if a == b => {
prefix.push(Lit::new(j as u32, !a));
prefix.push(Lit::new(k as u32, !b));
}
_ => {
let mut c = prefix.clone();
c.push(Lit::new(j as u32, false)); c.push(Lit::new(k as u32, true)); if actionable(&c) {
out.push(c);
}
break;
}
}
}
}
out
}
}
fn symmetry_propagate_solve(num_vars: usize, clauses: &[Vec<Lit>]) -> Option<Solved> {
if num_vars == 0 || num_vars > 64 {
return None;
}
let gens = crate::sym_break::variable_automorphism_generators(num_vars, clauses)?;
if gens.is_empty() {
return None;
}
let mut solver = Solver::new(num_vars);
for c in clauses {
solver.add_clause(c.clone());
}
let mut theories: Vec<Box<dyn crate::cdcl::Theory>> =
vec![Box::new(LexLeaderTheory { num_vars, generators: gens })];
match solver.solve_with(&mut theories) {
SolveResult::Sat(model) => {
let projected: Vec<bool> = model[..num_vars].to_vec();
clauses
.iter()
.all(|c| c.iter().any(|l| projected[l.var() as usize] == l.is_positive()))
.then_some(Solved {
answer: Answer::Sat(projected),
via: Route::SymmetryPropagate,
proof: Vec::new(),
conflicts: solver.conflicts(),
})
}
SolveResult::Unsat => Some(Solved {
answer: Answer::Unsat,
via: Route::SymmetryPropagate,
proof: Vec::new(),
conflicts: solver.conflicts(),
}),
}
}
fn uf_find(parent: &mut [usize], mut x: usize) -> usize {
while parent[x] != x {
parent[x] = parent[parent[x]];
x = parent[x];
}
x
}
fn component_solve(num_vars: usize, clauses: &[Vec<Lit>]) -> Option<Solved> {
if num_vars == 0 || num_vars > 64 || clauses.is_empty() {
return None;
}
let mut parent: Vec<usize> = (0..num_vars).collect();
for c in clauses {
if c.is_empty() {
return Some(Solved::unsat(Route::Component)); }
let r0 = uf_find(&mut parent, c[0].var() as usize);
for l in &c[1..] {
let r = uf_find(&mut parent, l.var() as usize);
parent[r] = r0;
}
}
let mut comp_clauses: Vec<Vec<Vec<Lit>>> = vec![Vec::new(); num_vars];
for c in clauses {
let r = uf_find(&mut parent, c[0].var() as usize);
comp_clauses[r].push(c.clone());
}
let roots: Vec<usize> = (0..num_vars).filter(|&r| !comp_clauses[r].is_empty()).collect();
if roots.len() <= 1 {
return None; }
let mut model = vec![false; num_vars];
let mut conflicts = 0u64;
for &r in &roots {
let sub = solve_comprehensive(num_vars, &comp_clauses[r]);
conflicts += sub.conflicts;
match sub.answer {
Answer::Unsat => {
return Some(Solved { answer: Answer::Unsat, via: Route::Component, proof: Vec::new(), conflicts });
}
Answer::Sat(m) => {
let vars: std::collections::BTreeSet<usize> =
comp_clauses[r].iter().flatten().map(|l| l.var() as usize).collect();
for v in vars {
model[v] = m[v];
}
}
}
}
clauses
.iter()
.all(|c| c.iter().any(|l| model[l.var() as usize] == l.is_positive()))
.then_some(Solved { answer: Answer::Sat(model), via: Route::Component, proof: Vec::new(), conflicts })
}
pub fn solve_by_components(num_vars: usize, clauses: &[Vec<Lit>]) -> Solved {
component_solve(num_vars, clauses).unwrap_or_else(|| cdcl_fallback(num_vars, clauses))
}
fn symmetric_component_solve(num_vars: usize, clauses: &[Vec<Lit>]) -> Option<Solved> {
if num_vars == 0 || num_vars > 64 || clauses.is_empty() {
return None;
}
let mut parent: Vec<usize> = (0..num_vars).collect();
for c in clauses {
if c.is_empty() {
return Some(Solved::unsat(Route::SymmetricComponent)); }
let r0 = uf_find(&mut parent, c[0].var() as usize);
for l in &c[1..] {
let r = uf_find(&mut parent, l.var() as usize);
parent[r] = r0;
}
}
let mut appears = vec![false; num_vars];
for c in clauses {
for l in c {
appears[l.var() as usize] = true;
}
}
let mut comp_vars: Vec<Vec<usize>> = vec![Vec::new(); num_vars];
for v in 0..num_vars {
if appears[v] {
let r = uf_find(&mut parent, v);
comp_vars[r].push(v);
}
}
let roots: Vec<usize> = (0..num_vars).filter(|&r| !comp_vars[r].is_empty()).collect();
if roots.len() <= 1 {
return None; }
let mut comp_clauses: Vec<Vec<Vec<Lit>>> = vec![Vec::new(); num_vars];
for c in clauses {
let r = uf_find(&mut parent, c[0].var() as usize);
comp_clauses[r].push(c.clone());
}
let gens = crate::sym_break::variable_automorphism_generators(num_vars, clauses)?;
if gens.is_empty() {
return None;
}
let identity: Vec<usize> = (0..num_vars).collect();
let mut orbit_of: Vec<Option<usize>> = vec![None; num_vars];
let mut orbits: Vec<Vec<(usize, Vec<usize>)>> = Vec::new();
for &r in &roots {
if orbit_of[r].is_some() {
continue;
}
let oi = orbits.len();
orbit_of[r] = Some(oi);
let mut orbit: Vec<(usize, Vec<usize>)> = vec![(r, identity.clone())];
let mut i = 0;
while i < orbit.len() {
let (cr, perm) = orbit[i].clone();
i += 1;
for g in &gens {
let img_root = uf_find(&mut parent, g[comp_vars[cr][0]]);
if orbit_of[img_root].is_none() {
orbit_of[img_root] = Some(oi);
let new_perm: Vec<usize> = (0..num_vars).map(|v| g[perm[v]]).collect();
orbit.push((img_root, new_perm));
}
}
}
orbits.push(orbit);
}
if !orbits.iter().any(|o| o.len() >= 2) {
return None;
}
let mut model = vec![false; num_vars];
let mut conflicts = 0u64;
for orbit in &orbits {
let rep_root = orbit[0].0;
let solved = solve_comprehensive(num_vars, &comp_clauses[rep_root]);
conflicts += solved.conflicts;
match solved.answer {
Answer::Unsat => {
return Some(Solved {
answer: Answer::Unsat,
via: Route::SymmetricComponent,
proof: Vec::new(),
conflicts,
});
}
Answer::Sat(rep_model) => {
for (_, perm) in orbit {
for &v in &comp_vars[rep_root] {
model[perm[v]] = rep_model[v];
}
}
}
}
}
clauses
.iter()
.all(|c| c.iter().any(|l| model[l.var() as usize] == l.is_positive()))
.then_some(Solved { answer: Answer::Sat(model), via: Route::SymmetricComponent, proof: Vec::new(), conflicts })
}
fn root_propagate(num_vars: usize, clauses: &[Vec<Lit>]) -> Option<(Vec<Lit>, Vec<Vec<Lit>>)> {
let mut val: Vec<Option<bool>> = vec![None; num_vars];
loop {
let mut changed = false;
for c in clauses {
let mut sat = false;
let mut unit: Option<Lit> = None;
let mut count = 0;
for &l in c {
match val[l.var() as usize] {
Some(b) if b == l.is_positive() => {
sat = true;
break;
}
Some(_) => {}
None => {
count += 1;
unit = Some(l);
}
}
}
if sat {
continue;
}
if count == 0 {
return None; }
if count == 1 {
let u = unit.unwrap();
val[u.var() as usize] = Some(u.is_positive());
changed = true;
}
}
if !changed {
break;
}
}
let forced: Vec<Lit> =
(0..num_vars).filter_map(|v| val[v].map(|b| Lit::new(v as u32, b))).collect();
let mut residual: Vec<Vec<Lit>> = Vec::new();
for c in clauses {
let mut sat = false;
let mut shrunk: Vec<Lit> = Vec::new();
for &l in c {
match val[l.var() as usize] {
Some(b) if b == l.is_positive() => {
sat = true;
break;
}
Some(_) => {} None => shrunk.push(l),
}
}
if !sat {
if shrunk.is_empty() {
return None; }
residual.push(shrunk);
}
}
Some((forced, residual))
}
fn symmetry_via_simplification_solve(num_vars: usize, clauses: &[Vec<Lit>]) -> Option<Solved> {
if num_vars == 0 || num_vars > 64 {
return None;
}
let (rho, residual) = match root_propagate(num_vars, clauses) {
None => return Some(Solved::unsat(Route::SymmetrySimplify)), Some(x) => x,
};
if rho.is_empty() {
return None; }
let mut detect = residual.clone();
for &l in &rho {
detect.push(vec![l]);
}
let res_gens = crate::sym_break::variable_automorphism_generators(num_vars, &detect)
.unwrap_or_default();
if res_gens.is_empty() {
return None; }
let raw_set: HashSet<Vec<(u32, bool)>> = clauses
.iter()
.map(|c| {
let mut k: Vec<(u32, bool)> = c.iter().map(|l| (l.var(), l.is_positive())).collect();
k.sort_unstable();
k
})
.collect();
let is_raw_symmetry = |g: &[usize]| -> bool {
clauses.iter().all(|c| {
let mut img: Vec<(u32, bool)> =
c.iter().map(|l| (g[l.var() as usize] as u32, l.is_positive())).collect();
img.sort_unstable();
raw_set.contains(&img)
})
};
if res_gens.iter().all(|g| is_raw_symmetry(g)) {
return None; }
let solved = solve_comprehensive(num_vars, &residual);
match solved.answer {
Answer::Unsat => Some(Solved {
answer: Answer::Unsat,
via: Route::SymmetrySimplify,
proof: Vec::new(),
conflicts: solved.conflicts,
}),
Answer::Sat(mut model) => {
for &l in &rho {
model[l.var() as usize] = l.is_positive();
}
clauses
.iter()
.all(|c| c.iter().any(|l| model[l.var() as usize] == l.is_positive()))
.then_some(Solved {
answer: Answer::Sat(model),
via: Route::SymmetrySimplify,
proof: Vec::new(),
conflicts: solved.conflicts,
})
}
}
}
fn nested_block_tower_break(num_vars: usize, clauses: &[Vec<Lit>]) -> Option<(Vec<Vec<Lit>>, usize)> {
let gens = crate::sym_break::variable_automorphism_generators(num_vars, clauses)?;
if gens.is_empty() {
return None;
}
let bsgs = crate::permgroup::schreier_sims(num_vars, &gens);
let to_litsym = |p: &[usize]| -> Vec<Lit> { (0..num_vars).map(|v| Lit::pos(p[v] as u32)).collect() };
let mut structured: Vec<Vec<Lit>> = Vec::new();
let mut blocks = crate::permgroup::minimal_block_system(num_vars, &gens)?; for _level in 0..num_vars {
let k = blocks.len();
let m = blocks[0].len();
if blocks.iter().any(|b| b.len() != m) {
break; }
for i in 0..k.saturating_sub(1) {
let mut p: Vec<usize> = (0..num_vars).collect();
for j in 0..m {
p[blocks[i][j]] = blocks[i + 1][j];
p[blocks[i + 1][j]] = blocks[i][j];
}
if bsgs.contains(&p) {
structured.push(to_litsym(&p));
}
}
for j in 0..m.saturating_sub(1) {
let mut p: Vec<usize> = (0..num_vars).collect();
for b in &blocks {
p[b[j]] = b[j + 1];
p[b[j + 1]] = b[j];
}
if bsgs.contains(&p) {
structured.push(to_litsym(&p));
}
}
if k <= 1 {
break;
}
let mut block_of = vec![usize::MAX; num_vars];
for (bi, b) in blocks.iter().enumerate() {
for &v in b {
block_of[v] = bi;
}
}
let induced: Vec<Vec<usize>> = gens
.iter()
.map(|g| (0..k).map(|bi| block_of[g[blocks[bi][0]]]).collect())
.collect();
let Some(super_blocks) = crate::permgroup::minimal_block_system(k, &induced) else {
break; };
let mut next: Vec<Vec<usize>> = Vec::new();
for sb in &super_blocks {
let mut nb = Vec::new();
for &bi in sb {
nb.extend_from_slice(&blocks[bi]);
}
next.push(nb);
}
if next.len() >= blocks.len() {
break; }
blocks = next;
}
if structured.is_empty() {
return None;
}
Some(crate::sym_break::lex_leader_sbp_lit(num_vars, &structured))
}
fn nested_symmetry_solve(num_vars: usize, clauses: &[Vec<Lit>]) -> Option<Solved> {
if num_vars == 0 || num_vars > 64 {
return None;
}
let (sbp, total) = nested_block_tower_break(num_vars, clauses)?;
let mut solver = Solver::new(total);
for c in clauses {
solver.add_clause(c.clone());
}
for c in &sbp {
solver.add_clause(c.clone());
}
match solver.solve() {
SolveResult::Sat(model) => {
let projected: Vec<bool> = model[..num_vars].to_vec();
clauses
.iter()
.all(|c| c.iter().any(|l| projected[l.var() as usize] == l.is_positive()))
.then_some(Solved {
answer: Answer::Sat(projected),
via: Route::NestedSymmetry,
proof: Vec::new(),
conflicts: solver.conflicts(),
})
}
SolveResult::Unsat => {
Some(Solved { answer: Answer::Unsat, via: Route::NestedSymmetry, proof: Vec::new(), conflicts: solver.conflicts() })
}
}
}
fn canon_clause(c: &[Lit]) -> Vec<(u32, bool)> {
let mut k: Vec<(u32, bool)> = c.iter().map(|l| (l.var(), l.is_positive())).collect();
k.sort_unstable();
k
}
fn swap_clause_vars(c: &[Lit], a: usize, b: usize) -> Vec<Lit> {
c.iter()
.map(|l| {
let v = l.var() as usize;
let nv = if v == a {
b
} else if v == b {
a
} else {
v
};
Lit::new(nv as u32, l.is_positive())
})
.collect()
}
fn clause_is_implied(num_vars: usize, clauses: &[Vec<Lit>], c: &[Lit]) -> bool {
let mut s = Solver::new(num_vars);
for cl in clauses {
s.add_clause(cl.clone());
}
for &l in c {
s.add_clause(vec![l.negated()]);
}
matches!(s.solve(), SolveResult::Unsat)
}
pub fn semantic_symmetry_pairs(num_vars: usize, clauses: &[Vec<Lit>]) -> (Vec<(usize, usize)>, bool) {
let clause_set: HashSet<Vec<(u32, bool)>> = clauses.iter().map(|c| canon_clause(c)).collect();
let mut pairs = Vec::new();
let mut any_non_syntactic = false;
for a in 0..num_vars {
for b in (a + 1)..num_vars {
let syntactic =
clauses.iter().all(|c| clause_set.contains(&canon_clause(&swap_clause_vars(c, a, b))));
let semantic = syntactic
|| clauses.iter().all(|c| {
let sc = swap_clause_vars(c, a, b);
clause_set.contains(&canon_clause(&sc)) || clause_is_implied(num_vars, clauses, &sc)
});
if semantic {
pairs.push((a, b));
if !syntactic {
any_non_syntactic = true;
}
}
}
}
(pairs, any_non_syntactic)
}
fn semantic_symmetry_solve(num_vars: usize, clauses: &[Vec<Lit>]) -> Option<Solved> {
if num_vars == 0 || num_vars > 20 || clauses.len() > 256 {
return None; }
let (pairs, any_non_syntactic) = semantic_symmetry_pairs(num_vars, clauses);
if pairs.is_empty() || !any_non_syntactic {
return None; }
let gens: Vec<Vec<Lit>> = pairs
.iter()
.map(|&(a, b)| {
(0..num_vars)
.map(|v| {
let img = if v == a {
b
} else if v == b {
a
} else {
v
};
Lit::pos(img as u32)
})
.collect()
})
.collect();
let (sbp, total) = crate::sym_break::lex_leader_sbp_lit(num_vars, &gens);
let mut solver = Solver::new(total);
for c in clauses {
solver.add_clause(c.clone());
}
for c in &sbp {
solver.add_clause(c.clone());
}
match solver.solve() {
SolveResult::Sat(model) => {
let projected: Vec<bool> = model[..num_vars].to_vec();
clauses
.iter()
.all(|c| c.iter().any(|l| projected[l.var() as usize] == l.is_positive()))
.then_some(Solved {
answer: Answer::Sat(projected),
via: Route::SemanticSymmetry,
proof: Vec::new(),
conflicts: solver.conflicts(),
})
}
SolveResult::Unsat => {
Some(Solved { answer: Answer::Unsat, via: Route::SemanticSymmetry, proof: Vec::new(), conflicts: solver.conflicts() })
}
}
}
pub fn almost_symmetry_pairs(
num_vars: usize,
clauses: &[Vec<Lit>],
max_broken: usize,
) -> Vec<(usize, usize, Vec<Vec<Lit>>)> {
let clause_set: HashSet<Vec<(u32, bool)>> = clauses.iter().map(|c| canon_clause(c)).collect();
let mut out = Vec::new();
for a in 0..num_vars {
for b in (a + 1)..num_vars {
let mut images = Vec::new();
for c in clauses {
let sc = swap_clause_vars(c, a, b);
if !clause_set.contains(&canon_clause(&sc)) {
images.push(sc);
}
}
if !images.is_empty() && images.len() <= max_broken {
out.push((a, b, images));
}
}
}
out
}
fn almost_symmetry_solve(num_vars: usize, clauses: &[Vec<Lit>]) -> Option<Solved> {
if num_vars == 0 || num_vars > 20 || clauses.len() > 256 {
return None;
}
let mut pairs = almost_symmetry_pairs(num_vars, clauses, 2);
if pairs.is_empty() {
return None;
}
pairs.sort_by_key(|(_, _, imgs)| imgs.len());
let (a, b, images) = &pairs[0];
let mut aux = num_vars as u32;
let mut extra: Vec<Vec<Lit>> = Vec::new();
let mut guard_neg: Vec<Lit> = Vec::new();
for img in images {
let z = aux;
aux += 1;
for &l in img {
extra.push(vec![l.negated(), Lit::pos(z)]);
}
let mut zc = vec![Lit::neg(z)];
zc.extend(img.iter().copied());
extra.push(zc);
guard_neg.push(Lit::neg(z));
}
let mut guarded = guard_neg;
guarded.push(Lit::neg(*a as u32));
guarded.push(Lit::pos(*b as u32));
extra.push(guarded);
let mut solver = Solver::new(aux as usize);
for c in clauses {
solver.add_clause(c.clone());
}
for c in &extra {
solver.add_clause(c.clone());
}
match solver.solve() {
SolveResult::Sat(model) => {
let projected: Vec<bool> = model[..num_vars].to_vec();
clauses
.iter()
.all(|c| c.iter().any(|l| projected[l.var() as usize] == l.is_positive()))
.then_some(Solved {
answer: Answer::Sat(projected),
via: Route::AlmostSymmetry,
proof: Vec::new(),
conflicts: solver.conflicts(),
})
}
SolveResult::Unsat => {
Some(Solved { answer: Answer::Unsat, via: Route::AlmostSymmetry, proof: Vec::new(), conflicts: solver.conflicts() })
}
}
}
fn apply_perm_to_clause(c: &[Lit], g: &[usize]) -> Vec<Lit> {
c.iter().map(|l| Lit::new(g[l.var() as usize] as u32, l.is_positive())).collect()
}
fn perm_preserves_clause_set(clauses: &[Vec<Lit>], g: &[usize]) -> bool {
let set: HashSet<Vec<(u32, bool)>> = clauses.iter().map(|c| canon_clause(c)).collect();
clauses.iter().all(|c| set.contains(&canon_clause(&apply_perm_to_clause(c, g))))
}
pub fn common_automorphism_generators(
num_vars: usize,
f: &[Vec<Lit>],
s: &[Vec<Lit>],
) -> Vec<crate::permgroup::Perm> {
let mut candidates = crate::sym_break::variable_automorphism_generators(num_vars, f).unwrap_or_default();
candidates.extend(crate::sym_break::variable_automorphism_generators(num_vars, s).unwrap_or_default());
let mut out: Vec<Vec<usize>> = Vec::new();
for g in candidates {
let well_formed = g.len() == num_vars;
let nontrivial = g.iter().enumerate().any(|(i, &x)| i != x);
if well_formed
&& nontrivial
&& perm_preserves_clause_set(f, &g)
&& perm_preserves_clause_set(s, &g)
&& !out.contains(&g)
{
out.push(g);
}
}
out
}
fn clause_orbits(clauses: &[Vec<Lit>], gens: &[crate::permgroup::Perm]) -> Vec<Vec<usize>> {
let index: HashMap<Vec<(u32, bool)>, usize> =
clauses.iter().enumerate().map(|(i, c)| (canon_clause(c), i)).collect();
let n = clauses.len();
let mut parent: Vec<usize> = (0..n).collect();
fn find(parent: &mut [usize], mut x: usize) -> usize {
while parent[x] != x {
parent[x] = parent[parent[x]];
x = parent[x];
}
x
}
for (i, c) in clauses.iter().enumerate() {
for g in gens {
if let Some(&j) = index.get(&canon_clause(&apply_perm_to_clause(c, g))) {
let (a, b) = (find(&mut parent, i), find(&mut parent, j));
parent[a] = b;
}
}
}
let mut groups: std::collections::BTreeMap<usize, Vec<usize>> = std::collections::BTreeMap::new();
for i in 0..n {
let r = find(&mut parent, i);
groups.entry(r).or_default().push(i);
}
groups.into_values().collect()
}
fn entailment_counterexample(num_vars: usize, clauses: &[Vec<Lit>], c: &[Lit]) -> Option<Vec<bool>> {
let mut s = Solver::new(num_vars);
for cl in clauses {
s.add_clause(cl.clone());
}
for &l in c {
s.add_clause(vec![l.negated()]);
}
match s.solve() {
SolveResult::Sat(m) => Some(m),
SolveResult::Unsat => None,
}
}
#[derive(Clone, Debug, PartialEq, Eq)]
pub enum EquivVerdict {
Equivalent,
Differ(Vec<bool>),
}
pub fn equivalent_modulo_symmetry(num_vars: usize, f: &[Vec<Lit>], s: &[Vec<Lit>]) -> EquivVerdict {
let gens = common_automorphism_generators(num_vars, f, s);
for orbit in clause_orbits(s, &gens) {
if let Some(m) = entailment_counterexample(num_vars, f, &s[orbit[0]]) {
return EquivVerdict::Differ(m); }
}
for orbit in clause_orbits(f, &gens) {
if let Some(m) = entailment_counterexample(num_vars, s, &f[orbit[0]]) {
return EquivVerdict::Differ(m);
}
}
EquivVerdict::Equivalent
}
pub fn equivalence_check_counts(num_vars: usize, f: &[Vec<Lit>], s: &[Vec<Lit>]) -> (usize, usize) {
let gens = common_automorphism_generators(num_vars, f, s);
(clause_orbits(s, &gens).len() + clause_orbits(f, &gens).len(), s.len() + f.len())
}
pub fn optimization_symmetry_generators(
num_vars: usize,
clauses: &[Vec<Lit>],
weights: &[i64],
) -> Vec<crate::permgroup::Perm> {
crate::sym_break::variable_automorphism_generators(num_vars, clauses)
.unwrap_or_default()
.into_iter()
.filter(|g| g.len() == num_vars && (0..num_vars).all(|v| weights[g[v]] == weights[v]))
.collect()
}
fn optimization_break(num_vars: usize, clauses: &[Vec<Lit>], weights: &[i64]) -> Vec<Vec<Lit>> {
let mut broken = clauses.to_vec();
for g in optimization_symmetry_generators(num_vars, clauses, weights) {
if let Some(v) = (0..num_vars).find(|&v| g[v] != v) {
broken.push(vec![Lit::new(v as u32, false), Lit::new(g[v] as u32, true)]); }
}
broken
}
fn min_weight_model(num_vars: usize, clauses: &[Vec<Lit>], weights: &[i64]) -> Option<(i64, Vec<bool>, usize)> {
let mut working = clauses.to_vec();
let mut best: Option<(i64, Vec<bool>)> = None;
let mut enumerated = 0usize;
loop {
let mut solver = Solver::new(num_vars);
for c in &working {
solver.add_clause(c.clone());
}
match solver.solve() {
SolveResult::Unsat => break,
SolveResult::Sat(model) => {
enumerated += 1;
let w: i64 = (0..num_vars).filter(|&i| model[i]).map(|i| weights[i]).sum();
if best.as_ref().map_or(true, |(bw, _)| w < *bw) {
best = Some((w, model[..num_vars].to_vec()));
}
working.push((0..num_vars).map(|i| Lit::new(i as u32, !model[i])).collect());
}
}
}
best.map(|(w, m)| (w, m, enumerated))
}
pub fn optimize_modulo_symmetry(
num_vars: usize,
clauses: &[Vec<Lit>],
weights: &[i64],
) -> Option<(i64, Vec<bool>)> {
let broken = optimization_break(num_vars, clauses, weights);
min_weight_model(num_vars, &broken, weights).map(|(w, m, _)| (w, m))
}
pub fn optimize_enumeration_counts(num_vars: usize, clauses: &[Vec<Lit>], weights: &[i64]) -> (usize, usize) {
let broken = optimization_break(num_vars, clauses, weights);
let with = min_weight_model(num_vars, &broken, weights).map_or(0, |(_, _, c)| c);
let without = min_weight_model(num_vars, clauses, weights).map_or(0, |(_, _, c)| c);
(with, without)
}
fn full_assignment_orbit(num_vars: usize, m: &[bool], gens: &[crate::permgroup::Perm]) -> Vec<Vec<bool>> {
let mut seen: HashSet<Vec<bool>> = HashSet::from([m.to_vec()]);
let mut out = vec![m.to_vec()];
let mut i = 0;
while i < out.len() {
let cur = out[i].clone();
i += 1;
for g in gens {
let mut pm = vec![false; num_vars];
for v in 0..num_vars {
pm[g[v]] = cur[v];
}
if seen.insert(pm.clone()) {
out.push(pm);
}
}
}
out
}
pub fn weighted_model_count(num_vars: usize, clauses: &[Vec<Lit>], weight: &[(i64, i64)]) -> i128 {
let gens = crate::sym_break::variable_automorphism_generators(num_vars, clauses).unwrap_or_default();
let weight_of = |m: &[bool]| -> i128 {
(0..num_vars).map(|v| if m[v] { weight[v].1 as i128 } else { weight[v].0 as i128 }).product()
};
let mut working = clauses.to_vec();
let mut z = 0i128;
loop {
let mut solver = Solver::new(num_vars);
for c in &working {
solver.add_clause(c.clone());
}
match solver.solve() {
SolveResult::Unsat => break,
SolveResult::Sat(model) => {
let orbit = full_assignment_orbit(num_vars, &model[..num_vars], &gens);
z += orbit.iter().map(|m| weight_of(m)).sum::<i128>();
for m in &orbit {
working.push((0..num_vars).map(|i| Lit::new(i as u32, !m[i])).collect());
}
}
}
}
z
}
pub fn weighted_model_count_solve_counts(num_vars: usize, clauses: &[Vec<Lit>]) -> (usize, usize) {
let gens = crate::sym_break::variable_automorphism_generators(num_vars, clauses).unwrap_or_default();
let mut working = clauses.to_vec();
let (mut solves, mut models) = (0usize, 0usize);
loop {
let mut solver = Solver::new(num_vars);
for c in &working {
solver.add_clause(c.clone());
}
match solver.solve() {
SolveResult::Unsat => break,
SolveResult::Sat(model) => {
solves += 1;
let orbit = full_assignment_orbit(num_vars, &model[..num_vars], &gens);
models += orbit.len();
for m in &orbit {
working.push((0..num_vars).map(|i| Lit::new(i as u32, !m[i])).collect());
}
}
}
}
(solves, models)
}
fn rank_signatures<S: Ord + Clone>(sigs: &[S]) -> Vec<usize> {
let mut distinct: Vec<S> = sigs.to_vec();
distinct.sort();
distinct.dedup();
sigs.iter().map(|s| distinct.binary_search(s).expect("present")).collect()
}
pub fn color_refinement(num_vars: usize, clauses: &[Vec<Lit>]) -> Vec<usize> {
equitable_refine(num_vars, clauses, &vec![0usize; num_vars])
}
fn equitable_refine(num_vars: usize, clauses: &[Vec<Lit>], var_init: &[usize]) -> Vec<usize> {
let mut var_color = rank_signatures(var_init);
let mut clause_color: Vec<usize> = rank_signatures(&clauses.iter().map(|c| c.len()).collect::<Vec<_>>());
loop {
let clause_sig: Vec<(usize, Vec<(usize, bool)>)> = clauses
.iter()
.enumerate()
.map(|(ci, c)| {
let mut nbrs: Vec<(usize, bool)> =
c.iter().map(|l| (var_color[l.var() as usize], l.is_positive())).collect();
nbrs.sort_unstable();
(clause_color[ci], nbrs)
})
.collect();
let new_clause_color = rank_signatures(&clause_sig);
let mut var_nbrs: Vec<Vec<(usize, bool)>> = vec![Vec::new(); num_vars];
for (ci, c) in clauses.iter().enumerate() {
for l in c {
var_nbrs[l.var() as usize].push((new_clause_color[ci], l.is_positive()));
}
}
for nbrs in var_nbrs.iter_mut() {
nbrs.sort_unstable();
}
let var_sig: Vec<(usize, Vec<(usize, bool)>)> =
(0..num_vars).map(|v| (var_color[v], std::mem::take(&mut var_nbrs[v]))).collect();
let new_var_color = rank_signatures(&var_sig);
if new_var_color == var_color && new_clause_color == clause_color {
break; }
var_color = new_var_color;
clause_color = new_clause_color;
}
var_color
}
pub fn color_refinement_cells(num_vars: usize, clauses: &[Vec<Lit>]) -> usize {
color_refinement(num_vars, clauses).iter().copied().max().map_or(0, |m| m + 1)
}
pub fn provably_asymmetric_variables(num_vars: usize, clauses: &[Vec<Lit>]) -> Vec<usize> {
let cells = color_refinement(num_vars, clauses);
let mut size = vec![0usize; num_vars];
for &c in &cells {
size[c] += 1;
}
(0..num_vars).filter(|&v| size[cells[v]] == 1).collect()
}
fn cooccurrence_matrix(num_vars: usize, clauses: &[Vec<Lit>]) -> Vec<Vec<i64>> {
let mut a = vec![vec![0i64; num_vars]; num_vars];
for c in clauses {
let vars: Vec<usize> = c.iter().map(|l| l.var() as usize).collect();
for &u in &vars {
for &v in &vars {
if u != v {
a[u][v] += 1;
}
}
}
}
a
}
fn equitable_partition_of(num_vars: usize, a: &[Vec<i64>]) -> Vec<usize> {
let mut color = vec![0usize; num_vars];
loop {
let sig: Vec<(usize, Vec<(usize, i64)>)> = (0..num_vars)
.map(|u| {
let mut nbrs: Vec<(usize, i64)> =
(0..num_vars).filter(|&v| a[u][v] != 0).map(|v| (color[v], a[u][v])).collect();
nbrs.sort_unstable();
(color[u], nbrs)
})
.collect();
let next = rank_signatures(&sig);
if next == color {
return color;
}
color = next;
}
}
pub fn fractional_automorphism(num_vars: usize, clauses: &[Vec<Lit>]) -> Vec<usize> {
equitable_partition_of(num_vars, &cooccurrence_matrix(num_vars, clauses))
}
pub fn is_fractional_automorphism(num_vars: usize, clauses: &[Vec<Lit>], partition: &[usize]) -> bool {
let a = cooccurrence_matrix(num_vars, clauses);
let d = partition.iter().copied().max().map_or(0, |m| m + 1);
let mut cell: Vec<Vec<usize>> = vec![Vec::new(); d];
for (v, &c) in partition.iter().enumerate() {
cell[c].push(v);
}
let sum_over = |rows: &[usize], w: usize, by_row: bool| -> i64 {
rows.iter().map(|&x| if by_row { a[x][w] } else { a[w][x] }).sum()
};
for u in 0..num_vars {
for w in 0..num_vars {
let cu = &cell[partition[u]];
let cw = &cell[partition[w]];
let lhs = cw.len() as i64 * sum_over(cu, w, true);
let rhs = cu.len() as i64 * sum_over(cw, u, false);
if lhs != rhs {
return false;
}
}
}
true
}
pub fn two_wl_pair_colors(num_vars: usize, clauses: &[Vec<Lit>]) -> Vec<Vec<usize>> {
let wl1 = color_refinement(num_vars, clauses);
let mut cooc: Vec<Vec<Vec<(usize, bool, bool)>>> = vec![vec![Vec::new(); num_vars]; num_vars];
for c in clauses {
let lits: Vec<(usize, bool)> = c.iter().map(|l| (l.var() as usize, l.is_positive())).collect();
for &(vi, si) in &lits {
for &(vj, sj) in &lits {
if vi != vj {
cooc[vi][vj].push((c.len(), si, sj));
}
}
}
}
for row in cooc.iter_mut() {
for s in row.iter_mut() {
s.sort_unstable();
}
}
let mut flat: Vec<(bool, usize, usize, Vec<(usize, bool, bool)>)> = Vec::with_capacity(num_vars * num_vars);
for i in 0..num_vars {
for j in 0..num_vars {
flat.push((i == j, wl1[i], wl1[j], cooc[i][j].clone()));
}
}
let mut color: Vec<usize> = rank_signatures(&flat); let at = |i: usize, j: usize| i * num_vars + j;
loop {
let mut sig: Vec<(usize, Vec<(usize, usize)>)> = Vec::with_capacity(num_vars * num_vars);
for i in 0..num_vars {
for j in 0..num_vars {
let mut tri: Vec<(usize, usize)> =
(0..num_vars).map(|k| (color[at(i, k)], color[at(k, j)])).collect();
tri.sort_unstable();
sig.push((color[at(i, j)], tri));
}
}
let next = rank_signatures(&sig);
if next == color {
break;
}
color = next;
}
(0..num_vars).map(|i| (0..num_vars).map(|j| color[at(i, j)]).collect()).collect()
}
pub fn two_wl_pair_cells(num_vars: usize, clauses: &[Vec<Lit>]) -> usize {
let c = two_wl_pair_colors(num_vars, clauses);
c.iter().flatten().copied().max().map_or(0, |m| m + 1)
}
pub fn two_wl_fingerprint(num_vars: usize, clauses: &[Vec<Lit>]) -> Vec<usize> {
let c = two_wl_pair_colors(num_vars, clauses);
let k = c.iter().flatten().copied().max().map_or(0, |m| m + 1);
let mut sizes = vec![0usize; k];
for &col in c.iter().flatten() {
sizes[col] += 1;
}
sizes.sort_unstable();
sizes
}
pub fn coherent_configuration_constants(num_vars: usize, clauses: &[Vec<Lit>]) -> Option<(usize, Vec<Vec<Vec<u128>>>)> {
let n = num_vars;
let pc = two_wl_pair_colors(n, clauses);
let d = pc.iter().flatten().copied().max().map_or(0, |m| m + 1);
if d == 0 {
return None;
}
let count_matrix = |x: usize, y: usize| -> Vec<Vec<u128>> {
let mut m = vec![vec![0u128; d]; d];
for z in 0..n {
m[pc[x][z]][pc[z][y]] += 1;
}
m
};
let mut rep: Vec<Option<(usize, usize)>> = vec![None; d];
for i in 0..n {
for j in 0..n {
rep[pc[i][j]].get_or_insert((i, j));
}
}
let mut p = vec![vec![vec![0u128; d]; d]; d];
for k in 0..d {
let (x, y) = rep[k]?;
let m = count_matrix(x, y);
for i in 0..d {
for j in 0..d {
p[i][j][k] = m[i][j];
}
}
}
for x in 0..n {
for y in 0..n {
let k = pc[x][y];
let m = count_matrix(x, y);
for i in 0..d {
for j in 0..d {
if m[i][j] != p[i][j][k] {
return None;
}
}
}
}
}
Some((d, p))
}
pub fn coherent_rank(num_vars: usize, clauses: &[Vec<Lit>]) -> Option<usize> {
coherent_configuration_constants(num_vars, clauses).map(|(d, _)| d)
}
fn gf_simultaneous_eigenvalues(mmats: &[Vec<Vec<u64>>], d: usize, p: u64) -> Option<Vec<Vec<u64>>> {
use crate::permgroup::{gf_mat_vec, gf_nullspace, mod_inv};
let mut subspaces: Vec<Vec<Vec<u64>>> = vec![(0..d)
.map(|i| {
let mut e = vec![0u64; d];
e[i] = 1;
e
})
.collect()];
for mi in mmats {
if subspaces.iter().all(|s| s.len() == 1) {
break;
}
let mut next: Vec<Vec<Vec<u64>>> = Vec::new();
for s in &subspaces {
if s.len() == 1 {
next.push(s.clone());
continue;
}
let bn = s.len();
let mb: Vec<Vec<u64>> = s.iter().map(|b| gf_mat_vec(mi, b, p)).collect();
let mut pieces: Vec<Vec<Vec<u64>>> = Vec::new();
let mut covered = 0usize;
for lam in 0..p {
let mut rows = vec![vec![0u64; bn]; d];
for k in 0..d {
for (jj, sj) in s.iter().enumerate() {
let shift = (lam as u128 * sj[k] as u128) % p as u128;
rows[k][jj] = ((mb[jj][k] as u128 + p as u128 - shift) % p as u128) as u64;
}
}
let ns = gf_nullspace(rows, bn, p);
if ns.is_empty() {
continue;
}
let eig: Vec<Vec<u64>> = ns
.iter()
.map(|c| {
let mut x = vec![0u64; d];
for (jj, &cj) in c.iter().enumerate() {
if cj != 0 {
for k in 0..d {
x[k] = ((x[k] as u128 + cj as u128 * s[jj][k] as u128) % p as u128) as u64;
}
}
}
x
})
.collect();
covered += eig.len();
pieces.push(eig);
if covered == bn {
break;
}
}
if covered == bn {
next.extend(pieces);
} else {
next.push(s.clone());
}
}
subspaces = next;
}
if subspaces.iter().any(|s| s.len() != 1) {
return None; }
Some(
subspaces
.iter()
.map(|s| {
let v = &s[0];
let t = v.iter().position(|&x| x != 0).unwrap();
let inv = mod_inv(v[t], p);
mmats
.iter()
.map(|mi| {
let mv = gf_mat_vec(mi, v, p);
(mv[t] as u128 * inv as u128 % p as u128) as u64
})
.collect()
})
.collect(),
)
}
pub fn association_scheme_eigenmatrix(num_vars: usize, clauses: &[Vec<Lit>]) -> Option<(u64, Vec<Vec<u64>>)> {
let (d, a) = coherent_configuration_constants(num_vars, clauses)?;
if d == 0 {
return None;
}
for i in 0..d {
for j in 0..d {
for k in 0..d {
if a[i][j][k] != a[j][i][k] {
return None;
}
}
}
}
let valency: Vec<u128> = (0..d).map(|i| (0..d).map(|j| a[i][j][0]).sum()).collect();
let mut tried = 0;
let mut p = 2u64;
while tried < 200 && p < 100_000 {
if crate::permgroup::is_prime(p) {
tried += 1;
let mmats: Vec<Vec<Vec<u64>>> = (0..d)
.map(|i| (0..d).map(|k| (0..d).map(|j| (a[i][j][k] % p as u128) as u64).collect()).collect())
.collect();
if let Some(rows) = gf_simultaneous_eigenvalues(&mmats, d, p) {
let hom_ok = rows.iter().all(|row| {
(0..d).all(|i| {
(0..d).all(|j| {
let lhs = row[i] as u128 * row[j] as u128 % p as u128;
let rhs = (0..d)
.map(|k| (a[i][j][k] % p as u128) * row[k] as u128 % p as u128)
.sum::<u128>()
% p as u128;
lhs == rhs
})
})
});
let has_valency =
rows.iter().any(|row| (0..d).all(|i| row[i] as u128 == valency[i] % p as u128));
if hom_ok && has_valency {
return Some((p, rows));
}
}
}
p += 1;
}
None
}
pub fn association_scheme_multiplicities(num_vars: usize, clauses: &[Vec<Lit>]) -> Option<Vec<u128>> {
let (d, a) = coherent_configuration_constants(num_vars, clauses)?;
if d == 0 {
return None;
}
for i in 0..d {
for j in 0..d {
for k in 0..d {
if a[i][j][k] != a[j][i][k] {
return None; }
}
}
}
let valency: Vec<u128> = (0..d).map(|i| (0..d).map(|j| a[i][j][0]).sum()).collect();
let pc = two_wl_pair_colors(num_vars, clauses);
let mut transpose = vec![usize::MAX; d];
for x in 0..num_vars {
for y in 0..num_vars {
let i = pc[x][y];
if transpose[i] == usize::MAX {
transpose[i] = pc[y][x];
}
}
}
let n = num_vars as u128;
let mut tried = 0;
let mut p = 2u64;
while tried < 300 && p < 1_000_000 {
if crate::permgroup::is_prime(p) && p as u128 > n {
tried += 1;
let mmats: Vec<Vec<Vec<u64>>> = (0..d)
.map(|i| (0..d).map(|k| (0..d).map(|j| (a[i][j][k] % p as u128) as u64).collect()).collect())
.collect();
if let Some(rows) = gf_simultaneous_eigenvalues(&mmats, d, p) {
let mut mult = Vec::with_capacity(d);
let mut ok = true;
for row in &rows {
let mut denom = 0u64;
for i in 0..d {
let ki = (valency[i] % p as u128) as u64;
let term = (row[i] as u128 * row[transpose[i]] as u128 % p as u128) as u64;
denom = ((denom as u128 + term as u128 * crate::permgroup::mod_inv(ki, p) as u128)
% p as u128) as u64;
}
if denom == 0 {
ok = false;
break;
}
let m = (n % p as u128) * crate::permgroup::mod_inv(denom, p) as u128 % p as u128;
if m == 0 || m > n {
ok = false;
break;
}
mult.push(m);
}
let trivial_ok = ok
&& rows.iter().zip(&mult).any(|(row, &m)| {
m == 1 && (0..d).all(|i| row[i] as u128 == valency[i] % p as u128)
});
if ok && trivial_ok && mult.iter().sum::<u128>() == n {
mult.sort_unstable();
return Some(mult);
}
}
}
p += 1;
}
None
}
pub fn three_wl_colors(num_vars: usize, clauses: &[Vec<Lit>]) -> Vec<Vec<Vec<usize>>> {
let n = num_vars;
let pc = two_wl_pair_colors(n, clauses);
let at = |i: usize, j: usize, k: usize| (i * n + j) * n + k;
let init: Vec<(usize, usize, usize)> = (0..n)
.flat_map(|i| (0..n).flat_map(move |j| (0..n).map(move |k| (i, j, k))))
.map(|(i, j, k)| (pc[i][j], pc[i][k], pc[j][k]))
.collect();
let mut color = rank_signatures(&init);
loop {
let mut sig: Vec<(usize, Vec<(usize, usize, usize)>)> = Vec::with_capacity(n * n * n);
for i in 0..n {
for j in 0..n {
for k in 0..n {
let mut nbr: Vec<(usize, usize, usize)> =
(0..n).map(|w| (color[at(w, j, k)], color[at(i, w, k)], color[at(i, j, w)])).collect();
nbr.sort_unstable();
sig.push((color[at(i, j, k)], nbr));
}
}
}
let next = rank_signatures(&sig);
if next == color {
break;
}
color = next;
}
(0..n)
.map(|i| (0..n).map(|j| (0..n).map(|k| color[at(i, j, k)]).collect()).collect())
.collect()
}
pub fn three_wl_fingerprint(num_vars: usize, clauses: &[Vec<Lit>]) -> Vec<usize> {
let c = three_wl_colors(num_vars, clauses);
let max = c.iter().flatten().flatten().copied().max().map_or(0, |m| m + 1);
let mut sizes = vec![0usize; max];
for &col in c.iter().flatten().flatten() {
sizes[col] += 1;
}
sizes.sort_unstable();
sizes
}
fn formula_certificate(clauses: &[Vec<Lit>], coloring: &[usize]) -> Vec<Vec<(usize, bool)>> {
let label = rank_signatures(coloring); let mut cls: Vec<Vec<(usize, bool)>> = clauses
.iter()
.map(|c| {
let mut lits: Vec<(usize, bool)> =
c.iter().map(|l| (label[l.var() as usize], l.is_positive())).collect();
lits.sort_unstable();
lits
})
.collect();
cls.sort_unstable();
cls
}
fn ir_canonical(
num_vars: usize,
clauses: &[Vec<Lit>],
colors: &[usize],
nodes: &mut usize,
cap: usize,
) -> Option<Vec<Vec<(usize, bool)>>> {
*nodes += 1;
if *nodes > cap {
return None;
}
let refined = equitable_refine(num_vars, clauses, colors);
let d = refined.iter().copied().max().map_or(0, |m| m + 1);
let mut members: Vec<Vec<usize>> = vec![Vec::new(); d];
for (v, &c) in refined.iter().enumerate() {
members[c].push(v);
}
match (0..d).find(|&c| members[c].len() > 1) {
None => Some(formula_certificate(clauses, &refined)), Some(c) => {
let mut best: Option<Vec<Vec<(usize, bool)>>> = None;
for &v in &members[c] {
let mut nc = refined.clone();
nc[v] = d; let leaf = ir_canonical(num_vars, clauses, &nc, nodes, cap)?;
if best.as_ref().map_or(true, |b| leaf > *b) {
best = Some(leaf);
}
}
best
}
}
}
pub fn canonical_form(num_vars: usize, clauses: &[Vec<Lit>]) -> Option<Vec<Vec<(usize, bool)>>> {
let mut nodes = 0;
ir_canonical(num_vars, clauses, &vec![0usize; num_vars], &mut nodes, 200_000)
}
pub fn formulas_isomorphic(num_vars: usize, f: &[Vec<Lit>], g: &[Vec<Lit>]) -> Option<bool> {
Some(canonical_form(num_vars, f)? == canonical_form(num_vars, g)?)
}
fn is_declared_symmetry(num_vars: usize, clauses: &[Vec<Lit>], g: &[usize]) -> bool {
if g.len() != num_vars {
return false;
}
let mut seen = vec![false; num_vars];
for &x in g {
if x >= num_vars || seen[x] {
return false; }
seen[x] = true;
}
let clause_set: HashSet<Vec<(u32, bool)>> = clauses.iter().map(|c| canon_clause(c)).collect();
let syntactic = clauses.iter().all(|c| clause_set.contains(&canon_clause(&apply_perm_to_clause(c, g))));
syntactic
|| clauses.iter().all(|c| {
let gc = apply_perm_to_clause(c, g);
clause_set.contains(&canon_clause(&gc)) || clause_is_implied(num_vars, clauses, &gc)
})
}
pub fn solve_with_declared_symmetry(
num_vars: usize,
clauses: &[Vec<Lit>],
declared: &[crate::permgroup::Perm],
) -> Solved {
let mut gens = crate::sym_break::variable_automorphism_generators(num_vars, clauses).unwrap_or_default();
for g in declared {
if is_declared_symmetry(num_vars, clauses, g) {
gens.push(g.clone());
}
}
if gens.is_empty() {
return solve_comprehensive(num_vars, clauses);
}
let bsgs = crate::permgroup::schreier_sims(num_vars, &gens);
let to_litsym = |p: &[usize]| -> Vec<Lit> { (0..num_vars).map(|v| Lit::pos(p[v] as u32)).collect() };
let group: Vec<Vec<Lit>> = match bsgs.elements(50_000) {
Some(elts) => elts.iter().map(|p| to_litsym(p)).collect(),
None => gens.iter().map(|p| to_litsym(p)).collect(),
};
let (sbp, total) = crate::sym_break::lex_leader_sbp_lit(num_vars, &group);
let mut solver = Solver::new(total);
for c in clauses {
solver.add_clause(c.clone());
}
for c in &sbp {
solver.add_clause(c.clone());
}
match solver.solve() {
SolveResult::Sat(model) => {
let projected: Vec<bool> = model[..num_vars].to_vec();
if clauses.iter().all(|c| c.iter().any(|l| projected[l.var() as usize] == l.is_positive())) {
Solved { answer: Answer::Sat(projected), via: Route::DeclaredSymmetry, proof: Vec::new(), conflicts: solver.conflicts() }
} else {
solve_comprehensive(num_vars, clauses) }
}
SolveResult::Unsat => {
Solved { answer: Answer::Unsat, via: Route::DeclaredSymmetry, proof: Vec::new(), conflicts: solver.conflicts() }
}
}
}
#[derive(Clone, Debug, PartialEq, Eq)]
pub struct SymmetricCount {
pub representatives: Vec<Vec<bool>>,
pub total_models: u128,
pub exhaustive: bool,
}
fn assignment_orbit(num_vars: usize, m: &[bool], gens: &[crate::permgroup::Perm], occurs: &[usize]) -> Vec<Vec<bool>> {
let proj = |a: &[bool]| -> Vec<bool> { occurs.iter().map(|&v| a[v]).collect() };
let mut seen: HashSet<Vec<bool>> = HashSet::from([proj(m)]);
let mut out = vec![m.to_vec()];
let mut i = 0;
while i < out.len() {
let cur = out[i].clone();
i += 1;
for g in gens {
let mut pm = vec![false; num_vars];
for v in 0..num_vars {
pm[g[v]] = cur[v];
}
if seen.insert(proj(&pm)) {
out.push(pm);
}
}
}
out
}
pub fn models_up_to_symmetry(num_vars: usize, clauses: &[Vec<Lit>], cap: usize) -> SymmetricCount {
let mut appears = vec![false; num_vars];
for c in clauses {
for l in c {
appears[l.var() as usize] = true;
}
}
let occurs: Vec<usize> = (0..num_vars).filter(|&v| appears[v]).collect();
let gens = crate::sym_break::variable_automorphism_generators(num_vars, clauses).unwrap_or_default();
let mut working = clauses.to_vec();
let mut representatives: Vec<Vec<bool>> = Vec::new();
let mut total_models: u128 = 0;
let mut exhaustive = true;
loop {
if representatives.len() >= cap {
exhaustive = false;
break;
}
match solve_comprehensive(num_vars, &working).answer {
Answer::Unsat => break,
Answer::Sat(m) => {
let orbit = assignment_orbit(num_vars, &m, &gens, &occurs);
total_models = total_models.saturating_add(orbit.len() as u128);
representatives.push(m);
for a in &orbit {
working.push(occurs.iter().map(|&v| Lit::new(v as u32, !a[v])).collect());
}
}
}
}
SymmetricCount { representatives, total_models, exhaustive }
}
#[derive(Clone, Debug, PartialEq, Eq)]
pub struct SymmetryProfile {
pub order: u128,
pub generators: usize,
pub num_orbits: usize,
pub rank: usize,
pub transitivity: usize,
pub primitive: bool,
pub blocks: Option<usize>,
pub abelian: bool,
pub solvable: Option<bool>,
pub nilpotent: Option<bool>,
pub derived_length: Option<usize>,
pub nilpotency_class: Option<usize>,
pub derived_order: u128,
pub conjugacy_classes: Option<usize>,
pub center_order: Option<u128>,
pub exponent: Option<u128>,
pub assignment_orbits: Option<u128>,
pub abelianization: Option<(u128, u128)>,
pub subgroups: Option<usize>,
pub simple: Option<bool>,
pub composition_factors: Option<Vec<u128>>,
pub sylow: Option<Vec<(u128, usize)>>,
pub real_classes: Option<usize>,
pub rational_classes: Option<usize>,
pub irreducible_degrees: Option<Vec<u128>>,
pub frobenius_schur: Option<Vec<i8>>,
pub isotypic_multiplicities: Option<Vec<u128>>,
pub automorphism_order: Option<u128>,
pub outer_automorphism_order: Option<u128>,
pub coherent_rank: Option<usize>,
}
pub fn symmetry_structure(num_vars: usize, clauses: &[Vec<Lit>]) -> SymmetryProfile {
let gens = crate::sym_break::variable_automorphism_generators(num_vars, clauses).unwrap_or_default();
let mut profile = profile_of_generators(num_vars, &gens);
profile.coherent_rank = Some(coherent_rank(num_vars, clauses).unwrap_or_else(|| two_wl_pair_cells(num_vars, clauses)));
profile
}
fn profile_of_generators(num_vars: usize, gens: &[crate::permgroup::Perm]) -> SymmetryProfile {
if gens.is_empty() {
return SymmetryProfile {
order: 1,
generators: 0,
num_orbits: num_vars,
rank: 0,
transitivity: 0,
primitive: false,
blocks: None,
abelian: true, solvable: Some(true),
nilpotent: Some(true),
derived_length: Some(0),
nilpotency_class: Some(0),
derived_order: 1,
conjugacy_classes: Some(1),
center_order: Some(1),
exponent: Some(1),
assignment_orbits: Some(1u128 << num_vars.min(127)),
abelianization: Some((1, 1)),
subgroups: Some(1),
simple: Some(false), composition_factors: Some(Vec::new()),
sylow: Some(Vec::new()),
irreducible_degrees: Some(vec![1]), frobenius_schur: Some(vec![1]), isotypic_multiplicities: Some(vec![num_vars as u128]),
real_classes: Some(1),
rational_classes: Some(1), automorphism_order: Some(1), outer_automorphism_order: Some(1),
coherent_rank: None, };
}
let gens = gens.to_vec();
let order = crate::permgroup::schreier_sims(num_vars, &gens).order();
let num_orbits = crate::permgroup::orbits(num_vars, &gens).len();
let rank = if num_vars <= 48 { crate::permgroup::rank(num_vars, &gens) } else { 0 };
let transitivity =
if num_vars <= 24 { crate::permgroup::transitivity_degree(num_vars, &gens, 3) } else { 0 };
let primitive = crate::permgroup::is_primitive(num_vars, &gens);
let blocks = crate::permgroup::minimal_block_system(num_vars, &gens).map(|b| b.len());
let abelian = crate::permgroup::is_abelian(num_vars, &gens);
let (solvable, nilpotent, derived_length, nilpotency_class, derived_order) = if num_vars <= 24 {
let dl = crate::permgroup::derived_length(num_vars, &gens);
let nc = crate::permgroup::nilpotency_class(num_vars, &gens);
let d = crate::permgroup::derived_subgroup(num_vars, &gens);
(Some(dl.is_some()), Some(nc.is_some()), dl, nc, crate::permgroup::schreier_sims(num_vars, &d).order())
} else {
(None, None, None, None, 0)
};
const ENUM_CAP: usize = 4096;
let classes = crate::permgroup::conjugacy_classes(num_vars, &gens, ENUM_CAP);
let conjugacy_classes = classes.as_ref().map(|c| c.len());
let center_order = classes.map(|c| c.iter().filter(|cls| cls.len() == 1).count() as u128);
let exponent = crate::permgroup::exponent(num_vars, &gens, ENUM_CAP);
let assignment_orbits = crate::permgroup::polya_count(num_vars, &gens, 2, ENUM_CAP);
let abelianization = crate::permgroup::abelianization(num_vars, &gens, ENUM_CAP);
let subgroups = crate::permgroup::subgroup_count(num_vars, &gens, 256);
let simple = crate::permgroup::is_simple(num_vars, &gens, ENUM_CAP);
let composition_factors = crate::permgroup::composition_factor_orders(num_vars, &gens, 256);
let sylow = crate::permgroup::sylow_counts(num_vars, &gens, 256);
let real_classes = crate::permgroup::real_class_count(num_vars, &gens, ENUM_CAP);
let rational_classes = crate::permgroup::rational_class_count(num_vars, &gens, ENUM_CAP);
let ctable = crate::permgroup::character_table(num_vars, &gens, ENUM_CAP);
let irreducible_degrees = ctable.as_ref().map(|t| t.degrees.clone());
let frobenius_schur = ctable.as_ref().and_then(crate::permgroup::frobenius_schur_from_table);
let isotypic_multiplicities =
ctable.as_ref().and_then(|t| crate::permgroup::isotypic_from_table(num_vars, &gens, t));
let automorphism_order = crate::permgroup::automorphism_group_order(num_vars, &gens, 256);
let outer_automorphism_order = match (automorphism_order, center_order) {
(Some(a), Some(c)) if c > 0 => Some(a / (order / c)), _ => None,
};
SymmetryProfile {
order,
generators: gens.len(),
num_orbits,
rank,
transitivity,
primitive,
blocks,
abelian,
solvable,
nilpotent,
derived_length,
nilpotency_class,
derived_order,
conjugacy_classes,
center_order,
exponent,
assignment_orbits,
abelianization,
subgroups,
simple,
composition_factors,
sylow,
real_classes,
rational_classes,
irreducible_degrees,
frobenius_schur,
isotypic_multiplicities,
automorphism_order,
outer_automorphism_order,
coherent_rank: None, }
}
pub fn pb_symmetry_profile(num_vars: usize, constraints: &[crate::pseudo_boolean::PbConstraint]) -> SymmetryProfile {
let gens = crate::pseudo_boolean::coeff_symmetry_generators(num_vars, constraints);
profile_of_generators(num_vars, &gens)
}
pub fn class_algebra_constants(num_vars: usize, clauses: &[Vec<Lit>]) -> Option<Vec<Vec<Vec<u128>>>> {
let gens = crate::sym_break::variable_automorphism_generators(num_vars, clauses).unwrap_or_default();
crate::permgroup::class_multiplication_coefficients(num_vars, &gens, 4096)
}
pub fn character_table(num_vars: usize, clauses: &[Vec<Lit>]) -> Option<crate::permgroup::CharacterTable> {
let gens = crate::sym_break::variable_automorphism_generators(num_vars, clauses).unwrap_or_default();
crate::permgroup::character_table(num_vars, &gens, 4096)
}
pub fn frobenius_schur_indicators(num_vars: usize, clauses: &[Vec<Lit>]) -> Option<Vec<i8>> {
let gens = crate::sym_break::variable_automorphism_generators(num_vars, clauses).unwrap_or_default();
crate::permgroup::frobenius_schur_indicators(num_vars, &gens, 4096)
}
pub fn permutation_character(num_vars: usize, clauses: &[Vec<Lit>]) -> Option<Vec<u128>> {
let gens = crate::sym_break::variable_automorphism_generators(num_vars, clauses).unwrap_or_default();
crate::permgroup::permutation_character(num_vars, &gens, 4096)
}
pub fn isotypic_multiplicities(num_vars: usize, clauses: &[Vec<Lit>]) -> Option<Vec<u128>> {
let gens = crate::sym_break::variable_automorphism_generators(num_vars, clauses).unwrap_or_default();
crate::permgroup::isotypic_multiplicities(num_vars, &gens, 4096)
}
pub fn tensor_decomposition(num_vars: usize, clauses: &[Vec<Lit>]) -> Option<Vec<Vec<Vec<u128>>>> {
let gens = crate::sym_break::variable_automorphism_generators(num_vars, clauses).unwrap_or_default();
crate::permgroup::tensor_decomposition(num_vars, &gens, 4096)
}
pub fn galois_class_orbits(num_vars: usize, clauses: &[Vec<Lit>]) -> Option<Vec<Vec<usize>>> {
let gens = crate::sym_break::variable_automorphism_generators(num_vars, clauses).unwrap_or_default();
crate::permgroup::galois_class_orbits(num_vars, &gens, 4096)
}
pub fn table_of_marks(num_vars: usize, clauses: &[Vec<Lit>]) -> Option<(Vec<u128>, Vec<Vec<u128>>)> {
let gens = crate::sym_break::variable_automorphism_generators(num_vars, clauses).unwrap_or_default();
crate::permgroup::table_of_marks(num_vars, &gens, 256)
}
pub fn burnside_ring_product(num_vars: usize, clauses: &[Vec<Lit>]) -> Option<Vec<Vec<Vec<i128>>>> {
let gens = crate::sym_break::variable_automorphism_generators(num_vars, clauses).unwrap_or_default();
crate::permgroup::burnside_ring_product(num_vars, &gens, 256)
}
pub fn mobius_number(num_vars: usize, clauses: &[Vec<Lit>]) -> Option<i128> {
let gens = crate::sym_break::variable_automorphism_generators(num_vars, clauses).unwrap_or_default();
crate::permgroup::mobius_number(num_vars, &gens, 256)
}
pub fn generating_tuple_count(num_vars: usize, clauses: &[Vec<Lit>], k: u32) -> Option<i128> {
let gens = crate::sym_break::variable_automorphism_generators(num_vars, clauses).unwrap_or_default();
crate::permgroup::generating_tuple_count(num_vars, &gens, 256, k)
}
pub fn permutation_character_decomposition(
num_vars: usize,
clauses: &[Vec<Lit>],
) -> Option<(Vec<u128>, Vec<u128>, Vec<Vec<u128>>)> {
let gens = crate::sym_break::variable_automorphism_generators(num_vars, clauses).unwrap_or_default();
crate::permgroup::permutation_character_decomposition(num_vars, &gens, 256)
}
pub fn automorphism_group_order(num_vars: usize, clauses: &[Vec<Lit>]) -> Option<u128> {
let gens = crate::sym_break::variable_automorphism_generators(num_vars, clauses).unwrap_or_default();
crate::permgroup::automorphism_group_order(num_vars, &gens, 256)
}
pub fn assignment_weight_inventory(num_vars: usize, clauses: &[Vec<Lit>]) -> Option<Vec<u128>> {
let gens = crate::sym_break::variable_automorphism_generators(num_vars, clauses).unwrap_or_default();
crate::permgroup::pattern_inventory(num_vars, &gens, 4096)
}
pub fn break_all_symmetry(num_vars: usize, clauses: &[Vec<Lit>]) -> Vec<Vec<Lit>> {
let key = |a: Lit, b: Lit| -> (u32, bool, u32, bool) {
let (x, y) = ((a.var(), a.is_positive()), (b.var(), b.is_positive()));
if x <= y { (x.0, x.1, y.0, y.1) } else { (y.0, y.1, x.0, x.1) }
};
let mut combined = clauses.to_vec();
let mut seen: HashSet<(u32, bool, u32, bool)> =
combined.iter().filter(|c| c.len() == 2).map(|c| key(c[0], c[1])).collect();
loop {
let gens =
crate::sym_break::variable_automorphism_generators(num_vars, &combined).unwrap_or_default();
if gens.is_empty() {
break; }
let bsgs = crate::permgroup::schreier_sims(num_vars, &gens);
let mut added = false;
for orbit in crate::permgroup::orbits(num_vars, &gens) {
if orbit.len() < 2 {
continue;
}
let full = orbit.windows(2).all(|w| {
let mut t: Vec<usize> = (0..num_vars).collect();
t.swap(w[0], w[1]);
bsgs.contains(&t)
});
if full {
for w in orbit.windows(2) {
let (a, b) = (Lit::neg(w[0] as u32), Lit::pos(w[1] as u32)); if seen.insert(key(a, b)) {
combined.push(vec![a, b]);
added = true;
}
}
}
}
if !added {
for g in &gens {
let Some(v) = (0..num_vars).find(|&i| g[i] != i) else { continue };
let (a, b) = (Lit::neg(v as u32), Lit::pos(g[v] as u32)); if seen.insert(key(a, b)) {
combined.push(vec![a, b]);
added = true;
}
}
}
if !added {
break; }
}
combined
}
pub fn break_all_symmetry_complete(num_vars: usize, clauses: &[Vec<Lit>]) -> (Vec<Vec<Lit>>, usize) {
let gens = crate::sym_break::variable_automorphism_generators(num_vars, clauses).unwrap_or_default();
if gens.is_empty() {
return (clauses.to_vec(), num_vars);
}
let bsgs = crate::permgroup::schreier_sims(num_vars, &gens);
let to_litsym = |p: &[usize]| -> Vec<Lit> { (0..num_vars).map(|v| Lit::pos(p[v] as u32)).collect() };
let group: Vec<Vec<Lit>> = match bsgs.elements(50_000) {
Some(elts) => elts.iter().map(|p| to_litsym(p)).collect(), None => {
let mut g: Vec<Vec<Lit>> = gens.iter().map(|p| to_litsym(p)).collect();
g.extend(bsgs.transversal_elements().iter().map(|p| to_litsym(p)));
g
}
};
let (sbp, total) = crate::sym_break::lex_leader_sbp_lit(num_vars, &group);
let mut combined = clauses.to_vec();
combined.extend(sbp);
(combined, total)
}
pub fn solve_by_symmetry_breaking(num_vars: usize, clauses: &[Vec<Lit>]) -> Solved {
let broken = break_all_symmetry(num_vars, clauses);
let inner = solve_comprehensive(num_vars, &broken);
match inner.answer {
Answer::Sat(model) => {
if clauses.iter().all(|c| c.iter().any(|l| model[l.var() as usize] == l.is_positive())) {
Solved { answer: Answer::Sat(model), via: inner.via, proof: inner.proof, conflicts: inner.conflicts }
} else {
solve_comprehensive(num_vars, clauses) }
}
Answer::Unsat => Solved { answer: Answer::Unsat, via: inner.via, proof: inner.proof, conflicts: inner.conflicts },
}
}
fn modp_route(num_vars: usize, clauses: &[Vec<Lit>]) -> Option<Solved> {
use crate::modp::{self, ModpOutcome};
let rec = modp::recover_from_cnf(num_vars, clauses)?;
let build_model = |assign: &[u64]| -> Option<Vec<bool>> {
let mut model = vec![false; num_vars];
for (g, group) in rec.groups.iter().enumerate() {
if let Some(&bit) = group.get(*assign.get(g).unwrap_or(&0) as usize) {
if (bit as usize) < model.len() {
model[bit as usize] = true;
}
}
}
clauses
.iter()
.all(|c| c.iter().any(|l| model.get(l.var() as usize).copied().unwrap_or(false) == l.is_positive()))
.then_some(model)
};
if modp::is_prime(rec.modulus) {
match modp::solve(&rec.equations, rec.num_vars, rec.modulus) {
ModpOutcome::Unsat(combo) => {
debug_assert!(
modp::is_refutation(&rec.equations, rec.num_vars, rec.modulus, &combo),
"the recovered GF(p) refutation must re-check"
);
Some(Solved::unsat(Route::ModP))
}
ModpOutcome::Sat(assign) => Some(Solved {
answer: Answer::Sat(build_model(&assign)?),
via: Route::ModP,
proof: Vec::new(),
conflicts: 0,
}),
}
} else {
use crate::modm::{self, ModmOutcome};
match modm::solve(&rec.equations, rec.num_vars, rec.modulus)? {
ModmOutcome::Unsat { modulus, combo } => {
debug_assert!(
modm::is_refutation(&rec.equations, rec.num_vars, modulus, &combo),
"the recovered ℤ/m refutation must re-check"
);
Some(Solved::unsat(Route::ModM))
}
ModmOutcome::Sat(assign) => Some(Solved {
answer: Answer::Sat(build_model(&assign)?),
via: Route::ModM,
proof: Vec::new(),
conflicts: 0,
}),
}
}
}
pub fn mine_clauses(num_vars: usize, clauses: &[Vec<Lit>]) -> Vec<Vec<Lit>> {
let mut seen: HashSet<Vec<i64>> = clauses.iter().map(|c| canon(c)).collect();
let mut pool = Vec::new();
let mut add = |bundle: Vec<Vec<Lit>>, pool: &mut Vec<Vec<Lit>>, seen: &mut HashSet<Vec<i64>>| {
for c in bundle {
if seen.insert(canon(&c)) {
pool.push(c);
}
}
};
add(xor_gaussian_bundle(num_vars, clauses), &mut pool, &mut seen);
add(failed_literal_bundle(num_vars, clauses), &mut pool, &mut seen);
pool
}
fn canon(c: &[Lit]) -> Vec<i64> {
let mut k: Vec<i64> = c
.iter()
.map(|l| if l.is_positive() { l.var() as i64 + 1 } else { -(l.var() as i64 + 1) })
.collect();
k.sort_unstable();
k.dedup();
k
}
fn xor_width() -> usize {
std::env::var("LOGOS_XOR_WIDTH").ok().and_then(|s| s.parse().ok()).unwrap_or(3)
}
fn xor_gaussian_bundle(num_vars: usize, clauses: &[Vec<Lit>]) -> Vec<Vec<Lit>> {
let eqs = extract_xor(num_vars, clauses);
if eqs.len() < 2 {
return Vec::new();
}
IncXor::new(num_vars, &eqs).derived_clauses(xor_width())
}
fn failed_literal_bundle(num_vars: usize, clauses: &[Vec<Lit>]) -> Vec<Vec<Lit>> {
if num_vars > 5000 || clauses.len() > 50_000 {
return Vec::new();
}
let mut out = Vec::new();
for v in 0..num_vars {
let neg = Lit::new(v as u32, false);
let pos = Lit::new(v as u32, true);
if crate::rup::is_rup(num_vars, clauses, std::slice::from_ref(&neg)) {
out.push(vec![neg]);
} else if crate::rup::is_rup(num_vars, clauses, std::slice::from_ref(&pos)) {
out.push(vec![pos]);
}
}
out
}
fn as_two_sat(clauses: &[Vec<Lit>]) -> Option<Vec<(crate::twosat::Lit, crate::twosat::Lit)>> {
let cvt = |l: &Lit| {
if l.is_positive() {
crate::twosat::Lit::pos(l.var() as usize)
} else {
crate::twosat::Lit::neg(l.var() as usize)
}
};
let mut out = Vec::with_capacity(clauses.len());
for c in clauses {
match c.as_slice() {
[a] => out.push((cvt(a), cvt(a))),
[a, b] => out.push((cvt(a), cvt(b))),
_ => return None,
}
}
Some(out)
}
fn as_horn(clauses: &[Vec<Lit>]) -> Option<Vec<crate::hornsat::HornClause>> {
let mut out = Vec::with_capacity(clauses.len());
for c in clauses {
if c.is_empty() {
return None;
}
let pos: Vec<usize> = c.iter().filter(|l| l.is_positive()).map(|l| l.var() as usize).collect();
let neg: Vec<usize> = c.iter().filter(|l| !l.is_positive()).map(|l| l.var() as usize).collect();
match pos.len() {
0 => out.push(crate::hornsat::HornClause::goal(neg)),
1 if neg.is_empty() => out.push(crate::hornsat::HornClause::fact(pos[0])),
1 => out.push(crate::hornsat::HornClause::rule(neg, pos[0])),
_ => return None,
}
}
Some(out)
}
fn cnf_to_expr(clauses: &[Vec<Lit>]) -> Option<ProofExpr> {
let atom = |l: &Lit| {
let a = ProofExpr::Atom(format!("v{}", l.var()));
if l.is_positive() { a } else { ProofExpr::Not(Box::new(a)) }
};
let mut clause_exprs = Vec::with_capacity(clauses.len());
for c in clauses {
if c.is_empty() {
return None;
}
let atoms: Vec<ProofExpr> = c.iter().map(&atom).collect();
clause_exprs.push(balanced(atoms, &|a, b| ProofExpr::Or(Box::new(a), Box::new(b)))?);
}
balanced(clause_exprs, &|a, b| ProofExpr::And(Box::new(a), Box::new(b)))
}
fn balanced(mut items: Vec<ProofExpr>, combine: &dyn Fn(ProofExpr, ProofExpr) -> ProofExpr) -> Option<ProofExpr> {
if items.is_empty() {
return None;
}
while items.len() > 1 {
let mut next = Vec::with_capacity(items.len().div_ceil(2));
let mut it = items.into_iter();
while let Some(a) = it.next() {
match it.next() {
Some(b) => next.push(combine(a, b)),
None => next.push(a),
}
}
items = next;
}
items.into_iter().next()
}
fn hybrid_xor(num_vars: usize, clauses: &[Vec<Lit>]) -> Option<Solved> {
if num_vars == 0 {
return None;
}
let eqs = extract_xor(num_vars, clauses);
let mut xor_vars = HashSet::new();
for e in &eqs {
xor_vars.extend(e.vars.iter().copied());
}
if eqs.len() < 2 || xor_vars.len() * 2 < num_vars {
return None;
}
let engine = IncXor::new(num_vars, &eqs);
if !engine.is_active() {
return None;
}
let witness = match crate::xorsat::solve(&eqs, num_vars) {
XorOutcome::Unsat(_) => return Some(Solved::unsat(Route::HybridXor)),
XorOutcome::Sat(w) => w,
};
let derived = engine.derived_clauses(xor_width());
let mut solver = Solver::new(num_vars);
for c in clauses {
solver.add_clause(c.clone());
}
for c in derived {
solver.add_clause(c);
}
if xor_seed() {
solver.set_initial_phase(&witness);
}
let result = if xor_live() {
let live = IncXor::new(num_vars, &eqs);
if xor_kernel() {
let decisions = live.decision_vars();
solver.set_decision_vars(&decisions);
}
let mut theories: Vec<Box<dyn crate::cdcl::Theory>> = vec![Box::new(live)];
solver.solve_with(&mut theories)
} else {
solver.solve()
};
match result {
SolveResult::Sat(model) => Some(Solved {
answer: Answer::Sat(model),
via: Route::HybridXor,
proof: Vec::new(),
conflicts: solver.conflicts(),
}),
SolveResult::Unsat => {
let proof = solver.learned().iter().map(|lc| ProofStep::Rup(lc.lits.clone())).collect();
Some(Solved { answer: Answer::Unsat, via: Route::HybridXor, proof, conflicts: solver.conflicts() })
}
}
}
fn fused_modular_solve(num_vars: usize, clauses: &[Vec<Lit>]) -> Option<Solved> {
if num_vars == 0 {
return None;
}
let eqs = extract_xor(num_vars, clauses);
let amo = crate::lyapunov::recover_cardinality_substructure(num_vars, clauses);
if eqs.is_empty() || amo.is_empty() {
return None;
}
let mut solver = Solver::new(num_vars);
for c in clauses {
solver.add_clause(c.clone());
}
let mut theories: Vec<Box<dyn crate::cdcl::Theory>> = vec![
Box::new(crate::xor_engine::XorEngine::new(num_vars, &eqs)),
Box::new(crate::pseudo_boolean::CardinalityTheory::new(num_vars, &amo)),
Box::new(crate::lyapunov::SymmetryTheory::new(num_vars, crate::lyapunov::fused_symmetry_group(num_vars, clauses))),
];
match solver.solve_with(&mut theories) {
SolveResult::Sat(model) => {
clauses
.iter()
.all(|c| c.iter().any(|l| model[l.var() as usize] == l.is_positive()))
.then_some(Solved {
answer: Answer::Sat(model),
via: Route::HybridXor,
proof: Vec::new(),
conflicts: solver.conflicts(),
})
}
SolveResult::Unsat => {
Some(Solved { answer: Answer::Unsat, via: Route::HybridXor, proof: Vec::new(), conflicts: solver.conflicts() })
}
}
}
fn xor_live() -> bool {
std::env::var("LOGOS_XOR_LIVE").map(|s| s != "0" && !s.is_empty()).unwrap_or(false)
}
fn xor_kernel() -> bool {
std::env::var("LOGOS_XOR_KERNEL").map(|s| s != "0" && !s.is_empty()).unwrap_or(true)
}
fn xor_seed() -> bool {
std::env::var("LOGOS_XOR_SEED").map(|s| s != "0" && !s.is_empty()).unwrap_or(true)
}
#[cfg(test)]
mod tests {
use super::*;
use crate::families::{clique_coloring, php, tseitin_expander};
use crate::rup::check_refutation;
#[test]
fn pigeonhole_is_crushed_by_a_specialist_not_cdcl() {
let (cnf, _) = php(20);
let solved = solve_structured(cnf.num_vars, &cnf.clauses);
assert!(matches!(solved.answer, Answer::Unsat));
assert_ne!(solved.via, Route::Cdcl, "PHP must be crushed structurally, got CDCL");
}
#[test]
fn massive_pigeonhole_does_not_fall_to_search() {
let (cnf, _) = php(50);
let solved = solve_structured(cnf.num_vars, &cnf.clauses);
assert!(matches!(solved.answer, Answer::Unsat));
assert_ne!(solved.via, Route::Cdcl);
}
#[test]
fn clique_colouring_is_crushed_structurally() {
let (cnf, _) = clique_coloring(8, 7);
let solved = solve_structured(cnf.num_vars, &cnf.clauses);
assert!(matches!(solved.answer, Answer::Unsat));
assert_ne!(solved.via, Route::Cdcl, "clique-colouring must be crushed structurally");
}
#[test]
fn sparse_sat_is_certified_by_lll_not_search() {
let cl = |vs: [u32; 4]| vs.iter().map(|&v| Lit::pos(v)).collect::<Vec<_>>();
let clauses = vec![cl([0, 1, 2, 3]), cl([4, 5, 6, 7]), cl([8, 9, 10, 11]), cl([12, 13, 14, 15])];
let solved = solve_structured(16, &clauses);
assert_eq!(solved.via, Route::Lll, "a locally-sparse SAT formula must route to LLL");
match &solved.answer {
Answer::Sat(model) => assert!(
clauses.iter().all(|c| c.iter().any(|l| model[l.var() as usize] == l.is_positive())),
"the LLL/Moser–Tardos witness must satisfy every clause"
),
Answer::Unsat => panic!("a satisfiable sparse formula must not be reported UNSAT"),
}
}
#[test]
fn tseitin_parity_is_crushed_structurally() {
let (_, cnf, _) = tseitin_expander(40, 7);
let solved = solve_structured(cnf.num_vars, &cnf.clauses);
assert!(matches!(solved.answer, Answer::Unsat));
assert!(
matches!(solved.via, Route::Parity | Route::Collapse),
"Tseitin parity must go through the GF(2) route, got {:?}",
solved.via
);
}
#[test]
fn two_sat_is_decided_with_a_model() {
let clauses = vec![
vec![Lit::new(0, true), Lit::new(1, true)],
vec![Lit::new(0, false), Lit::new(1, true)],
vec![Lit::new(0, true), Lit::new(1, false)],
];
let solved = solve_structured(2, &clauses);
assert_eq!(solved.via, Route::TwoSat);
match solved.answer {
Answer::Sat(m) => {
for c in &clauses {
assert!(c.iter().any(|l| m[l.var() as usize] == l.is_positive()));
}
}
Answer::Unsat => panic!("instance is SAT"),
}
}
#[test]
fn horn_is_decided_with_its_least_model() {
let clauses = vec![
vec![Lit::new(0, true)],
vec![Lit::new(1, true)],
vec![Lit::new(0, false), Lit::new(1, false), Lit::new(2, true)],
];
let solved = solve_structured(3, &clauses);
assert_eq!(solved.via, Route::Horn);
match solved.answer {
Answer::Sat(m) => assert!(m[0] && m[1] && m[2]),
Answer::Unsat => panic!("instance is SAT"),
}
}
#[test]
fn unstructured_sat_returns_a_model_via_cdcl() {
let clauses = vec![
vec![Lit::new(0, true), Lit::new(1, true), Lit::new(2, true)],
vec![Lit::new(0, false), Lit::new(1, true), Lit::new(2, false)],
];
let solved = solve_structured(3, &clauses);
match solved.answer {
Answer::Sat(m) => {
for c in &clauses {
assert!(c.iter().any(|l| m[l.var() as usize] == l.is_positive()));
}
}
Answer::Unsat => panic!("instance is SAT"),
}
}
#[test]
fn cdcl_route_carries_a_valid_rup_certificate() {
let clauses = vec![
vec![Lit::new(0, true), Lit::new(1, true), Lit::new(2, true)],
vec![Lit::new(0, true), Lit::new(1, true), Lit::new(2, false)],
vec![Lit::new(0, false), Lit::new(1, false), 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, false), Lit::new(2, true)],
vec![Lit::new(0, false), Lit::new(1, true), Lit::new(2, false)],
vec![Lit::new(0, true), Lit::new(1, false), Lit::new(2, false)],
vec![Lit::new(0, false), Lit::new(1, true), Lit::new(2, true)],
];
let solved = solve_structured(3, &clauses);
assert!(matches!(solved.answer, Answer::Unsat));
if solved.via == Route::Cdcl {
let learned: Vec<Vec<Lit>> = solved.proof.iter().map(|s| s.clause().to_vec()).collect();
assert!(check_refutation(3, &clauses, &learned));
}
}
fn xor_gadget(vars: &[u32], rhs: bool) -> Vec<Vec<Lit>> {
let k = vars.len();
let mut clauses = Vec::new();
for mask in 0u32..(1 << k) {
if ((mask.count_ones() % 2) == 1) != rhs {
clauses.push((0..k).map(|i| Lit::new(vars[i], (mask >> i) & 1 == 0)).collect());
}
}
clauses
}
#[test]
fn hybrid_xor_solves_an_xor_heavy_sat_instance_with_a_valid_model() {
let mut clauses = xor_gadget(&[0, 1, 2], false);
clauses.extend(xor_gadget(&[2, 3], true));
clauses.push(vec![Lit::new(0, true)]);
clauses.push(vec![Lit::new(1, true), Lit::new(3, true)]);
let solved = solve_structured(4, &clauses);
assert_eq!(solved.via, Route::HybridXor, "XOR-heavy SAT must take the hybrid route");
match solved.answer {
Answer::Sat(m) => {
for c in &clauses {
assert!(c.iter().any(|l| m[l.var() as usize] == l.is_positive()), "model fails {c:?}");
}
}
Answer::Unsat => panic!("instance is SAT"),
}
}
#[test]
fn fused_route_decides_a_mixed_parity_cardinality_instance() {
let mut clauses: Vec<Vec<Lit>> = vec![
vec![Lit::new(0, true), Lit::new(1, true), Lit::new(2, true)],
vec![Lit::new(0, false), Lit::new(1, false)],
vec![Lit::new(0, false), Lit::new(2, false)],
vec![Lit::new(1, false), Lit::new(2, false)],
];
for i in 0..3u32 {
clauses.extend(xor_gadget(&[i, i + 3], false)); }
clauses.extend(xor_gadget(&[3, 4, 5], false)); let solved = solve_comprehensive(6, &clauses);
assert!(matches!(solved.answer, Answer::Unsat), "the mixed instance is UNSAT (via {:?})", solved.via);
assert_eq!(solved.via, Route::HybridXor, "the fused parity+cardinality route must fire");
}
#[test]
fn xor_inconsistent_system_is_refuted_structurally() {
let mut clauses = xor_gadget(&[0, 1], false);
clauses.extend(xor_gadget(&[1, 2], false));
clauses.extend(xor_gadget(&[0, 2], true));
let solved = solve_structured(3, &clauses);
assert!(matches!(solved.answer, Answer::Unsat));
assert_ne!(solved.via, Route::Cdcl, "a contradictory linear system must collapse structurally");
}
#[test]
fn mod_p_tseitin_cnf_is_lifted_to_gf_p_not_left_to_cdcl() {
for &p in &[3u64, 5] {
let (_, cnf, _) = crate::families::mod_p_tseitin_expander(6, p, 0xC0FFEE);
let solved = solve_structured(cnf.num_vars, &cnf.clauses);
assert!(matches!(solved.answer, Answer::Unsat), "mod-{p} Tseitin is UNSAT");
assert_eq!(solved.via, Route::ModP, "mod-{p} CNF must be lifted to the GF(p) route");
assert_eq!(solved.conflicts, 0, "the GF(p) collapse spends no search");
}
}
#[test]
fn the_gf_p_route_returns_a_verified_model_on_a_satisfiable_mod_p_cnf() {
let p = 3u64;
let (_, cnf, _) = crate::families::mod_p_consistent_onehot(6, p, 0xABCD);
let solved = solve_structured(cnf.num_vars, &cnf.clauses);
assert_eq!(solved.via, Route::ModP, "a consistent mod-p one-hot CNF must take the GF(p) route");
match &solved.answer {
Answer::Sat(m) => assert!(
cnf.clauses.iter().all(|c| c.iter().any(|l| m[l.var() as usize] == l.is_positive())),
"the GF(p) model must satisfy every clause"
),
Answer::Unsat => panic!("a consistent mod-p system must be SAT"),
}
}
#[test]
fn the_gf_p_route_never_misfires_on_unstructured_or_non_linear_cnf() {
let rnd = crate::families::random_3sat(30, 120, 0x5EED);
let rnd_via = solve_structured(rnd.num_vars, &rnd.clauses).via;
assert_ne!(rnd_via, Route::ModP);
assert_ne!(rnd_via, Route::ModM, "random must not be misrouted to the composite lift either");
let (php_cnf, _) = php(6);
let php_via = solve_structured(php_cnf.num_vars, &php_cnf.clauses).via;
assert_ne!(php_via, Route::ModP);
assert_ne!(php_via, Route::ModM);
}
#[test]
fn the_gf_p_route_agrees_with_boolean_brute_force_on_tiny_instances() {
for (cnf, want_sat) in [
(crate::families::mod_p_tseitin_expander(4, 3, 1).1, false),
(crate::families::mod_p_consistent_onehot(4, 3, 1).1, true),
] {
let solved = solve_structured(cnf.num_vars, &cnf.clauses);
assert_eq!(solved.via, Route::ModP, "a tiny mod-3 instance must take the GF(p) route");
let brute = (0u64..(1u64 << cnf.num_vars)).any(|code| {
let asg: Vec<bool> = (0..cnf.num_vars).map(|i| (code >> i) & 1 == 1).collect();
cnf.clauses.iter().all(|c| c.iter().any(|l| asg[l.var() as usize] == l.is_positive()))
});
assert_eq!(matches!(solved.answer, Answer::Sat(_)), brute, "GF(p) verdict must match brute force");
assert_eq!(brute, want_sat, "family verdict sanity");
}
}
#[test]
fn composite_modulus_onehot_cnf_is_lifted_to_zmod_m_not_left_to_cdcl() {
let (_, cnf, _) = crate::families::mod_p_tseitin_expander(6, 6, 0xC0FFEE);
let solved = solve_structured(cnf.num_vars, &cnf.clauses);
assert!(matches!(solved.answer, Answer::Unsat), "mod-6 Tseitin is UNSAT");
assert_eq!(solved.via, Route::ModM, "a composite mod-6 CNF must be lifted to the ℤ/m route");
assert_eq!(solved.conflicts, 0, "the ℤ/m collapse spends no search");
}
#[test]
fn the_zmod_m_route_returns_a_verified_model_on_a_satisfiable_composite_cnf() {
let (_, cnf, _) = crate::families::mod_p_consistent_onehot(6, 6, 0xABCD);
let solved = solve_structured(cnf.num_vars, &cnf.clauses);
assert_eq!(solved.via, Route::ModM, "a consistent composite one-hot CNF must take the ℤ/m route");
match &solved.answer {
Answer::Sat(m) => assert!(
cnf.clauses.iter().all(|c| c.iter().any(|l| m[l.var() as usize] == l.is_positive())),
"the ℤ/m model must satisfy every clause"
),
Answer::Unsat => panic!("a consistent composite system must be SAT"),
}
}
#[test]
fn the_sos_route_is_sound_in_the_dispatcher() {
fn sm(s: &mut u64) -> u64 {
*s = s.wrapping_add(0x9E37_79B9_7F4A_7C15);
let mut z = *s;
z = (z ^ (z >> 30)).wrapping_mul(0xBF58_476D_1CE4_E5B9);
z ^ (z >> 31)
}
fn brute_sat(nv: usize, cl: &[Vec<Lit>]) -> bool {
(0u64..(1u64 << nv))
.any(|x| cl.iter().all(|c| c.iter().any(|l| ((x >> l.var()) & 1 != 0) == l.is_positive())))
}
let mut state = 0x5005_7777u64;
for _ in 0..120 {
let nv = 4usize;
let m = 6 + (sm(&mut state) % 8) as usize;
let mut cl: Vec<Vec<Lit>> = Vec::new();
for _ in 0..m {
let mut vs: Vec<u32> = Vec::new();
while vs.len() < 3 {
let v = (sm(&mut state) % nv as u64) as u32;
if !vs.contains(&v) {
vs.push(v);
}
}
cl.push(vs.iter().map(|&v| Lit::new(v, sm(&mut state) % 2 == 0)).collect());
}
let solved = solve_structured(nv, &cl);
let sat = brute_sat(nv, &cl);
if solved.via == Route::Sos {
assert!(matches!(solved.answer, Answer::Unsat), "the SoS route only ever refutes");
assert!(!sat, "the SoS route must never fire on a satisfiable instance: {cl:?}");
}
if sat {
assert_ne!(solved.via, Route::Sos, "a satisfiable instance must not be routed to SoS");
}
}
}
#[test]
fn solve_comprehensive_matches_brute_force() {
fn sm(s: &mut u64) -> u64 {
*s = s.wrapping_add(0x9E37_79B9_7F4A_7C15);
let mut z = *s;
z = (z ^ (z >> 30)).wrapping_mul(0xBF58_476D_1CE4_E5B9);
z ^ (z >> 31)
}
fn brute_sat(nv: usize, cl: &[Vec<Lit>]) -> bool {
(0u64..(1u64 << nv))
.any(|x| cl.iter().all(|c| c.iter().any(|l| ((x >> l.var()) & 1 != 0) == l.is_positive())))
}
let mut state = 0xC0DE_5A1Du64;
for _ in 0..80 {
let nv = 3 + (sm(&mut state) % 3) as usize; let m = 2 + (sm(&mut state) % 10) as usize;
let mut cl: Vec<Vec<Lit>> = Vec::new();
for _ in 0..m {
let mut c = Vec::new();
for v in 0..nv {
if sm(&mut state) % 2 == 0 {
c.push(Lit::new(v as u32, sm(&mut state) % 2 == 0));
}
}
if !c.is_empty() {
cl.push(c);
}
}
if cl.is_empty() {
continue;
}
let solved = solve_comprehensive(nv, &cl);
assert_eq!(
matches!(solved.answer, Answer::Sat(_)),
brute_sat(nv, &cl),
"solve_comprehensive verdict must match brute force via {:?}: {cl:?}",
solved.via
);
if let Answer::Sat(m) = &solved.answer {
assert!(
cl.iter().all(|c| c.iter().any(|l| m[l.var() as usize] == l.is_positive())),
"a reported model must satisfy every clause: {cl:?}"
);
}
}
}
#[test]
fn the_symmetry_break_route_solves_a_symmetric_instance() {
let (cnf, _) = crate::families::clique_coloring(3, 3);
let s = symmetry_break_solve(cnf.num_vars, &cnf.clauses)
.expect("clique colouring has a usable, phase-free symmetry group");
assert_eq!(s.via, Route::SymmetryBreak);
match s.answer {
Answer::Sat(m) => assert!(
cnf.clauses.iter().all(|c| c.iter().any(|l| m[l.var() as usize] == l.is_positive())),
"the symmetry-break route returns a valid model"
),
Answer::Unsat => panic!("clique_coloring(3,3) is SAT"),
}
}
#[test]
fn dynamic_sel_refutes_a_symmetric_instance_in_search() {
let (cnf, _) = crate::families::php(5);
let solved =
dynamic_sel(cnf.num_vars, &cnf.clauses).expect("PHP is symmetric — dynamic SEL engages");
assert_eq!(solved.via, Route::Sel);
assert!(matches!(solved.answer, Answer::Unsat), "PHP(5) is UNSAT");
assert!(!solved.proof.is_empty(), "SEL returns a refutation proof");
}
#[test]
fn orbital_branch_collapses_symmetric_branches_and_is_correct() {
let (sat_cnf, _) = crate::families::clique_coloring(3, 3);
let s = orbital_branch_solve(sat_cnf.num_vars, &sat_cnf.clauses)
.expect("a large variable orbit drives orbital branching");
assert_eq!(s.via, Route::OrbitalBranch);
match &s.answer {
Answer::Sat(m) => assert!(
sat_cnf.clauses.iter().all(|c| c.iter().any(|l| m[l.var() as usize] == l.is_positive())),
"orbital branching returns a valid model"
),
Answer::Unsat => panic!("clique_coloring(3,3) is SAT"),
}
let (unsat_cnf, _) = crate::families::clique_coloring(4, 3);
let u = orbital_branch_solve(unsat_cnf.num_vars, &unsat_cnf.clauses)
.expect("a large variable orbit drives orbital branching");
assert_eq!(u.via, Route::OrbitalBranch);
assert!(matches!(u.answer, Answer::Unsat), "clique_coloring(4,3) is UNSAT");
let (big_cnf, _) = crate::families::clique_coloring(4, 4);
let big = orbital_branch_solve(big_cnf.num_vars, &big_cnf.clauses)
.expect("recursive orbital branching engages on the larger grid");
assert_eq!(big.via, Route::OrbitalBranch);
match &big.answer {
Answer::Sat(m) => assert!(
big_cnf.clauses.iter().all(|c| c.iter().any(|l| m[l.var() as usize] == l.is_positive())),
"the recursive orbital model is valid"
),
Answer::Unsat => panic!("clique_coloring(4,4) is SAT"),
}
for (cnf, _) in [
crate::families::clique_coloring(3, 3),
crate::families::clique_coloring(4, 3),
crate::families::clique_coloring(4, 4),
] {
let nv = cnf.num_vars;
let brute = (0u64..(1u64 << nv)).any(|x| {
let a: Vec<bool> = (0..nv).map(|i| (x >> i) & 1 == 1).collect();
cnf.clauses.iter().all(|c| c.iter().any(|l| a[l.var() as usize] == l.is_positive()))
});
let got = orbital_branch_solve(nv, &cnf.clauses).expect("orbital fires");
assert_eq!(
matches!(got.answer, Answer::Sat(_)),
brute,
"orbital-branch verdict matches brute force (nv={nv})"
);
}
}
#[test]
fn solve_by_symmetry_breaking_matches_brute_force() {
let instances = [
crate::families::clique_coloring(3, 3), crate::families::clique_coloring(4, 3), crate::families::clique_coloring(4, 4), ];
for (cnf, _) in instances {
let nv = cnf.num_vars;
let brute = (0u64..(1u64 << nv)).any(|x| {
let a: Vec<bool> = (0..nv).map(|i| (x >> i) & 1 == 1).collect();
cnf.clauses.iter().all(|c| c.iter().any(|l| a[l.var() as usize] == l.is_positive()))
});
let solved = solve_by_symmetry_breaking(nv, &cnf.clauses);
assert_eq!(matches!(solved.answer, Answer::Sat(_)), brute, "break-then-solve matches brute (nv={nv})");
if let Answer::Sat(m) = &solved.answer {
assert!(
cnf.clauses.iter().all(|c| c.iter().any(|l| m[l.var() as usize] == l.is_positive())),
"the projected model satisfies the original formula"
);
}
}
}
#[test]
fn break_all_symmetry_complete_leaves_one_model_per_orbit() {
let count_original = |total: usize, cl: &[Vec<Lit>], nv: usize| -> usize {
let mut working = cl.to_vec();
let mut count = 0;
loop {
match solve_comprehensive(total, &working).answer {
Answer::Unsat => break,
Answer::Sat(m) => {
count += 1;
working.push((0..nv).map(|v| Lit::new(v as u32, !m[v])).collect());
}
}
}
count
};
let n = |v| Lit::new(v, false);
let amo = vec![vec![n(0), n(1)], vec![n(0), n(2)], vec![n(1), n(2)]];
let orbits_amo = models_up_to_symmetry(3, &amo, 1000).representatives.len();
let (b1, t1) = break_all_symmetry_complete(3, &amo);
assert_eq!(count_original(t1, &b1, 3), orbits_amo, "one model per orbit (at-most-1-of-3)");
let (cnf, _) = crate::families::clique_coloring(3, 3);
let orbits_clq = models_up_to_symmetry(cnf.num_vars, &cnf.clauses, 1000).representatives.len();
let (b2, t2) = break_all_symmetry_complete(cnf.num_vars, &cnf.clauses);
assert_eq!(orbits_clq, 1, "clique(3,3)'s colourings form a single orbit");
assert_eq!(count_original(t2, &b2, cnf.num_vars), 1, "complete breaking leaves exactly one model (clique)");
let asym = vec![vec![Lit::new(0, true)], vec![n(1), Lit::new(2, true)]];
let (b3, t3) = break_all_symmetry_complete(3, &asym);
assert_eq!((b3.len(), t3), (asym.len(), 3), "no symmetry ⇒ no breaks");
}
#[test]
fn break_all_symmetry_runs_to_a_fixpoint_soundly() {
let (cnf, _) = crate::families::clique_coloring(3, 3);
let before = symmetry_structure(cnf.num_vars, &cnf.clauses).order;
let broken = break_all_symmetry(cnf.num_vars, &cnf.clauses);
let after = symmetry_structure(cnf.num_vars, &broken).order;
assert!(after < before, "the breaker reduced the symmetry group: {before} → {after}");
let orig = solve_comprehensive(cnf.num_vars, &cnf.clauses).answer;
let brk = solve_comprehensive(cnf.num_vars, &broken).answer;
assert_eq!(matches!(orig, Answer::Sat(_)), matches!(brk, Answer::Sat(_)), "breaking preserves the verdict");
if let Answer::Sat(m) = &brk {
assert!(
cnf.clauses.iter().all(|c| c.iter().any(|l| m[l.var() as usize] == l.is_positive())),
"the broken-formula model is a genuine model of the original"
);
}
let twice = break_all_symmetry(cnf.num_vars, &broken);
assert_eq!(twice.len(), broken.len(), "already at the fixpoint — re-breaking is a no-op");
let asym = vec![vec![Lit::new(0, true)], vec![Lit::new(1, false), Lit::new(2, true)]];
assert_eq!(break_all_symmetry(3, &asym).len(), asym.len(), "no symmetry ⇒ no breaks");
}
#[test]
fn class_algebra_constants_wrapper_has_the_right_shape() {
let (cnf, _) = crate::families::clique_coloring(3, 3);
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");
assert_eq!(a.len(), k, "the class-algebra tensor is k × k × k");
assert!(a.iter().all(|m| m.len() == k && m.iter().all(|r| r.len() == k)));
}
#[test]
fn character_table_wrapper_is_the_grid_groups_table() {
let (cnf, _) = crate::families::clique_coloring(3, 3);
let t = character_table(cnf.num_vars, &cnf.clauses).expect("enumerable group");
assert_eq!(t.degrees, vec![1, 1, 1, 1, 2, 2, 2, 2, 4], "S₃×S₃ irreducible degrees");
assert_eq!(t.degrees.iter().map(|d| d * d).sum::<u128>(), 36, "Σ dᵢ² = |S₃×S₃|");
assert_eq!(t.values.len(), t.degrees.len(), "one character per irreducible");
assert!(t.values.iter().all(|row| row.len() == t.class_sizes.len()), "a value per conjugacy class");
assert!(t.values.iter().any(|row| row.iter().all(|&x| x == 1)), "the trivial character is present");
}
#[test]
fn frobenius_schur_wrapper_reports_a_real_grid_group() {
let (cnf, _) = crate::families::clique_coloring(3, 3);
let fs = frobenius_schur_indicators(cnf.num_vars, &cnf.clauses).expect("enumerable group");
assert_eq!(fs, vec![1; 9], "S₃×S₃: nine real irreducibles");
}
#[test]
fn isotypic_decomposition_wrapper_bridges_action_and_representation() {
let (cnf, _) = crate::families::clique_coloring(3, 3);
let iso = isotypic_multiplicities(cnf.num_vars, &cnf.clauses).expect("enumerable group");
let degs = symmetry_structure(cnf.num_vars, &cnf.clauses).irreducible_degrees.unwrap();
assert_eq!(iso.iter().zip(°s).map(|(m, d)| m * d).sum::<u128>(), 9, "Σ m·d = 9 cells");
let pi = permutation_character(cnf.num_vars, &cnf.clauses).expect("enumerable group");
assert!(pi.contains(&9), "the identity class fixes all 9 variables");
}
#[test]
fn automorphism_group_wrapper_measures_the_symmetry_of_the_symmetry() {
let (cnf, _) = crate::families::clique_coloring(3, 3);
assert_eq!(
automorphism_group_order(cnf.num_vars, &cnf.clauses),
Some(72),
"|Aut(S₃×S₃)| = 72"
);
}
#[test]
fn table_of_marks_wrapper_classifies_a_grid_groups_g_sets() {
let (cnf, _) = crate::families::clique_coloring(3, 3);
let (orders, marks) = table_of_marks(cnf.num_vars, &cnf.clauses).expect("subgroup lattice in range");
let k = orders.len();
assert_eq!(*orders.last().unwrap(), 36, "the whole group S₃×S₃ has order 36");
assert_eq!(marks[0][0], 36, "m(1, 1) = [G:1] = |G| = 36 (the regular action)");
for j in 0..k {
assert_eq!(marks[0][j], 36 / orders[j], "m(1, H_j) = [G : H_j]");
assert_eq!(marks[j][k - 1], 1, "every subgroup fixes the one coset of G");
}
}
#[test]
fn galois_class_orbits_wrapper_partitions_a_rational_grid_group() {
let (cnf, _) = crate::families::clique_coloring(3, 3);
let orbits = galois_class_orbits(cnf.num_vars, &cnf.clauses).expect("enumerable group");
assert_eq!(orbits.len(), 9, "S₃×S₃ has 9 conjugacy classes");
assert!(orbits.iter().all(|o| o.len() == 1), "all rational ⇒ every orbit is a singleton");
let prof = symmetry_structure(cnf.num_vars, &cnf.clauses);
assert_eq!(prof.rational_classes, Some(9));
}
#[test]
fn tensor_decomposition_wrapper_is_a_valid_fusion_ring() {
let (cnf, _) = crate::families::clique_coloring(3, 3);
let degs = symmetry_structure(cnf.num_vars, &cnf.clauses).irreducible_degrees.unwrap();
let n = tensor_decomposition(cnf.num_vars, &cnf.clauses).expect("enumerable group");
let k = degs.len();
assert_eq!(n.len(), k, "a k×k×k fusion tensor");
for i in 0..k {
for j in 0..k {
assert_eq!(
(0..k).map(|c| n[i][j][c] * degs[c]).sum::<u128>(),
degs[i] * degs[j],
"dim(χ_i ⊗ χ_j) = d_i·d_j"
);
}
}
}
#[test]
fn equivalence_symmetry_matches_brute_force_and_reduces() {
let p = |v: u32| Lit::new(v, true);
let nl = |v: u32| Lit::new(v, false);
let sat = |m: &[bool], cls: &[Vec<Lit>]| {
cls.iter().all(|c| c.iter().any(|l| m[l.var() as usize] == l.is_positive()))
};
let brute_equiv = |nv: usize, f: &[Vec<Lit>], s: &[Vec<Lit>]| -> bool {
(0u32..(1u32 << nv)).all(|x| {
let a: Vec<bool> = (0..nv).map(|i| (x >> i) & 1 == 1).collect();
sat(&a, f) == sat(&a, s)
})
};
let amo: Vec<Vec<Lit>> =
(0..4u32).flat_map(|i| ((i + 1)..4).map(move |j| vec![nl(i), nl(j)])).collect();
assert_eq!(amo.len(), 6);
let gens = common_automorphism_generators(4, &amo, &amo);
assert!(!gens.is_empty(), "at-most-one-of-4 has a nontrivial common symmetry group");
let (reps, naive) = equivalence_check_counts(4, &amo, &amo);
assert!(reps < naive, "the common symmetry must reduce the work: {reps} < {naive}");
assert_eq!(equivalent_modulo_symmetry(4, &amo, &amo), EquivVerdict::Equivalent);
let f2 = vec![vec![p(0), p(1)], vec![nl(0), p(1)]];
let mut s2 = f2.clone();
s2.push(vec![p(1)]);
assert!(brute_equiv(2, &f2, &s2), "sanity: the resolvent makes them equivalent");
assert_eq!(equivalent_modulo_symmetry(2, &f2, &s2), EquivVerdict::Equivalent);
let f3 = vec![vec![p(0), p(1)], vec![nl(0), nl(1)]];
let s3 = vec![vec![p(0), p(1)]];
match equivalent_modulo_symmetry(2, &f3, &s3) {
EquivVerdict::Differ(m) => assert_ne!(sat(&m, &f3), sat(&m, &s3), "witness must distinguish"),
EquivVerdict::Equivalent => panic!("f3 and s3 are NOT equivalent"),
}
let fa = vec![vec![p(0), p(1)]];
let sa = vec![vec![p(0), p(1)], vec![p(1), p(2)]];
let (r, t) = equivalence_check_counts(3, &fa, &sa);
assert_eq!(r, t, "no common symmetry ⇒ one check per clause");
fn xs(s: &mut u64) -> u64 {
*s ^= *s << 13;
*s ^= *s >> 7;
*s ^= *s << 17;
*s
}
let nv = 4usize;
let mk = |s: &mut u64| -> Vec<Vec<Lit>> {
let m = (xs(s) % 5) as usize; (0..m)
.map(|_| {
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()
})
.collect()
};
let mut seed = 0x1234_5678_9abc_def0u64;
for _ in 0..400 {
let f = mk(&mut seed);
let s = mk(&mut seed);
let want = brute_equiv(nv, &f, &s);
match equivalent_modulo_symmetry(nv, &f, &s) {
EquivVerdict::Equivalent => {
assert!(want, "claimed equivalent but brute says differ: F={f:?} S={s:?}")
}
EquivVerdict::Differ(m) => {
assert!(!want, "claimed differ but brute says equivalent: F={f:?} S={s:?}");
assert_ne!(sat(&m, &f), sat(&m, &s), "witness must distinguish F and S");
}
}
}
}
#[test]
fn optimization_symmetry_matches_brute_force_and_reduces() {
let p = |v: u32| Lit::new(v, true);
let sat = |m: &[bool], cls: &[Vec<Lit>]| {
cls.iter().all(|c| c.iter().any(|l| m[l.var() as usize] == l.is_positive()))
};
let brute_min = |nv: usize, f: &[Vec<Lit>], w: &[i64]| -> Option<i64> {
(0u32..(1u32 << nv))
.filter_map(|x| {
let a: Vec<bool> = (0..nv).map(|i| (x >> i) & 1 == 1).collect();
sat(&a, f).then(|| (0..nv).filter(|&i| a[i]).map(|i| w[i]).sum::<i64>())
})
.min()
};
let amo1 = vec![vec![p(0), p(1), p(2), p(3)]];
let w1 = vec![1i64; 4];
let (opt, m) = optimize_modulo_symmetry(4, &amo1, &w1).expect("F is satisfiable");
assert_eq!(opt, 1, "minimum is one variable true");
assert!(sat(&m, &amo1), "witness satisfies F");
assert_eq!(m.iter().filter(|&&b| b).count(), 1, "witness has weight 1");
let (with, without) = optimize_enumeration_counts(4, &amo1, &w1);
assert!(with < without, "symmetry must shrink the enumeration: {with} < {without}");
assert_eq!(optimize_modulo_symmetry(2, &[vec![p(0)], vec![Lit::new(0, false)]], &[1, 1]), None);
let w_distinct = vec![1i64, 2, 3, 4];
assert!(optimization_symmetry_generators(4, &amo1, &w_distinct).is_empty(), "distinct weights ⇒ no sym");
let (wa, wo) = optimize_enumeration_counts(4, &amo1, &w_distinct);
assert_eq!(wa, wo, "no usable symmetry ⇒ no reduction");
fn xs(s: &mut u64) -> u64 {
*s ^= *s << 13;
*s ^= *s >> 7;
*s ^= *s << 17;
*s
}
let nv = 4usize;
let mut seed = 0xC0FFEE_1234_5678u64;
for _ in 0..400 {
let m = (xs(&mut seed) % 5) as usize;
let f: Vec<Vec<Lit>> = (0..m)
.map(|_| {
let wclause = 1 + (xs(&mut seed) % 2) as usize;
(0..wclause).map(|_| Lit::new((xs(&mut seed) % nv as u64) as u32, xs(&mut seed) & 1 == 0)).collect()
})
.collect();
let weights: Vec<i64> = (0..nv).map(|_| (xs(&mut seed) % 5) as i64 - 2).collect();
let want = brute_min(nv, &f, &weights);
match optimize_modulo_symmetry(nv, &f, &weights) {
None => assert!(want.is_none(), "claimed UNSAT but a model exists: F={f:?}"),
Some((opt, wit)) => {
assert_eq!(Some(opt), want, "optimum must match brute force: F={f:?} w={weights:?}");
assert!(sat(&wit, &f), "witness must satisfy F");
let ww: i64 = (0..nv).filter(|&i| wit[i]).map(|i| weights[i]).sum();
assert_eq!(ww, opt, "witness must achieve the optimum");
}
}
}
}
#[test]
fn fractional_automorphism_is_a_doubly_stochastic_commuting_relaxation() {
let edge = |a: u32, b: u32| vec![Lit::new(a, true), Lit::new(b, true)];
let (php, _) = crate::families::php(4);
let (clq, _) = crate::families::clique_coloring(3, 3);
let c6: Vec<Vec<Lit>> = (0..6).map(|i| edge(i, (i + 1) % 6)).collect();
for (nv, cl) in [(php.num_vars, php.clauses.clone()), (clq.num_vars, clq.clauses.clone()), (6, c6.clone())] {
let part = fractional_automorphism(nv, &cl);
assert!(is_fractional_automorphism(nv, &cl, &part), "the equitable partition commutes with A");
let cells = part.iter().copied().max().map_or(0, |m| m + 1);
assert!(cells < nv, "a non-discrete partition ⇒ a genuine (non-permutation) fractional automorphism");
let gens = crate::sym_break::variable_automorphism_generators(nv, &cl).unwrap_or_default();
for orbit in crate::permgroup::orbits(nv, &gens) {
assert!(orbit.iter().all(|&v| part[v] == part[orbit[0]]), "orbit ⊆ fractional-automorphism cell");
}
}
let (nv, _) = (clq.num_vars, ());
assert!(is_fractional_automorphism(nv, &clq.clauses, &(0..nv).collect::<Vec<_>>()), "identity is a fractional automorphism");
let p4 = vec![edge(0, 1), edge(1, 2), edge(2, 3)];
assert!(!is_fractional_automorphism(4, &p4, &[0, 0, 1, 1]), "a non-equitable partition is rejected");
assert!(is_fractional_automorphism(4, &p4, &[0, 1, 1, 0]), "the reflection partition is equitable");
assert_eq!(fractional_automorphism(4, &p4), vec![0, 1, 1, 0], "P₄'s coarsest equitable partition is the reflection");
fn xs(s: &mut u64) -> u64 {
*s ^= *s << 13;
*s ^= *s >> 7;
*s ^= *s << 17;
*s
}
let n = 5usize;
let mut seed = 0x0FAC_0000_1234_9999u64;
for _ in 0..200 {
let m = (xs(&mut seed) % 6) as usize;
let cl: Vec<Vec<Lit>> = (0..m)
.map(|_| {
let w = 1 + (xs(&mut seed) % 3) as usize;
(0..w).map(|_| Lit::new((xs(&mut seed) % n as u64) as u32, xs(&mut seed) & 1 == 0)).collect()
})
.collect();
let part = fractional_automorphism(n, &cl);
assert!(is_fractional_automorphism(n, &cl, &part), "canonical partition must always commute: {cl:?}");
}
}
#[test]
fn color_refinement_over_approximates_the_orbit_partition() {
let p = |v: u32| Lit::new(v, true);
let (php, _) = crate::families::php(4);
assert_eq!(color_refinement_cells(php.num_vars, &php.clauses), 1, "PHP(4) variables are all alike");
let (clq, _) = crate::families::clique_coloring(3, 3);
assert_eq!(color_refinement_cells(clq.num_vars, &clq.clauses), 1, "clique(3,3) variables are all alike");
let f = vec![vec![p(0)], vec![p(1), p(2)]]; let cells = color_refinement(3, &f);
assert_ne!(cells[0], cells[1], "the unit variable is distinguished from the binary pair");
assert_eq!(cells[1], cells[2], "x1 and x2 are interchangeable");
assert_eq!(provably_asymmetric_variables(3, &f), vec![0], "x0 is provably fixed by every automorphism");
for g in crate::sym_break::variable_automorphism_generators(3, &f).unwrap_or_default() {
assert_eq!(g[0], 0, "an automorphism must fix the provably-asymmetric variable");
}
let check = |nv: usize, cl: &[Vec<Lit>]| {
let gens = crate::sym_break::variable_automorphism_generators(nv, cl).unwrap_or_default();
let orbits = crate::permgroup::orbits(nv, &gens);
let cells = color_refinement(nv, cl);
for orbit in &orbits {
let c0 = cells[orbit[0]];
assert!(orbit.iter().all(|&v| cells[v] == c0), "orbit {orbit:?} must be monochromatic: {cells:?}");
}
assert!(
color_refinement_cells(nv, cl) <= orbits.len(),
"the equitable partition is coarser than the orbit partition"
);
};
check(php.num_vars, &php.clauses);
check(clq.num_vars, &clq.clauses);
check(3, &f);
fn xs(s: &mut u64) -> u64 {
*s ^= *s << 13;
*s ^= *s >> 7;
*s ^= *s << 17;
*s
}
let nv = 5usize;
let mut seed = 0xA5A5_1234_DEAD_BEEFu64;
for _ in 0..200 {
let m = (xs(&mut seed) % 6) as usize;
let cl: Vec<Vec<Lit>> = (0..m)
.map(|_| {
let w = 1 + (xs(&mut seed) % 3) as usize;
(0..w).map(|_| Lit::new((xs(&mut seed) % nv as u64) as u32, xs(&mut seed) & 1 == 0)).collect()
})
.collect();
check(nv, &cl);
}
}
#[test]
fn two_wl_over_approximates_orbitals_and_beats_one_wl() {
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)];
let two_tri = vec![edge(0, 1), edge(1, 2), edge(0, 2), edge(3, 4), edge(4, 5), edge(3, 5)];
assert_eq!(color_refinement_cells(6, &c6), 1, "1-WL: C₆ is one cell");
assert_eq!(color_refinement_cells(6, &two_tri), 1, "1-WL: 2·C₃ is one cell — same as C₆");
assert_ne!(
two_wl_fingerprint(6, &c6),
two_wl_fingerprint(6, &two_tri),
"2-WL SEPARATES C₆ from 2·C₃ where 1-WL cannot"
);
let diag_refines_1wl = |nv: usize, cl: &[Vec<Lit>]| {
let wl1 = color_refinement(nv, cl);
let pc = two_wl_pair_colors(nv, cl);
for a in 0..nv {
for b in 0..nv {
if pc[a][a] == pc[b][b] {
assert_eq!(wl1[a], wl1[b], "2-WL diagonal must refine 1-WL");
}
}
}
};
diag_refines_1wl(6, &c6);
diag_refines_1wl(6, &two_tri);
let check = |nv: usize, cl: &[Vec<Lit>]| {
let gens = crate::sym_break::variable_automorphism_generators(nv, cl).unwrap_or_default();
let orbitals = crate::permgroup::orbitals(nv, &gens);
let pc = two_wl_pair_colors(nv, cl);
for orbital in &orbitals {
let (i0, j0) = orbital[0];
let c0 = pc[i0][j0];
assert!(orbital.iter().all(|&(i, j)| pc[i][j] == c0), "orbital must be monochromatic");
}
assert!(two_wl_pair_cells(nv, cl) <= orbitals.len(), "pair-cells ≤ orbitals");
};
let (php, _) = crate::families::php(4);
let (clq, _) = crate::families::clique_coloring(3, 3);
check(php.num_vars, &php.clauses);
check(clq.num_vars, &clq.clauses);
check(6, &c6);
check(6, &two_tri);
assert_eq!(color_refinement_cells(clq.num_vars, &clq.clauses), 1);
assert!(two_wl_pair_cells(clq.num_vars, &clq.clauses) >= 4, "2-WL sees the 4 orbitals of the grid");
fn xs(s: &mut u64) -> u64 {
*s ^= *s << 13;
*s ^= *s >> 7;
*s ^= *s << 17;
*s
}
let nv = 5usize;
let mut seed = 0x2B0C_1A7E_55AA_F00Du64;
for _ in 0..120 {
let m = (xs(&mut seed) % 6) as usize;
let cl: Vec<Vec<Lit>> = (0..m)
.map(|_| {
let w = 1 + (xs(&mut seed) % 3) as usize;
(0..w).map(|_| Lit::new((xs(&mut seed) % nv as u64) as u32, xs(&mut seed) & 1 == 0)).collect()
})
.collect();
check(nv, &cl);
}
}
#[test]
fn association_scheme_multiplicities_are_the_eigenspace_dimensions() {
let edge = |a: u32, b: u32| vec![Lit::new(a, true), Lit::new(b, true)];
let (clq, _) = crate::families::clique_coloring(3, 3);
let c6: Vec<Vec<Lit>> = (0..6).map(|i| edge(i, (i + 1) % 6)).collect();
assert_eq!(
association_scheme_multiplicities(clq.num_vars, &clq.clauses),
Some(vec![1, 2, 2, 4]),
"clique(3,3): eigenspace dimensions = S₃×S₃ constituent degrees"
);
for (nv, cl) in [(clq.num_vars, clq.clauses.clone()), (6, c6.clone())] {
let m = association_scheme_multiplicities(nv, &cl).expect("commutative scheme has multiplicities");
assert_eq!(m.iter().sum::<u128>(), nv as u128, "Σ multiplicities = number of vertices");
assert!(m.iter().all(|&x| x >= 1), "each eigenspace is non-empty");
assert_eq!(m[0], 1, "the smallest (trivial) eigenspace has dimension 1");
assert_eq!(m.len(), coherent_rank(nv, &cl).unwrap(), "one multiplicity per eigenspace");
}
}
#[test]
fn association_scheme_eigenmatrix_is_the_scheme_character_table() {
let edge = |a: u32, b: u32| vec![Lit::new(a, true), Lit::new(b, true)];
let (clq, _) = crate::families::clique_coloring(3, 3);
let c6: Vec<Vec<Lit>> = (0..6).map(|i| edge(i, (i + 1) % 6)).collect();
assert_eq!(coherent_rank(clq.num_vars, &clq.clauses), Some(4), "clique(3,3): 4 relations");
for (nv, cl) in [(clq.num_vars, clq.clauses.clone()), (6, c6.clone())] {
let d = coherent_rank(nv, &cl).unwrap();
let (p, pm) = association_scheme_eigenmatrix(nv, &cl).expect("a commutative scheme has an eigenmatrix");
assert_eq!(pm.len(), d, "P has one row per common eigenspace (d × d)");
assert!(pm.iter().all(|r| r.len() == d));
let (_, a) = coherent_configuration_constants(nv, &cl).unwrap();
for row in &pm {
for i in 0..d {
for j in 0..d {
let lhs = row[i] as u128 * row[j] as u128 % p as u128;
let rhs = (0..d)
.map(|k| (a[i][j][k] % p as u128) * row[k] as u128 % p as u128)
.sum::<u128>()
% p as u128;
assert_eq!(lhs, rhs, "row must be an algebra homomorphism");
}
}
}
let valency: Vec<u128> = (0..d).map(|i| (0..d).map(|j| a[i][j][0]).sum()).collect();
assert_eq!(valency.iter().sum::<u128>(), nv as u128, "Σ valencies = number of vertices");
assert!(valency.contains(&1), "the diagonal relation has valency 1");
assert!(
pm.iter().any(|row| (0..d).all(|i| row[i] as u128 == valency[i] % p as u128)),
"the valency vector is a row of P (the trivial eigenspace)"
);
}
}
#[test]
fn coherent_configuration_is_a_genuine_association_scheme() {
let edge = |a: u32, b: u32| vec![Lit::new(a, true), Lit::new(b, true)];
let (php, _) = crate::families::php(4);
let (clq, _) = crate::families::clique_coloring(3, 3);
let c6 = vec![edge(0, 1), edge(1, 2), edge(2, 3), edge(3, 4), edge(4, 5), edge(5, 0)];
let check = |nv: usize, cl: &[Vec<Lit>]| {
let (d, p) = coherent_configuration_constants(nv, cl).expect("2-WL is coherent");
assert_eq!(d, two_wl_pair_cells(nv, cl), "rank = number of basis relations");
for k in 0..d {
let total: u128 = (0..d).flat_map(|i| (0..d).map(move |j| (i, j))).map(|(i, j)| p[i][j][k]).sum();
assert_eq!(total, nv as u128, "Σ_ij p[i][j][k] counts all n intermediate points");
}
let pc = two_wl_pair_colors(nv, cl);
let mut transpose = vec![usize::MAX; d];
for i in 0..nv {
for j in 0..nv {
let (r, rt) = (pc[i][j], pc[j][i]);
if transpose[r] == usize::MAX {
transpose[r] = rt;
} else {
assert_eq!(transpose[r], rt, "R_r^T must be a single relation");
}
}
}
d
};
check(php.num_vars, &php.clauses);
let dclq = check(clq.num_vars, &clq.clauses);
check(6, &c6);
assert_eq!(dclq, 4, "the rook's graph scheme has 4 relations");
let clq_gens = crate::sym_break::variable_automorphism_generators(clq.num_vars, &clq.clauses).unwrap();
assert_eq!(dclq, crate::permgroup::orbitals(clq.num_vars, &clq_gens).len(), "Schurian: relations = orbitals");
let pc6 = two_wl_pair_colors(6, &c6);
let (_d6, p6) = coherent_configuration_constants(6, &c6).unwrap();
let adj = pc6[0][1];
let dist2 = pc6[0][2];
assert_ne!(adj, dist2, "2-WL separates adjacency from distance-2 in C₆");
assert_eq!(p6[adj][adj][dist2], 1, "C₆: vertices at distance 2 share exactly one common neighbour");
fn xs(s: &mut u64) -> u64 {
*s ^= *s << 13;
*s ^= *s >> 7;
*s ^= *s << 17;
*s
}
let nv = 5usize;
let mut seed = 0x0C0E_4E17_C0FF_EE00u64;
for _ in 0..100 {
let m = (xs(&mut seed) % 6) as usize;
let cl: Vec<Vec<Lit>> = (0..m)
.map(|_| {
let w = 1 + (xs(&mut seed) % 3) as usize;
(0..w).map(|_| Lit::new((xs(&mut seed) % nv as u64) as u32, xs(&mut seed) & 1 == 0)).collect()
})
.collect();
assert!(coherent_configuration_constants(nv, &cl).is_some(), "2-WL must always be coherent");
}
}
#[test]
fn three_wl_over_approximates_3_orbits_and_beats_two_wl() {
let edge = |a: usize, b: usize| vec![Lit::new(a as u32, true), Lit::new(b as u32, true)];
let cayley = |conn: &[(i32, i32)]| -> Vec<Vec<Lit>> {
let idx = |r: i32, c: i32| (((r.rem_euclid(4)) * 4 + c.rem_euclid(4)) as usize);
let mut edges = std::collections::BTreeSet::new();
for r in 0..4 {
for c in 0..4 {
for &(dr, dc) in conn {
let (a, b) = (idx(r, c), idx(r + dr, c + dc));
if a < b {
edges.insert((a, b));
}
}
}
}
edges.into_iter().map(|(a, b)| edge(a, b)).collect()
};
let rook = cayley(&[(1, 0), (2, 0), (3, 0), (0, 1), (0, 2), (0, 3)]);
let shrikhande = cayley(&[(1, 0), (3, 0), (0, 1), (0, 3), (1, 1), (3, 3)]);
assert_eq!(
two_wl_fingerprint(16, &rook),
two_wl_fingerprint(16, &shrikhande),
"2-WL cannot separate two SRG(16,6,2,2) graphs"
);
assert_ne!(
three_wl_fingerprint(16, &rook),
three_wl_fingerprint(16, &shrikhande),
"3-WL SEPARATES the rook's graph from the Shrikhande graph"
);
let check = |nv: usize, cl: &[Vec<Lit>]| {
let gens = crate::sym_break::variable_automorphism_generators(nv, cl).unwrap_or_default();
let tw = three_wl_colors(nv, cl);
for orbit in crate::permgroup::orbits_on_tuples(nv, &gens, 3) {
let t0 = &orbit[0];
let c0 = tw[t0[0]][t0[1]][t0[2]];
assert!(orbit.iter().all(|t| tw[t[0]][t[1]][t[2]] == c0), "3-orbit must be monochromatic");
}
};
let (clq, _) = crate::families::clique_coloring(3, 3);
let c6: Vec<Vec<Lit>> = (0..6).map(|i| edge(i, (i + 1) % 6)).collect();
check(clq.num_vars, &clq.clauses);
check(6, &c6);
fn xs(s: &mut u64) -> u64 {
*s ^= *s << 13;
*s ^= *s >> 7;
*s ^= *s << 17;
*s
}
let nv = 5usize;
let mut seed = 0x33C0_FFEE_0033_0033u64;
for _ in 0..60 {
let m = (xs(&mut seed) % 6) as usize;
let cl: Vec<Vec<Lit>> = (0..m)
.map(|_| {
let w = 1 + (xs(&mut seed) % 3) as usize;
(0..w).map(|_| Lit::new((xs(&mut seed) % nv as u64) as u32, xs(&mut seed) & 1 == 0)).collect()
})
.collect();
check(nv, &cl);
}
}
#[test]
fn canonical_form_decides_formula_isomorphism() {
let edge = |a: usize, b: usize| vec![Lit::new(a as u32, true), Lit::new(b as u32, true)];
let relabel = |cl: &[Vec<Lit>], perm: &[usize]| -> Vec<Vec<Lit>> {
cl.iter()
.map(|c| c.iter().map(|l| Lit::new(perm[l.var() as usize] as u32, l.is_positive())).collect())
.collect()
};
let c6: Vec<Vec<Lit>> = (0..6).map(|i| edge(i, (i + 1) % 6)).collect();
let perm = [3usize, 5, 0, 2, 4, 1];
assert_eq!(
canonical_form(6, &c6),
canonical_form(6, &relabel(&c6, &perm)),
"isomorphic formulas share a canonical form"
);
assert_eq!(formulas_isomorphic(6, &c6, &relabel(&c6, &perm)), Some(true));
let two_tri = vec![edge(0, 1), edge(1, 2), edge(0, 2), edge(3, 4), edge(4, 5), edge(3, 5)];
assert_eq!(color_refinement_cells(6, &c6), color_refinement_cells(6, &two_tri), "1-WL cannot tell them apart");
assert_eq!(formulas_isomorphic(6, &c6, &two_tri), Some(false), "but canonical form CAN");
assert_ne!(canonical_form(6, &c6), canonical_form(6, &two_tri));
let path4 = vec![edge(0, 1), edge(1, 2), edge(2, 3)];
let star4 = vec![edge(0, 1), edge(0, 2), edge(0, 3)];
assert_eq!(formulas_isomorphic(4, &path4, &star4), Some(false));
fn xs(s: &mut u64) -> u64 {
*s ^= *s << 13;
*s ^= *s >> 7;
*s ^= *s << 17;
*s
}
let nv = 6usize;
let mut seed = 0xCA90_F00D_1234_5678u64;
for _ in 0..120 {
let m = (xs(&mut seed) % 7) as usize;
let f: Vec<Vec<Lit>> = (0..m)
.map(|_| {
let w = 1 + (xs(&mut seed) % 2) as usize;
(0..w).map(|_| Lit::new((xs(&mut seed) % nv as u64) as u32, xs(&mut seed) & 1 == 0)).collect()
})
.collect();
let mut perm: Vec<usize> = (0..nv).collect();
for i in (1..nv).rev() {
let j = (xs(&mut seed) % (i as u64 + 1)) as usize;
perm.swap(i, j);
}
let fp = relabel(&f, &perm);
assert_eq!(canonical_form(nv, &f), canonical_form(nv, &fp), "F ≅ π(F): F={f:?} perm={perm:?}");
assert_eq!(formulas_isomorphic(nv, &f, &fp), Some(true));
}
}
#[test]
fn weighted_model_count_is_exact_and_symmetry_accelerated() {
let p = |v: u32| Lit::new(v, true);
let nl = |v: u32| Lit::new(v, false);
let sat = |m: &[bool], cls: &[Vec<Lit>]| {
cls.iter().all(|c| c.iter().any(|l| m[l.var() as usize] == l.is_positive()))
};
let brute = |nv: usize, f: &[Vec<Lit>], w: &[(i64, i64)]| -> i128 {
(0u32..(1u32 << nv))
.filter_map(|x| {
let a: Vec<bool> = (0..nv).map(|i| (x >> i) & 1 == 1).collect();
sat(&a, f).then(|| (0..nv).map(|i| if a[i] { w[i].1 as i128 } else { w[i].0 as i128 }).product::<i128>())
})
.sum()
};
let amo = vec![vec![p(0), p(1), p(2)]]; let ones = vec![(1i64, 1i64); 3];
assert_eq!(weighted_model_count(3, &amo, &ones), 7, "unit weights ⇒ #models");
assert_eq!(weighted_model_count(3, &amo, &ones), brute(3, &amo, &ones));
let (solves, models) = weighted_model_count_solve_counts(3, &amo);
assert_eq!(models, 7, "7 models of at-least-one-of-3");
assert!(solves < models, "symmetry must reduce the solves: {solves} < {models}");
let w_sym = vec![(2i64, 3i64); 3];
assert_eq!(weighted_model_count(3, &amo, &w_sym), brute(3, &amo, &w_sym));
assert_eq!(weighted_model_count(2, &[vec![p(0)], vec![nl(0)]], &[(1, 1), (1, 1)]), 0);
fn xs(s: &mut u64) -> u64 {
*s ^= *s << 13;
*s ^= *s >> 7;
*s ^= *s << 17;
*s
}
let nv = 4usize;
let mut seed = 0x5EED_4321_FACE_0001u64;
for _ in 0..200 {
let m = (xs(&mut seed) % 5) as usize;
let f: Vec<Vec<Lit>> = (0..m)
.map(|_| {
let wd = 1 + (xs(&mut seed) % 2) as usize;
(0..wd).map(|_| Lit::new((xs(&mut seed) % nv as u64) as u32, xs(&mut seed) & 1 == 0)).collect()
})
.collect();
let w: Vec<(i64, i64)> = (0..nv).map(|_| ((xs(&mut seed) % 4) as i64, (xs(&mut seed) % 4) as i64)).collect();
assert_eq!(weighted_model_count(nv, &f, &w), brute(nv, &f, &w), "F={f:?} w={w:?}");
}
}
#[test]
fn assignment_weight_inventory_splits_orbits_by_weight() {
let (cnf, _) = crate::families::clique_coloring(3, 3);
let inv = assignment_weight_inventory(cnf.num_vars, &cnf.clauses).expect("enumerable group");
assert_eq!(inv.len(), 10, "weights 0..=9");
assert_eq!(inv.iter().sum::<u128>(), 36, "sums to the assignment-orbit count (36 binary 3×3 matrices)");
assert_eq!(inv[0], 1, "one all-false assignment");
assert_eq!(inv[1], 1, "all single-one matrices are row/column equivalent");
assert_eq!(inv[9], 1, "one all-true assignment");
assert_eq!(
Some(inv.iter().sum::<u128>()),
symmetry_structure(cnf.num_vars, &cnf.clauses).assignment_orbits,
"the inventory sums to the profile's assignment_orbits"
);
let asym = vec![vec![Lit::new(0, true)], vec![Lit::new(1, false), Lit::new(2, true)]];
assert_eq!(assignment_weight_inventory(3, &asym), Some(vec![1, 3, 3, 1]), "no symmetry ⇒ C(3,w)");
}
#[test]
fn pb_coefficient_symmetry_profiles_through_the_same_ladder() {
use crate::pseudo_boolean::PbConstraint;
let c = PbConstraint::new_weighted(&[(0, 3, true), (1, 3, true), (2, 3, true), (3, 5, true)], 6);
let prof = pb_symmetry_profile(4, &[c]);
assert_eq!(prof.order, 6, "S₃ on the three weight-3 variables");
assert_eq!(prof.num_orbits, 2, "two orbits: {{x0,x1,x2}} and the fixed point x3");
assert!(!prof.abelian, "S₃ is non-abelian");
assert_eq!(prof.solvable, Some(true), "S₃ is solvable");
assert_eq!(prof.coherent_rank, None, "the coefficient profile has no clauses ⇒ no scheme rank");
let distinct = PbConstraint::new_weighted(&[(0, 1, true), (1, 2, true), (2, 3, true)], 3);
assert_eq!(pb_symmetry_profile(3, &[distinct]).order, 1, "distinct weights ⇒ trivial group");
}
#[test]
fn symmetry_structure_profiles_the_variable_group() {
let p = |v| Lit::new(v, true);
let n = |v| Lit::new(v, false);
let exactly1 = vec![
vec![p(0), p(1), p(2)],
vec![n(0), n(1)], vec![n(0), n(2)], vec![n(1), n(2)],
];
let prof = symmetry_structure(3, &exactly1);
assert_eq!(prof.order, 6, "|S₃| = 6");
assert_eq!(prof.num_orbits, 1, "transitive on the 3 cells");
assert_eq!(prof.rank, 2, "S₃ is 2-transitive ⇒ rank 2");
assert_eq!(prof.coherent_rank, Some(2), "coherent (scheme) rank matches the orbital rank here");
assert!(prof.coherent_rank.unwrap() <= prof.rank, "coherent rank ≤ orbital rank");
assert_eq!(prof.transitivity, 3, "S₃ is 3-transitive on 3 points");
assert!(prof.primitive, "S₃ on 3 points is primitive");
assert_eq!(prof.blocks, None, "a primitive group has no block system");
assert!(!prof.abelian, "S₃ is non-abelian");
assert_eq!(prof.solvable, Some(true), "S₃ is solvable");
assert_eq!(prof.nilpotent, Some(false), "S₃ is solvable but NOT nilpotent");
assert_eq!(prof.derived_length, Some(2), "S₃ has derived length 2");
assert_eq!(prof.nilpotency_class, None, "S₃ is not nilpotent ⇒ no nilpotency class");
assert_eq!(prof.derived_order, 3, "[S₃,S₃] = A₃ has order 3");
assert_eq!(prof.conjugacy_classes, Some(3), "S₃ has 3 conjugacy classes (= 3 irreps)");
assert_eq!(prof.center_order, Some(1), "S₃ has a trivial centre");
assert_eq!(prof.exponent, Some(6), "S₃ has exponent 6 (lcm of orders 1,2,3)");
assert_eq!(prof.subgroups, Some(6), "S₃ has 6 subgroups");
assert_eq!(prof.simple, Some(false), "S₃ is not simple (A₃ is normal)");
assert_eq!(prof.composition_factors, Some(vec![2, 3]), "S₃ = C₂, C₃");
assert_eq!(prof.sylow, Some(vec![(2, 3), (3, 1)]), "S₃: 3 Sylow-2, 1 Sylow-3");
assert_eq!(prof.real_classes, Some(3), "S₃: all 3 classes (= irreps) are real");
assert_eq!(prof.rational_classes, Some(3), "S₃ is rational: all 3 classes rational");
assert_eq!(prof.automorphism_order, Some(6), "|Aut(S₃)| = 6 (S₃ is complete)");
assert_eq!(prof.outer_automorphism_order, Some(1), "Out(S₃) = 1");
assert_eq!(prof.irreducible_degrees, Some(vec![1, 1, 2]), "S₃ irreps: trivial, sign, 2-dim standard");
assert_eq!(prof.frobenius_schur, Some(vec![1, 1, 1]), "S₃ is totally real ⇒ all indicators +1");
{
let iso = prof.isotypic_multiplicities.as_ref().expect("S₃ isotypic decomposition");
let degs = prof.irreducible_degrees.as_ref().unwrap();
assert_eq!(iso.iter().zip(degs).map(|(m, d)| m * d).sum::<u128>(), 3, "Σ m·d = 3 variables");
assert_eq!(iso.iter().map(|m| m * m).sum::<u128>(), prof.rank as u128, "Σ m² = rank");
}
let (clique, _) = crate::families::clique_coloring(3, 3);
let cp = symmetry_structure(clique.num_vars, &clique.clauses);
assert_eq!(cp.order, 36, "|S₃ × S₃| = 36");
assert_eq!(cp.num_orbits, 1, "transitive on the 9 cells");
assert_eq!(cp.rank, 4, "the grid action has rank 4");
assert_eq!(cp.coherent_rank, Some(4), "clique(3,3): the coherent scheme has 4 relations");
assert_eq!(cp.transitivity, 1, "transitive but not 2-transitive");
assert!(!cp.primitive, "the grid action is imprimitive");
assert!(cp.blocks.is_some(), "rows/columns form a block system");
assert!(!cp.abelian, "S₃ × S₃ is non-abelian");
assert_eq!(cp.solvable, Some(true), "S₃ × S₃ is solvable");
assert_eq!(cp.nilpotent, Some(false), "S₃ × S₃ is not nilpotent (S₃ isn't)");
assert_eq!(cp.derived_order, 9, "[S₃×S₃, S₃×S₃] = A₃ × A₃ has order 9");
assert_eq!(cp.conjugacy_classes, Some(9), "S₃×S₃ has 3·3 = 9 conjugacy classes");
assert_eq!(cp.center_order, Some(1), "S₃×S₃ has a trivial centre");
assert_eq!(cp.rational_classes, Some(9), "S₃×S₃ is rational: all 9 classes rational");
assert_eq!(cp.automorphism_order, Some(72), "|Aut(S₃×S₃)| = 72");
assert_eq!(cp.outer_automorphism_order, Some(2), "Out(S₃×S₃) = C₂ (factor swap)");
assert_eq!(cp.assignment_orbits, Some(36), "2⁹ assignments up to S₃×S₃ = 36 binary 3×3 matrices");
assert_eq!(cp.abelianization, Some((4, 2)), "(S₃×S₃)ᵃᵇ = C₂×C₂ (order 4, exponent 2)");
assert!(cp.subgroups.is_some(), "the S₃×S₃ subgroup lattice is computed");
assert_eq!(cp.simple, Some(false), "S₃×S₃ is not simple");
assert_eq!(cp.composition_factors, Some(vec![2, 2, 3, 3]), "S₃×S₃ = C₂², C₃² (product 36)");
assert_eq!(cp.sylow, Some(vec![(2, 9), (3, 1)]), "S₃×S₃: 3² = 9 Sylow-2, 1 Sylow-3");
assert_eq!(
cp.irreducible_degrees,
Some(vec![1, 1, 1, 1, 2, 2, 2, 2, 4]),
"S₃×S₃ irreps = products of the S₃ irreps"
);
assert_eq!(
cp.frobenius_schur,
Some(vec![1, 1, 1, 1, 1, 1, 1, 1, 1]),
"S₃×S₃ is totally real ⇒ all nine indicators +1"
);
{
let iso = cp.isotypic_multiplicities.as_ref().expect("S₃×S₃ isotypic decomposition");
let degs = cp.irreducible_degrees.as_ref().unwrap();
assert_eq!(iso.iter().zip(degs).map(|(m, d)| m * d).sum::<u128>(), 9, "Σ m·d = 9 cells");
assert_eq!(iso.iter().map(|m| m * m).sum::<u128>(), cp.rank as u128, "⟨π,π⟩ = rank = 4");
}
let asym = vec![vec![p(0)], vec![n(1), p(2)]];
let ap = symmetry_structure(3, &asym);
assert_eq!(ap.order, 1, "no symmetry ⇒ trivial group");
assert!(ap.coherent_rank.is_some(), "the scheme rank is always computed from the clauses");
assert_eq!(ap.irreducible_degrees, Some(vec![1]), "trivial group: one trivial irreducible");
assert_eq!(ap.frobenius_schur, Some(vec![1]), "trivial group: its character is real");
assert_eq!(
ap.isotypic_multiplicities,
Some(vec![3]),
"trivial group on 3 vars: the perm rep is 3 copies of the trivial irreducible"
);
assert_eq!(ap.rational_classes, Some(1), "trivial group: its one class is rational");
assert_eq!(ap.automorphism_order, Some(1), "trivial group: Aut is trivial");
assert_eq!(ap.outer_automorphism_order, Some(1), "trivial group: Out is trivial");
}
#[test]
fn models_up_to_symmetry_enumerates_orbits_and_counts_exactly() {
let p = |v| Lit::new(v, true);
let n = |v| Lit::new(v, false);
let oracle = |nv: usize, cl: &[Vec<Lit>]| -> (u128, usize) {
let models: Vec<Vec<bool>> = (0u64..(1u64 << nv))
.filter_map(|x| {
let a: Vec<bool> = (0..nv).map(|i| (x >> i) & 1 == 1).collect();
cl.iter().all(|c| c.iter().any(|l| a[l.var() as usize] == l.is_positive())).then_some(a)
})
.collect();
let gens = crate::sym_break::variable_automorphism_generators(nv, cl).unwrap_or_default();
let model_set: std::collections::HashSet<Vec<bool>> = models.iter().cloned().collect();
let mut seen = std::collections::HashSet::new();
let mut orbits = 0;
for m in &models {
if seen.contains(m) {
continue;
}
orbits += 1;
let mut stack = vec![m.clone()];
while let Some(cur) = stack.pop() {
if !seen.insert(cur.clone()) {
continue;
}
for g in &gens {
let mut pm = vec![false; nv];
for v in 0..nv {
pm[g[v]] = cur[v];
}
if model_set.contains(&pm) && !seen.contains(&pm) {
stack.push(pm);
}
}
}
}
(models.len() as u128, orbits)
};
let exactly1 = vec![
vec![p(0), p(1), p(2)],
vec![n(0), n(1)], vec![n(0), n(2)], vec![n(1), n(2)],
];
let atmost1 = vec![vec![n(0), n(1)], vec![n(0), n(2)], vec![n(1), n(2)]];
for cl in [&exactly1, &atmost1] {
let (m_exact, m_orbits) = oracle(3, cl);
let sc = models_up_to_symmetry(3, cl, 1000);
assert!(sc.exhaustive, "the small instance is enumerated to exhaustion");
assert_eq!(sc.total_models, m_exact, "exact model count = sum of orbit sizes");
assert_eq!(sc.representatives.len(), m_orbits, "one representative per orbit");
if let Some(burnside) = crate::sym_break::count_models_modulo_symmetry(3, cl) {
assert_eq!(sc.representatives.len(), burnside, "enumeration agrees with Burnside");
}
for r in &sc.representatives {
assert!(cl.iter().all(|c| c.iter().any(|l| r[l.var() as usize] == l.is_positive())), "valid model");
}
let distinct: std::collections::HashSet<&Vec<bool>> = sc.representatives.iter().collect();
assert_eq!(distinct.len(), sc.representatives.len(), "representatives are distinct");
}
assert_eq!(models_up_to_symmetry(3, &exactly1, 1000).total_models, 3);
assert_eq!(models_up_to_symmetry(3, &exactly1, 1000).representatives.len(), 1);
assert_eq!(models_up_to_symmetry(3, &atmost1, 1000).total_models, 4);
assert_eq!(models_up_to_symmetry(3, &atmost1, 1000).representatives.len(), 2);
}
#[test]
fn declared_symmetry_is_verified_then_broken() {
let p = |v| Lit::new(v, true);
let brute = |cl: &[Vec<Lit>], nv: usize| {
(0u64..(1u64 << nv)).any(|x| {
let a: Vec<bool> = (0..nv).map(|i| (x >> i) & 1 == 1).collect();
cl.iter().all(|c| c.iter().any(|l| a[l.var() as usize] == l.is_positive()))
})
};
let (cnf, _) = crate::families::clique_coloring(3, 3);
let nv = cnf.num_vars;
let mut vswap: Vec<usize> = (0..nv).collect();
for c in 0..3 {
vswap.swap(c, 3 + c);
}
assert!(is_declared_symmetry(nv, &cnf.clauses, &vswap), "a vertex swap is a genuine clique symmetry");
let s = solve_with_declared_symmetry(nv, &cnf.clauses, &[vswap]);
assert_eq!(s.via, Route::DeclaredSymmetry);
match &s.answer {
Answer::Sat(m) => assert!(cnf.clauses.iter().all(|c| c.iter().any(|l| m[l.var() as usize] == l.is_positive()))),
Answer::Unsat => panic!("clique_coloring(3,3) is SAT"),
}
let mut bogus: Vec<usize> = (0..nv).collect();
bogus.swap(0, 5); assert!(!is_declared_symmetry(nv, &cnf.clauses, &bogus), "a non-symmetry must be rejected");
let wb = solve_with_declared_symmetry(nv, &cnf.clauses, &[bogus]);
assert!(matches!(wb.answer, Answer::Sat(_)), "a bogus declaration must not corrupt the SAT verdict");
if let Answer::Sat(m) = &wb.answer {
assert!(cnf.clauses.iter().all(|c| c.iter().any(|l| m[l.var() as usize] == l.is_positive())));
}
let f = vec![vec![p(0), p(2)], vec![p(1), p(2)], vec![p(0), p(2), p(3)]];
let mut ab: Vec<usize> = (0..4).collect();
ab.swap(0, 1);
assert!(is_declared_symmetry(4, &f, &ab), "a↔b is a semantic symmetry, verified by implication");
let sem = solve_with_declared_symmetry(4, &f, &[ab]);
assert_eq!(sem.via, Route::DeclaredSymmetry);
assert_eq!(matches!(sem.answer, Answer::Sat(_)), brute(&f, 4), "declared-symmetry verdict matches brute force");
assert!(!is_declared_symmetry(4, &f, &[0usize, 1]), "a wrong-length permutation is rejected");
let mf = solve_with_declared_symmetry(4, &f, &[vec![0usize, 1]]);
assert_eq!(
matches!(mf.answer, Answer::Sat(_)),
matches!(solve_comprehensive(4, &f).answer, Answer::Sat(_)),
"a malformed declaration is dropped, verdict unchanged"
);
}
#[test]
fn almost_symmetry_breaks_a_near_miss_conditionally() {
let p = |v| Lit::new(v, true);
let brute = |cl: &[Vec<Lit>], nv: usize| {
(0u64..(1u64 << nv)).any(|x| {
let a: Vec<bool> = (0..nv).map(|i| (x >> i) & 1 == 1).collect();
cl.iter().all(|c| c.iter().any(|l| a[l.var() as usize] == l.is_positive()))
})
};
let f = vec![vec![p(0), p(2)], vec![p(1), p(2)], vec![p(0), p(3)]];
let (sem, _) = semantic_symmetry_pairs(4, &f);
assert!(!sem.contains(&(0, 1)), "a,b is not a SEMANTIC symmetry here: {sem:?}");
let almost = almost_symmetry_pairs(4, &f, 2);
assert!(
almost.iter().any(|(a, b, imgs)| *a == 0 && *b == 1 && imgs.len() == 1),
"a↔b breaks exactly one clause: {almost:?}"
);
let s = almost_symmetry_solve(4, &f).expect("an almost-symmetry is detected and conditionally broken");
assert_eq!(s.via, Route::AlmostSymmetry);
assert_eq!(matches!(s.answer, Answer::Sat(_)), brute(&f, 4), "almost-symmetry verdict matches brute force");
if let Answer::Sat(m) = &s.answer {
assert!(f.iter().all(|c| c.iter().any(|l| m[l.var() as usize] == l.is_positive())), "valid model");
}
let mut un = f.clone();
un.extend([
vec![Lit::new(0, false)],
vec![Lit::new(1, false)],
vec![Lit::new(2, false)],
vec![Lit::new(3, false)],
]);
let u = almost_symmetry_solve(4, &un).expect("almost-symmetry still detected");
assert_eq!(u.via, Route::AlmostSymmetry);
assert!(matches!(u.answer, Answer::Unsat), "all variables off makes (a∨x) UNSAT");
assert_eq!(matches!(u.answer, Answer::Sat(_)), brute(&un, 4), "UNSAT verdict matches brute force");
}
#[test]
fn semantic_symmetry_breaks_a_non_syntactic_interchange() {
let p = |v| Lit::new(v, true);
let f = vec![vec![p(0), p(2)], vec![p(1), p(2)], vec![p(0), p(2), p(3)]];
let (pairs, non_syntactic) = semantic_symmetry_pairs(4, &f);
assert!(pairs.contains(&(0, 1)) && non_syntactic, "a,b are a semantic, non-syntactic symmetry: {pairs:?}");
let canon_set = |swap: bool| -> std::collections::HashSet<Vec<(u32, bool)>> {
f.iter()
.map(|c| {
let mut k: Vec<(u32, bool)> = c
.iter()
.map(|l| {
let v = l.var() as usize;
let nv = if swap && v == 0 { 1 } else if swap && v == 1 { 0 } else { v };
(nv as u32, l.is_positive())
})
.collect();
k.sort_unstable();
k
})
.collect()
};
assert_ne!(canon_set(true), canon_set(false), "the a↔b swap changes the clause set — not syntactic");
let s = semantic_symmetry_solve(4, &f).expect("a semantic symmetry is detected and broken");
assert_eq!(s.via, Route::SemanticSymmetry);
let brute = (0u64..16).any(|x| {
let a: Vec<bool> = (0..4).map(|i| (x >> i) & 1 == 1).collect();
f.iter().all(|c| c.iter().any(|l| a[l.var() as usize] == l.is_positive()))
});
assert_eq!(matches!(s.answer, Answer::Sat(_)), brute, "semantic-symmetry verdict matches brute force");
if let Answer::Sat(m) = &s.answer {
assert!(f.iter().all(|c| c.iter().any(|l| m[l.var() as usize] == l.is_positive())), "valid model");
}
let syntactic = vec![vec![p(0), p(2)], vec![p(1), p(2)]];
assert!(
semantic_symmetry_solve(3, &syntactic).is_none(),
"a purely syntactic symmetry is left to the syntactic route"
);
}
#[test]
fn nested_block_tower_breaks_multidimensional_symmetry() {
let p = |v| Lit::new(v, true);
let brute = |nv: usize, cl: &[Vec<Lit>]| -> bool {
(0u64..(1u64 << nv)).any(|x| {
let a: Vec<bool> = (0..nv).map(|i| (x >> i) & 1 == 1).collect();
cl.iter().all(|c| c.iter().any(|l| a[l.var() as usize] == l.is_positive()))
})
};
let (sat, _) = crate::families::clique_coloring(3, 3);
let s = nested_symmetry_solve(sat.num_vars, &sat.clauses).expect("a grid symmetry has a block system");
assert_eq!(s.via, Route::NestedSymmetry);
match &s.answer {
Answer::Sat(m) => assert!(sat.clauses.iter().all(|c| c.iter().any(|l| m[l.var() as usize] == l.is_positive()))),
Answer::Unsat => panic!("clique_coloring(3,3) is SAT"),
}
assert_eq!(matches!(s.answer, Answer::Sat(_)), brute(sat.num_vars, &sat.clauses), "verdict matches brute");
let (unsat, _) = crate::families::clique_coloring(4, 3);
let u = nested_symmetry_solve(unsat.num_vars, &unsat.clauses).expect("a grid symmetry has a block system");
assert_eq!(u.via, Route::NestedSymmetry);
assert!(matches!(u.answer, Answer::Unsat), "clique_coloring(4,3) is UNSAT");
assert_eq!(matches!(u.answer, Answer::Sat(_)), brute(unsat.num_vars, &unsat.clauses), "verdict matches brute");
let mut cube: Vec<Vec<Lit>> = Vec::new();
for v in 0u32..8 {
for b in 0..3 {
let w = v ^ (1 << b);
if v < w {
cube.push(vec![p(v), p(w)]);
}
}
}
let c = nested_symmetry_solve(8, &cube).expect("the cube's nested block tower engages");
assert_eq!(c.via, Route::NestedSymmetry);
match &c.answer {
Answer::Sat(m) => assert!(cube.iter().all(|cl| cl.iter().any(|l| m[l.var() as usize] == l.is_positive()))),
Answer::Unsat => panic!("covering every cube edge is SAT (e.g. all true)"),
}
assert_eq!(matches!(c.answer, Answer::Sat(_)), brute(8, &cube), "the nested-tower verdict matches brute force");
}
#[test]
fn symmetry_revealed_by_simplification_is_unlocked_and_broken() {
let p = |v| Lit::new(v, true);
let n = |v| Lit::new(v, false);
let unlock = vec![vec![p(0)], vec![p(1), p(2), n(0)], vec![p(1), p(3)]];
let s = symmetry_via_simplification_solve(4, &unlock).expect("simplification unlocks symmetry");
assert_eq!(s.via, Route::SymmetrySimplify);
match &s.answer {
Answer::Sat(m) => {
assert!(unlock.iter().all(|c| c.iter().any(|l| m[l.var() as usize] == l.is_positive())));
assert!(m[0], "the forced literal x0 is re-applied to the model");
}
Answer::Unsat => panic!("the instance is SAT"),
}
let brute = (0u64..16).any(|x| {
let a: Vec<bool> = (0..4).map(|i| (x >> i) & 1 == 1).collect();
unlock.iter().all(|c| c.iter().any(|l| a[l.var() as usize] == l.is_positive()))
});
assert_eq!(matches!(s.answer, Answer::Sat(_)), brute, "verdict matches brute force");
let already = vec![vec![p(0)], vec![p(1), p(2)], vec![p(1), p(3)]];
assert!(
symmetry_via_simplification_solve(4, &already).is_none(),
"symmetry already present on the raw formula ⟹ nothing unlocked"
);
let conflict = vec![vec![p(0)], vec![p(1)], vec![n(0), n(1)]];
let u = symmetry_via_simplification_solve(2, &conflict).expect("BCP reaches a conflict");
assert_eq!(u.via, Route::SymmetrySimplify);
assert!(matches!(u.answer, Answer::Unsat), "x0 ∧ x1 ∧ ¬(x0∧x1) is UNSAT");
}
#[test]
fn symmetric_binary_inference_learns_implication_orbits() {
let p = |v| Lit::new(v, true);
let n = |v| Lit::new(v, false);
let chain = vec![
vec![n(0), p(3)], vec![n(1), p(3)], vec![n(2), p(3)], vec![n(3), p(4)], ];
let s = symmetric_binary_inference_solve(5, &chain)
.expect("a derived implication orbit is learned");
assert_eq!(s.via, Route::SymmetricBinary);
match &s.answer {
Answer::Sat(m) => assert!(
chain.iter().all(|c| c.iter().any(|l| m[l.var() as usize] == l.is_positive())),
"the strengthened formula yields a valid model"
),
Answer::Unsat => panic!("the chain is SAT"),
}
let brute = (0u64..32).any(|x| {
let a: Vec<bool> = (0..5).map(|i| (x >> i) & 1 == 1).collect();
chain.iter().all(|c| c.iter().any(|l| a[l.var() as usize] == l.is_positive()))
});
assert_eq!(matches!(s.answer, Answer::Sat(_)), brute, "binary-inference verdict matches brute force");
let direct = vec![vec![n(0), p(2)], vec![n(1), p(2)]]; assert!(
symmetric_binary_inference_solve(3, &direct).is_none(),
"no new implication to learn ⟹ declines"
);
}
#[test]
fn symmetric_component_decomposition_solves_copies_once() {
let p = |v| Lit::new(v, true);
let n = |v| Lit::new(v, false);
let sat = vec![vec![p(0), p(1)], vec![p(2), p(3)]];
let s = symmetric_component_solve(4, &sat).expect("two symmetric components decompose");
assert_eq!(s.via, Route::SymmetricComponent);
match &s.answer {
Answer::Sat(m) => assert!(
sat.iter().all(|c| c.iter().any(|l| m[l.var() as usize] == l.is_positive())),
"the assembled model is valid"
),
Answer::Unsat => panic!("two copies of (x∨y) is SAT"),
}
let unsat = vec![
vec![p(0)], vec![p(1)], vec![n(0), n(1)],
vec![p(2)], vec![p(3)], vec![n(2), n(3)],
];
let u = symmetric_component_solve(4, &unsat).expect("two symmetric components decompose");
assert_eq!(u.via, Route::SymmetricComponent);
assert!(matches!(u.answer, Answer::Unsat), "an UNSAT component makes F UNSAT");
for cl in [&sat, &unsat] {
let brute = (0u64..16).any(|x| {
let a: Vec<bool> = (0..4).map(|i| (x >> i) & 1 == 1).collect();
cl.iter().all(|c| c.iter().any(|l| a[l.var() as usize] == l.is_positive()))
});
let got = symmetric_component_solve(4, cl).expect("decomposition fires");
assert_eq!(
matches!(got.answer, Answer::Sat(_)),
brute,
"component-decomposition verdict matches brute force"
);
}
let (clique, _) = crate::families::clique_coloring(3, 3);
assert!(
symmetric_component_solve(clique.num_vars, &clique.clauses).is_none(),
"a single component is not decomposable"
);
}
#[test]
fn plain_component_decomposition_solves_asymmetric_independent_parts() {
let p = |v| Lit::new(v, true);
let n = |v| Lit::new(v, false);
let sat = vec![vec![p(0), p(1)], vec![p(2), p(3)], vec![n(2), n(3)]];
assert!(symmetric_component_solve(4, &sat).is_none(), "asymmetric components: the symmetric route declines");
let s = solve_by_components(4, &sat);
assert_eq!(s.via, Route::Component);
match &s.answer {
Answer::Sat(m) => assert!(
sat.iter().all(|c| c.iter().any(|l| m[l.var() as usize] == l.is_positive())),
"the assembled model satisfies every clause"
),
Answer::Unsat => panic!("both components are satisfiable, so F is SAT"),
}
let unsat = vec![vec![p(0), p(1)], vec![p(2)], vec![n(2)]];
let u = solve_by_components(3, &unsat);
assert_eq!(u.via, Route::Component);
assert!(matches!(u.answer, Answer::Unsat), "an UNSAT component makes F UNSAT");
let single = vec![vec![p(0), p(1)], vec![n(0), p(1)]];
assert_ne!(solve_by_components(2, &single).via, Route::Component, "one component is not decomposable");
for (nv, cl) in [(4usize, &sat), (3, &unsat)] {
let brute = (0u64..(1 << nv)).any(|x| {
let a: Vec<bool> = (0..nv).map(|i| (x >> i) & 1 == 1).collect();
cl.iter().all(|c| c.iter().any(|l| a[l.var() as usize] == l.is_positive()))
});
assert_eq!(matches!(solve_by_components(nv, cl).answer, Answer::Sat(_)), brute, "matches brute force");
}
}
#[test]
fn symmetry_propagation_breaks_during_search_and_is_correct() {
let (sat, _) = crate::families::clique_coloring(3, 3);
let s = symmetry_propagate_solve(sat.num_vars, &sat.clauses)
.expect("a phase-free variable symmetry drives the propagator");
assert_eq!(s.via, Route::SymmetryPropagate);
match &s.answer {
Answer::Sat(m) => assert!(
sat.clauses.iter().all(|c| c.iter().any(|l| m[l.var() as usize] == l.is_positive())),
"the propagator returns a valid model"
),
Answer::Unsat => panic!("clique_coloring(3,3) is SAT"),
}
let (unsat, _) = crate::families::clique_coloring(4, 3);
let u = symmetry_propagate_solve(unsat.num_vars, &unsat.clauses).expect("variable symmetry");
assert_eq!(u.via, Route::SymmetryPropagate);
assert!(matches!(u.answer, Answer::Unsat), "clique_coloring(4,3) is UNSAT");
for (cnf, _) in [crate::families::clique_coloring(3, 3), crate::families::clique_coloring(4, 3)] {
let nv = cnf.num_vars;
let brute = (0u64..(1u64 << nv)).any(|x| {
let a: Vec<bool> = (0..nv).map(|i| (x >> i) & 1 == 1).collect();
cnf.clauses.iter().all(|c| c.iter().any(|l| a[l.var() as usize] == l.is_positive()))
});
let got = symmetry_propagate_solve(nv, &cnf.clauses).expect("propagator fires");
assert_eq!(
matches!(got.answer, Answer::Sat(_)),
brute,
"symmetry-propagation verdict matches brute force (nv={nv})"
);
}
}
#[test]
fn orbit_weight_quotient_collapses_a_full_symmetric_instance() {
let p = |v| Lit::new(v, true);
let at_least_2 = vec![vec![p(0), p(1)], vec![p(0), p(2)], vec![p(1), p(2)]];
let s = orbit_weight_quotient_solve(3, &at_least_2)
.expect("a full symmetric group collapses to weight classes");
assert_eq!(s.via, Route::OrbitWeightQuotient);
match &s.answer {
Answer::Sat(m) => {
assert!(at_least_2.iter().all(|c| c.iter().any(|l| m[l.var() as usize] == l.is_positive())));
assert!(m.iter().filter(|&&b| b).count() >= 2, "the witness has weight ≥ 2");
}
Answer::Unsat => panic!("at-least-2 of 3 is SAT"),
}
let subsets3 = [[0u32, 1, 2], [0, 1, 3], [0, 2, 3], [1, 2, 3]];
let pairs = [[0u32, 1], [0, 2], [0, 3], [1, 2], [1, 3], [2, 3]];
let mut card: Vec<Vec<Lit>> = Vec::new();
for sub in subsets3 {
card.push(sub.iter().map(|&v| Lit::new(v, true)).collect()); }
for pr in pairs {
card.push(pr.iter().map(|&v| Lit::new(v, false)).collect()); }
let u = orbit_weight_quotient_solve(4, &card).expect("S₄ is the full symmetric group on the orbit");
assert_eq!(u.via, Route::OrbitWeightQuotient);
assert!(matches!(u.answer, Answer::Unsat), "≥3 and ≤1 true is unsatisfiable");
for (nv, cl) in [(3usize, &at_least_2), (4, &card)] {
let brute = (0u64..(1u64 << nv)).any(|x| {
let a: Vec<bool> = (0..nv).map(|i| (x >> i) & 1 == 1).collect();
cl.iter().all(|c| c.iter().any(|l| a[l.var() as usize] == l.is_positive()))
});
let got = orbit_weight_quotient_solve(nv, cl).expect("quotient fires");
assert_eq!(
matches!(got.answer, Answer::Sat(_)),
brute,
"orbit-weight-quotient verdict matches brute force (nv={nv})"
);
}
let (clique, _) = crate::families::clique_coloring(3, 3);
assert!(
orbit_weight_quotient_solve(clique.num_vars, &clique.clauses).is_none(),
"a product symmetry that is not the full symmetric group is not a weight quotient"
);
}
#[test]
fn symmetric_probe_infers_a_whole_orbit_from_one_failed_literal() {
let y = |b| Lit::new(3, b);
let nx = |v| Lit::new(v, false);
let base: Vec<Vec<Lit>> =
(0u32..3).flat_map(|v| [vec![nx(v), y(true)], vec![nx(v), y(false)]]).collect();
let s = symmetric_probe_solve(4, &base).expect("a symmetric failed literal engages the probe");
assert_eq!(s.via, Route::SymmetricProbe);
match &s.answer {
Answer::Sat(m) => {
assert!(base.iter().all(|c| c.iter().any(|l| m[l.var() as usize] == l.is_positive())));
assert!(!m[0] && !m[1] && !m[2], "the whole orbit was inferred false from one probe");
}
Answer::Unsat => panic!("the base instance is SAT"),
}
let mut unsat = base.clone();
unsat.push(vec![Lit::new(0, true), Lit::new(1, true), Lit::new(2, true)]);
let u = symmetric_probe_solve(4, &unsat).expect("the probe engages");
assert_eq!(u.via, Route::SymmetricProbe);
assert!(matches!(u.answer, Answer::Unsat), "forcing the orbit false refutes the cardinality clause");
for cl in [&base, &unsat] {
let brute = (0u64..16).any(|x| {
let a: Vec<bool> = (0..4).map(|i| (x >> i) & 1 == 1).collect();
cl.iter().all(|c| c.iter().any(|l| a[l.var() as usize] == l.is_positive()))
});
let got = symmetric_probe_solve(4, cl).expect("probe fires");
assert_eq!(
matches!(got.answer, Answer::Sat(_)),
brute,
"symmetric-probe verdict matches brute force"
);
}
}
#[test]
fn local_symmetry_solve_exploits_branch_symmetry_and_is_correct() {
let f = vec![
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)], ];
let brute = (0u64..8).any(|x| {
let a: Vec<bool> = (0..3).map(|i| (x >> i) & 1 == 1).collect();
f.iter().all(|c| c.iter().any(|l| a[l.var() as usize] == l.is_positive()))
});
let solved = local_symmetry_solve(3, &f).expect("a branch reveals local symmetry");
assert_eq!(solved.via, Route::LocalSymmetry);
assert_eq!(matches!(solved.answer, Answer::Sat(_)), brute, "local-symmetry verdict matches brute force");
if let Answer::Sat(m) = &solved.answer {
assert!(
f.iter().all(|c| c.iter().any(|l| m[l.var() as usize] == l.is_positive())),
"the model from a local-symmetry branch satisfies F"
);
}
}
#[test]
fn symmetry_breaking_scales_to_a_large_group_via_partial_breaking() {
let (cnf, _) = crate::families::clique_coloring(6, 6);
let s = symmetry_break_solve(cnf.num_vars, &cnf.clauses)
.expect("a large phase-free symmetry group still drives partial breaking");
assert_eq!(s.via, Route::SymmetryBreak);
match s.answer {
Answer::Sat(m) => assert!(
cnf.clauses.iter().all(|c| c.iter().any(|l| m[l.var() as usize] == l.is_positive())),
"partial breaking returns a valid model"
),
Answer::Unsat => panic!("clique_coloring(6,6) is SAT"),
}
}
#[test]
fn the_composite_lift_verdict_matches_the_supplied_equations() {
use crate::modm::{solve as modm_solve, ModmOutcome};
for (eqs, cnf, want) in [
crate::families::mod_p_tseitin_expander(6, 6, 7),
crate::families::mod_p_consistent_onehot(6, 6, 7),
] {
let solved = solve_structured(cnf.num_vars, &cnf.clauses);
assert_eq!(solved.via, Route::ModM, "a composite instance must take the ℤ/m route");
let num_gf_vars = cnf.num_vars / 6; let supplied_unsat = matches!(modm_solve(&eqs, num_gf_vars, 6), Some(ModmOutcome::Unsat { .. }));
assert_eq!(
matches!(solved.answer, Answer::Unsat),
supplied_unsat,
"the lifted-CNF verdict must match modm::solve on the supplied equations"
);
assert_eq!(
matches!(solved.answer, Answer::Unsat),
matches!(want, crate::families::ExpectedVerdict::Unsat),
"and the family's declared expectation"
);
}
}
#[test]
fn mine_clauses_derives_an_implied_unit_via_probing() {
let clauses = vec![vec![Lit::new(0, true)], vec![Lit::new(0, false), Lit::new(1, true)]];
let mined = mine_clauses(2, &clauses);
assert!(
mined.iter().any(|c| c.len() == 1 && c[0].var() == 1 && c[0].is_positive()),
"expected mined implied unit b; got {mined:?}"
);
}
#[test]
fn every_mined_clause_is_implied() {
let clauses = vec![
xor_gadget(&[0, 1, 2], false),
vec![vec![Lit::new(0, true)]],
vec![vec![Lit::new(1, true)]],
]
.concat();
let n = 3;
let mined = mine_clauses(n, &clauses);
assert!(!mined.is_empty(), "this instance has implied structure to mine");
for mask in 0u32..(1 << n) {
let asg: Vec<bool> = (0..n).map(|v| (mask >> v) & 1 == 1).collect();
let is_model = clauses.iter().all(|c| c.iter().any(|l| asg[l.var() as usize] == l.is_positive()));
if is_model {
for mc in &mined {
assert!(
mc.iter().any(|l| asg[l.var() as usize] == l.is_positive()),
"mined clause {mc:?} is not implied (fails model {asg:?})"
);
}
}
}
}
#[test]
fn exact_cover_lift_crushes_modular_counting_and_the_chessboard() {
for n in [7usize, 9, 11] {
let (cnf, _) = crate::families::mod_counting(n, 2);
let s = solve_structured(cnf.num_vars, &cnf.clauses);
assert!(matches!(s.answer, Answer::Unsat), "Count_2({n}) is UNSAT");
assert_eq!(s.via, Route::ExactCover, "Count_2({n}): the exact-cover lift fires");
assert_eq!(s.conflicts, 0, "Count_2({n}): zero search");
}
for (n, q) in [(7usize, 3usize), (8, 3), (6, 5), (7, 5)] {
let (cnf, _) = crate::families::mod_counting(n, q);
let s = solve_structured(cnf.num_vars, &cnf.clauses);
assert!(matches!(s.answer, Answer::Unsat), "Count_{q}({n}) is UNSAT");
assert_eq!(s.via, Route::ExactCover, "Count_{q}({n}): the exact-cover lift fires");
}
let (cb, _) = crate::families::mutilated_chessboard(4);
let s = solve_structured(cb.num_vars, &cb.clauses);
assert!(matches!(s.answer, Answer::Unsat), "chessboard(4) is UNSAT");
assert_eq!(s.conflicts, 0, "chessboard(4): a specialist decides — zero search");
assert_ne!(s.via, Route::Cdcl, "chessboard(4): never the fallback");
let (sat6, _) = crate::families::mod_counting(6, 3);
let s = solve_structured(sat6.num_vars, &sat6.clauses);
match s.answer {
Answer::Sat(model) => {
assert!(
sat6.clauses.iter().all(|c| c.iter().any(|l| model[l.var() as usize] == l.is_positive())),
"Count_3(6): the SAT model re-checks"
);
}
Answer::Unsat => panic!("Count_3(6) is satisfiable — the lift must decline"),
}
}
#[test]
#[ignore = "scale measurement — symmetry-arsenal wall time on Ramsey; run explicitly"]
fn ramsey_symmetric_attack_is_measured() {
for (s, t, n) in [(3usize, 3usize, 6usize), (3, 4, 9)] {
let (cnf, _) = crate::families::ramsey(s, t, n);
let t0 = std::time::Instant::now();
let fast = solve_structured(cnf.num_vars, &cnf.clauses);
let fast_ms = t0.elapsed().as_millis();
assert!(matches!(fast.answer, Answer::Unsat), "ramsey({s},{t};{n}) is UNSAT");
let t1 = std::time::Instant::now();
let full = solve_comprehensive(cnf.num_vars, &cnf.clauses);
let full_ms = t1.elapsed().as_millis();
assert!(matches!(full.answer, Answer::Unsat), "ramsey({s},{t};{n}) is UNSAT (arsenal)");
eprintln!(
"RAMSEY | ({s},{t};{n}) [{} vars]: fast={:?} {}ms {} conflicts | arsenal={:?} {}ms {} conflicts",
cnf.num_vars, fast.via, fast_ms, fast.conflicts, full.via, full_ms, full.conflicts
);
}
}
}