Function distinct_cofactor_dag 

pub fn distinct_cofactor_dag(
    n: usize,
    clauses: &CanonClauses,
) -> Option<(usize, Vec<Node>)>

Build the memoized strict distinct-cofactor DAG over the fixed order 0..n. Identical cofactors at the same depth SHARE a node. Returns None iff the formula is satisfiable (some fully unfolded branch carries no ⊥). The node count is the number of distinct cofactors — the OBDD width — and is the honest exponential floor on the residue (no order keeps it small).