pub fn min_resolution_width(cover: &Cover) -> Option<usize>Expand description
The minimum width of a resolution refutation of an UNSAT cover — the size of the widest clause
any width-bounded refutation must carry, the classic resolution complexity measure (Ben-Sasson–
Wigderson). A subcube is a clause (Subcube::clause_literals) and Subcube::resolve is the
geometry of the resolution step; the empty subcube (care = 0, the whole cube blocked) is the
derived contradiction. For width budget w we seed with the input blockers of support ≤ w and
saturate under width-≤ w resolution; the least w that derives the empty subcube is the width.
None only if the cover is satisfiable (no refutation at any width); every UNSAT cover succeeds by
w = n since full-width resolution is complete. (For small covers — it enumerates resolvents.)