Skip to main content

apply_renaming

Function apply_renaming 

Source
pub fn apply_renaming(clauses: &[Vec<Lit>], flips: &[bool]) -> Vec<Vec<Lit>>
Expand description

Apply a flip-renaming x_v → ¬x_v for every v with flips[v] — a phase-flip symmetry of the cube. It permutes models bijectively (negate the flipped coordinates), so it preserves satisfiability.