Function renaming_to_horn 

pub fn renaming_to_horn(
    num_vars: usize,
    clauses: &[Vec<Lit>],
) -> Option<Vec<bool>>

Recognize a new symmetry: renamable-Horn. Is there a flip-renaming under which every clause has at most one positive literal (Horn)? Horn-SAT is polynomial (unit propagation finds the least model), so a renamable-Horn formula is in a poly class our field cuts cannot see. Crucially, finding the renaming is itself a 2-SAT: a clause is Horn-after-flip iff no two of its literals are both positive, and “literal l is positive after flip” is the single f-literal (l.var, l.is_positive). Returns the flip-set, or None if no renaming makes it Horn.