Skip to main content

conditional_symmetry_generators

Function conditional_symmetry_generators 

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

Conditional (local) symmetry — the symmetry of the RESIDUAL formula after a partial assignment. A formula can be globally asymmetric yet its residual F|ρ symmetric: symmetries that emerge only down a branch, invisible to a global automorphism search. Returns the residual’s literal-symmetry generators (image-literal form). This is a different symmetry source — the basis for local symmetry breaking during search, where each decision can unlock fresh symmetry to exploit.