Skip to main content

minimal_cover_orbits

Function minimal_cover_orbits 

Source
pub fn minimal_cover_orbits(n: usize) -> Vec<Cover>
Expand description

Enumerate every minimal UNSAT cover of the n-cube, one canonical representative per Bₙ orbit. A minimal cover is a set of subcube blockers that covers every corner (UNSAT) and none of which is droppable (every blocker privately owns some corner) — i.e. a minimal unsatisfiable CNF (an MUS), the irreducible atom of the UNSAT universe. Branch on the lex-least uncovered corner: it lies in exactly 2ⁿ subcubes (one per support care ⊆ [n], with value = corner & care); recurse on each. Monotone pruning kills a branch the moment any chosen blocker becomes fully redundant (it can never recover a private corner once one is stolen). A leaf is total ∧ fully essential; leaves are folded to their canonical_cover key so each orbit is reported once. (Exhaustive; for small n.)