Skip to main content

apply_perm_to_model

Function apply_perm_to_model 

Source
pub fn apply_perm_to_model(perm: &Perm, model: &[bool]) -> Vec<bool>
Expand description

Push a model through an automorphism: if σ preserves the clause set and m satisfies it, so does σ(m). Variable v’s value lands on σ(+v)’s variable, negated when σ(+v) is the negative literal — chosen so m ⊨ C ⟹ σ(m) ⊨ σ(C).