Function search_cost_antipodal 

pub fn search_cost_antipodal(
    num_vars: usize,
    clauses: &[Vec<Lit>],
    budget: usize,
) -> SearchCost

Recursive antipodal symmetry breaking. Branch search that, at every node, re-detects whether the residual is antipodally symmetric (is_antipodally_symmetric); when it is, it fixes the pivot to false WLOG and prunes the true branch — soundly, since the residual’s models come in antipodal pairs. A disjoint union of self-complementary blocks keeps regaining the symmetry as each block’s first variable is fixed, so the break fires recursively, collapsing one factor of 2 per block.