Function optimize_modulo_symmetry 

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

Weighted minimization, symmetry-reduced. Minimise Σ weights[i]·x_i over the models of clauses, exploiting optimization_symmetry_generators: break the objective-preserving symmetry, then search the reduced model space. SOUND — the optimum is identical to the unbroken problem (an optimal orbit’s lex-leader survives the break and has the same objective) and the witness is a genuine model of the original F. None iff F is unsatisfiable. The symmetry-aware optimizer (a new problem class beyond the decision/counting/equivalence faces).