pub fn sel_refute(num_vars: usize, clauses: &[Vec<Lit>]) -> SelOutcomeExpand description
Refute clauses with Symmetric Explanation Learning, or report SAT / Unknown. The conflict
budget per round and the round cap bound the work; symmetric amplification is what makes the
total conflict count collapse on symmetry-rich instances.