pub fn level_widths(n: usize, root: &CanonClauses) -> Vec<usize>Expand description
The per-level widths of the strict decision DAG: w[i] = number of distinct residual clause-sets
reachable after branching on variables 0..i. The distinct-cofactor count is Σ w[i].