Module res_width 

Certified resolution-width lower bounds — the third proof system of the separations atlas, with the same zero-trust certificate discipline as the Nullstellensatz dual witnesses.

Width-w resolution keeps every clause in the derivation to ≤ w literals; Ben-Sasson–Wigderson made width the master resolution complexity measure (short proofs imply narrow proofs). At a fixed budget w the derivable set is a finite least fixpoint: saturate pairwise resolution, keeping resolvents of width ≤ w. That fixpoint is the lower-bound certificate: a clause set S that (i) contains the admissible inputs, (ii) is closed under width-≤ w resolution, and (iii) lacks the empty clause proves — by induction over any purported derivation — that no width-w resolution refutation exists. The certificate is re-checked by check_res_width_lower_bound with zero trust in the producer, mirroring polycalc::check_ns_lower_bound.

Two width conventions live in the literature, and they genuinely differ on wide-axiom families like pigeonhole (pigeon clauses have width m−1): WidthConvention::Strict counts axioms against the budget (the census’s hypercube::min_resolution_width convention); WidthConvention::WideAxioms admits every axiom and bounds only derived clauses — the convention under which PHP’s width question is non-trivial. Tautologies are dropped throughout: a resolvent with a second clashing variable is tautological (mirrored from Subcube::resolve, which requires a single clean pivot), and tautological axioms only ever produce subsumed or tautological resolvents.

Enums

WidthConvention

Which clauses the width budget w applies to.

Functions

check_res_width_lower_bound

Re-check a resolution-width lower-bound certificate (zero trust in the producer). closed certifies “no width-w resolution refutation of clauses under convention” iff: (i) it contains every admissible axiom, (ii) it is tautology-free, (iii) it is closed under width-≤ w resolution, and (iv) it lacks the empty clause. Soundness is an induction over any purported width-w derivation: its every clause lies in closed, and ⊥ ∉ closed. A padded (superset) certificate still certifies — extra clauses only weaken the producer, never the bound.

mask_clause

The bitmask form of a clause (duplicates collapse; ≤ 63 variables).

mask_width

The width of a mask clause — its literal count.

min_res_width_clauses

The minimum resolution-refutation width under a convention: the least w whose closure derives the empty clause. None iff the formula is satisfiable (resolution is complete at w = num_vars).

resolution_width_closure

The width-w resolution closure — the least fixpoint of pairwise resolution over the admissible axioms, keeping every resolvent of width ≤ w. This set contains every clause any width-w resolution derivation (under the convention) can produce, so it decides width-w refutability ((0,0) present ⟺ refutable) and, when the empty clause is absent, the set itself is the re-checkable lower-bound certificate (check_res_width_lower_bound).

resolve_masks

Resolve two mask clauses on their single clashing variable. Some(resolvent) iff exactly one variable appears positively in one and negatively in the other (a second clash would make every resolvent a tautology — the same single-pivot rule as Subcube::resolve). The resolvent is automatically tautology-free.

width_refutes

Does a width-w resolution refutation exist under the convention? Decided by the closure.

Type Aliases

MaskClause

A clause as a signed bitmask pair (pos, neg) over ≤ 63 variables — pos the positive literals’ variable set, neg the negative ones’. The empty clause is (0, 0); a tautology has pos & neg ≠ 0. This is the Subcube blocker seen from the clause side (care = pos|neg, value = neg).