Function decide_laddered_sym 

pub fn decide_laddered_sym(
    num_vars: usize,
    clauses: &[Vec<Lit>],
    use_cut: bool,
) -> (bool, LadderStats)

Symmetry-break the search itself. The same branch-and-cut ladder, but it branches variables in index order and prunes a node whenever a root automorphism maps its decided prefix to a lexicographically smaller decided assignment — classic lex-leader symmetry breaking during search. Sound by construction: every orbit of assignments keeps exactly one lex-leader, and only strict non-leaders are pruned, so the verdict never changes; symmetric subtrees are simply skipped. The automorphisms are discovered once at the root.