Skip to main content

affine_composite_shear_generators

Function affine_composite_shear_generators 

Source
pub fn affine_composite_shear_generators(
    num_vars: usize,
    clauses: &[Vec<Lit>],
    max_targets: usize,
) -> Vec<(Vec<u32>, u32)>
Expand description

A bounded-composite affine-symmetry finder — climbing the “single-transvection wall” instead of declaring it. affine_transvection_generators only sees depth-1 shears (a single x_i ↦ x_i ⊕ x_j), so it is blind to symmetries realized only as a product of transvections — the parity/linear shears are the canonical example (“add x_j to x_i and x_k” preserves ⊕ x = b because it adds x_j to the form twice = 0; neither half does). This extends the finder to shears of composite depth ≤ max_targets: for every source j and every target set S ⊆ vars∖{j} with 1 ≤ |S| ≤ max_targets, the commuting product “add x_j to each x_i ∈ S”. At max_targets = 1 it is the transvection finder; at max_targets = 2 it catches the parity shears I earlier called out of reach. Polynomial for fixed depth (O(n^{max_targets+1}·|clauses|)), sound (every returned generator is verified to permute the clause set), and still incomplete only at unbounded depth — but the depth is now a tunable window, and the composite depth a formula’s symmetries require is itself a complexity measure. Returns each generator as (S, j).