pub fn almost_symmetry_pairs(
num_vars: usize,
clauses: &[Vec<Lit>],
max_broken: usize,
) -> Vec<(usize, usize, Vec<Vec<Lit>>)>Expand description
The almost-symmetries (variable transpositions) of a CNF: pairs (a,b) whose swap preserves all but
at most max_broken clauses. Returns each pair with the broken images σ(B) = { swap(c) : swap(c) ∉ F } — the clauses that must hold for the swap to map a model to a model, i.e. the guard. An empty image
set is a true (syntactic) symmetry and is excluded.