Struct Cover 

pub struct Cover {
    pub n: usize,
    pub blockers: Vec<Subcube>,
}

A cover of the hypercube by clause-blockers — the geometric form of a CNF. UNSAT ⟺ the blockers leave no corner uncovered.

Fields

n: usize

blockers: Vec<Subcube>

Implementations

impl Cover

pub fn of_cnf(cnf: &DimacsCnf) -> Cover

The blocker cover of a CNF: one subcube per clause.

pub fn vertex_energy(&self, corner: Corner) -> usize

The energy of a corner: how many blockers cover it (Pnp.lean’s vertexEnergy). Energy zero ⟺ the corner is a satisfying assignment.

pub fn blocks(&self, corner: Corner) -> bool

Is corner forbidden by some clause? (Does it falsify the formula?)

pub fn is_tight(&self, corner: Corner) -> bool

Pnp.lean’s vertex energy classes. Tight: covered by exactly one blocker — that blocker is essential there, deleting it exposes the corner. Redundant: two or more cover it, robust to dropping one. (Uncovered, energy 0, is a model — escaping_corner.)

pub fn is_redundant(&self, corner: Corner) -> bool

Pnp.lean’s VertexOverlappedBy: two or more blockers cover this corner.

pub fn essential_blockers(&self) -> Vec<usize>

The essential blockers — the irreducible core of the cover. A blocker is essential when it privately covers some corner (a tight vertex no other blocker reaches); deleting it would break totality. The essential set is the geometric analog of a minimal resolution refutation: the rules you cannot drop. (Enumerates footprints — for small covers.)

pub fn escaping_corner(&self) -> Option<Corner>

The first corner no blocker reaches — a satisfying assignment of energy zero — or None when the cover is total. None ⟺ the formula is UNSAT. Brute over all 2ⁿ corners.

pub fn is_total(&self) -> bool

UNSAT ⟺ the blockers cover every corner of the hypercube (Pnp.lean’s HasNoHole).

pub fn solution_count(&self) -> u64

The number of satisfying assignments — uncovered corners of energy zero (solutionCount).

pub fn has_no_hole(&self) -> bool

Pnp.lean’s HasNoHole (refutation side): the cover is total — no corner escapes.

pub fn relaxation_feasible_at_center(&self) -> bool

The ½ key — is the LP relaxation feasible at the symmetric center? The all-½ point satisfies a clause’s relaxation (Σ lits ≥ 1) iff the clause has width ≥ 2 (each literal contributes ½). When every blocker has width ≥ 2, the center ½ⁿ is a feasible fractional point — so the cover can be integer-UNSAT while its LP relaxation is satisfiable. That integrality gap, sitting exactly at the symmetry-fixed center, is what resolution (which lives at the corners) cannot see and what the counting/cutting-planes shadows close.

pub fn counting_refutation(&self) -> Option<CountingCert>

Generalized counting crush: derive the O(1) Hall certificate (items > slots) from any matching-shaped cover — pigeonhole, clique-coloring, anything that symmetry-breaks to the same two rule-types — by recovering the bipartite structure. The pigeonhole crush, no longer hard-coded to pigeonhole.

pub fn hall_refutation(&self) -> Option<HallWitness>

The full Hall refutation — the matching invariant in its complete (subset) form. Catches a bipartite cover whose totals balance but where some subset of items competes for too few slots, returning the violating subset. Strictly stronger than counting_refutation.

pub fn has_unique_hole(&self) -> bool

Pnp.lean’s HasUniqueHole: exactly one corner is uncovered (search-critical SAT).

pub fn has_at_least_holes(&self, k: u64) -> bool

Pnp.lean’s HasAtLeastHoles k: at least k corners remain uncovered (search-easy SAT).

pub fn separated_by(&self, cut: u64) -> bool

Pnp.lean’s BlockerFamily.SeparatedBy: no blocker crosses the coordinate cut cut — each blocker’s support lies entirely inside it or entirely outside. The hypercube version of a decomposition separator.

pub fn variable_interaction(&self, i: usize, j: usize) -> bool

Pnp.lean’s BlockerFamily.VariableInteraction: some blocker mentions both i and j — the primal-graph edge of the cover.

pub fn to_expr(&self) -> Option<ProofExpr>

Recover the CNF this cover is the geometry of, as a ProofExpr over atoms x{var} — the door back into the certified prover. None when a blocker is the empty clause (an immediate contradiction with no propositional form) or the cover has no blockers.

pub fn prove_total_certified(&self) -> UnsatOutcome

Decide cover-totality through the certified prover, not brute force: route the cover’s CNF into crate::sat::prove_unsat, which returns a RUP/PR-checked Refuted when the cover is total (fail-closed — never a false Refuted) or a witnessing model when a corner escapes. This is what makes the geometry provable: pigeonhole covers certify via the counting shadow in polynomial time, where resolution would blow up.

pub fn neighbors(&self, i: usize) -> Vec<(usize, usize, Subcube)>

Reference one rule, get the rules it nets us. All blockers that resolve with blocker i, each paired with its pivot and the resolvent it produces — the neighbors of rule i in the resolution graph, and the new rules they beget.

pub fn clauses(&self) -> Vec<Vec<Lit>>

Recover the clauses this cover is the geometry of, as packed Lits — the door into the automorphism detector and the certified prover’s Lit-level core.

pub fn blocker_orbits(&self, generators: &[CubeSym]) -> Option<Vec<Vec<usize>>>

Symmetry-break the rules, not the corners. Partition the blocker indices into orbits under the automorphism group generated by generators. Each generator must map the blocker set into itself (it is verified by the image landing back among the blockers); if one ever maps a blocker off the set it is not a rule-automorphism and we return None, fail-closed.

This is the cheap, powerful move the corner-orbit walk is not: there are only polynomially many blockers (one per clause), so quotienting the rule set costs O(generators · blockers · n) — no 2ⁿ anywhere. The number of orbits is the count of essentially distinct rules: a complexity signature of the family computed without ever touching the exponential cube. (Assumes distinct blockers, as ordinary CNF families have.)

pub fn discovered_rule_symmetry(&self) -> RuleSymmetry

Discover this cover’s own symmetries and read off its rule-orbit signature — the fully self-driving complexity classifier. The detector (crate::symmetry_detect::find_generators) returns a generating set of automorphisms as Perms, and we quotient the rules by them with clause_orbits (clause-level, so it scales past the geometric cube’s 63-variable ceiling). A maximally symmetric family (pigeonhole) collapses to a handful of orbits at every scale; a random instance, with a trivial automorphism group, collapses to nothing — every rule its own.

impl Cover

pub fn auto_certify(&self) -> CoverVerdict

Auto-cut and crush. Try each certified cut in turn — the counting hyperplane (Hall), the affine GF(2) cut (Gaussian), the cardinality cutting plane (Farkas) — and fall back to the general certified prover if no structured cut fits. One call, every family: it reports which hyperplane family closed the cover, or that a corner escapes. This is the whole campaign behind a single door — and it is exactly sat::prove_unsat’s cascade, surfaced with the cut it used.

Trait Implementations

impl Clone for Cover

fn clone(&self) -> Cover

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for Cover

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.