pub fn auto_advance(
num_vars: usize,
clauses: &[Vec<Lit>],
max_steps: usize,
) -> (AdvanceStatus, Vec<AdvanceStep>)Expand description
Auto-diagnose, auto-break, auto-advance — to the fixpoint. Repeatedly diagnose the instance and apply the most decisive lever it offers: a certified cut decides it outright; otherwise carve (unit / pure-literal / subsumption) and bounded variable elimination peel it down; the loop advances until a verdict drops out or no structural lever reduces it further — the structureless residue, where the only remaining move is to branch. The returned trace shows the structure draining away step by step.