pub fn build_ns_certificate(
num_vars: usize,
clauses: &[Vec<Lit>],
) -> Result<NsCertificate, Vec<bool>>Expand description
The uniform Nullstellensatz completeness construction. For any CNF over num_vars ≤ 20 variables,
return either a constructive NsCertificate proving UNSAT, or a satisfying assignment proving SAT — a
total, certifying decision. The construction is the partition of unity Σ_a δ_a = 1: every corner a
is charged to one clause it falsifies (a corner that falsifies none is a model — SAT), and the
coefficient of clause C is g_C = Σ_{a charged to C} δ_a. Then Σ_C p_C · g_C = Σ_a p_{sel(a)} · δ_a = Σ_a δ_a = 1, because p_{sel(a)}(a) = 1 collapses p·δ_a to δ_a on the cube (multilinear
representations are unique). Because this succeeds identically at every n, it does not merely measure
but proves that every unsatisfiable formula has a degree-≤ n GF(2) Nullstellensatz refutation — no
minimal-UNSAT family is structureless, at any n. This is the census’s max_ns_degree = n ceiling as a
construction, settling n = 5, 6, … where the orbit census is infeasible.