Skip to main content

clause_orbits

Function clause_orbits 

Source
pub fn clause_orbits(
    clauses: &[Vec<Lit>],
    generators: &[Perm],
) -> Vec<Vec<usize>>
Expand description

Symmetry-break the rules at the clause level — the lift-and-shift-left form that scales to any number of variables. Partition the clause indices (the blockers) into orbits under a generating set of automorphisms, applying each Perm to clause literals directly via the canonical clause_key. A blocker is a clause, so this is the same rule-quotient as Cover::blocker_orbits — but with no 2ⁿ corner geometry and no 63-variable ceiling, so it runs at scales where the cube is astronomically large. The orbit count is the number of essentially-distinct rules. (Generators that move a clause off the set are simply not followed — only genuine rule-automorphisms close orbits.)