Function solve_certified 

pub fn solve_certified(
    num_vars: usize,
    clauses: &[Vec<Lit>],
) -> CertifiedOutcome

The unified certified solver — the apex of the campaign. Given ANY formula it (1) auto-discovers propagation-redundant clauses via SDCL (positive reduct + live symmetry), then (2) solves the augmented formula with the modernized CDCL core. On UNSAT it returns a single machine-checked refutation composed of every step; on SAT a model (valid for the original, since SDCL only adds satisfiability-preserving clauses). Symmetry breaking, SDCL, and CDCL, fused into one certified engine.