Module polycalc 

Polynomial Calculus / Nullstellensatz over GF(2) — the algebraic proof system that subsumes the linear cuts (parity is its degree-1 fragment) and, at higher degree, refutes strictly more.

A CNF is unsatisfiable iff the constant polynomial 1 lies in the ideal generated by the clause polynomials over the multilinear GF(2) ring (where x² = x, so every monomial is squarefree). At a fixed degree d this is a finite linear-algebra question — is 1 in the GF(2)-span of { m · p_C : clause C, monomial m, deg(m·p_C) ≤ d }? — answered by Gaussian elimination. So degree-d Nullstellensatz is polynomial, and the degree is the power dial: d = 1 recovers parity, larger d reaches counting-style and beyond. The genuinely hard residue (random) needs degree Θ(n), which is exactly why it stays hard — there is no low-degree algebraic certificate, just as there is no small symmetry quotient. The two are the same wall seen from two sides.

Symmetry meets this engine at the monomial basis: an automorphism of the formula permutes monomials, so the Nullstellensatz system has the family’s symmetry and its solution can be sought on the orbit quotient of the basis — the algebraic form of “decide on the quotient.”

Structs

NsCertificate

A constructive Nullstellensatz certificate over the multilinear GF(2) ring: one coefficient polynomial g_C per input clause such that Σ_C p_C · g_C = 1, where p_C = clause_polynomial(C) is the clause’s false-indicator. The identity is a re-checkable proof of UNSAT — evaluate it at any assignment a: the right side is 1, so some p_C(a) = 1, i.e. every assignment falsifies some clause. Where nullstellensatz_refutes only decides whether such a certificate exists, this one carries the witness.

Functions

build_ns_certificate

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.

check_ns_lower_bound

Re-check a ns_lower_bound_witness certificate (zero trust in the producer): the functional L (given as the monomials on which it is 1) must satisfy L(1) = 1 and L(m · p_C) = 0 for every degree-≤ d generator. true ⟹ F genuinely has no degree-d GF(2) Nullstellensatz refutation.

check_ns_lower_bound_polys

Re-check a ns_lower_bound_witness_polys certificate (zero trust in the producer): L(1) = 1 and L(m·g) = 0 for every admitted generator of the system. true ⟹ the generator system genuinely has no degree-d GF(2) Nullstellensatz refutation. Degree-bounded enumeration — num_vars ≤ 63.

clause_polynomial

The clause polynomial: 1 exactly on the clause’s falsifying assignment. The false-indicator of a positive literal x is 1 + x ({∅, {x}}), of a negative literal ¬x is x ({{x}}); the clause polynomial is their product. Degree = clause width.

exactly_one_linear_generators

The linear encoding of exactly-one constraints: for each group G the degree-1 generator 1 + Σ_{v∈G} x_v (the GF(2) form of Σ x = 1) plus the pairwise products x_u·x_v over each group, deduplicated. This is the encoding under which the modular-counting and pigeonhole degree lower bounds are stated in the literature — the wide at-least-one clause is recovered from it modulo the pairs (the interreduction test pins the identity, and the clause→linear direction is degree-preserving, so bounds against this encoding are the stronger statements). The linear generators come first (one per group, in group order), then the pairs.

monomial_orbits

Symmetry-break Polynomial Calculus at the basis. Partition the degree-≤degree monomials into orbits under the formula’s automorphisms. The orbit count is the width of the symmetry-reduced Nullstellensatz system — a symmetric certificate is constant on each orbit, so the Gaussian runs over the quotient instead of all C(n,d) monomials. The same collapse that made the field cuts O(1), inherited by the algebraic engine. (Bounded to num_vars ≤ 20.)

monomials_up_to_degree

All squarefree monomials of degree ≤ degree over num_vars ≤ 63 variables, ascending as u64s — enumerated directly (Gosper’s next-k-subset walk per degree class), never touching the 2ⁿ cube. This is the basis walk that lifts fixed-degree Nullstellensatz work past the clause engine’s 20-variable cap: the count is Σ_{k≤d} C(n,k) (nullstellensatz_basis_size), not 2ⁿ.

ns_lower_bound_witness

A re-checkable degree-d Nullstellensatz LOWER-bound certificate. Where nullstellensatz_refutes decides whether a degree-d refutation exists, this witnesses its NON-existence: a GF(2) linear functional L on the degree-≤ d monomials (a *degree-d pseudo-expectation) with L(1) = 1andL(m · p_C) = 0for every generator. Such anLexists iff1is **not** in theGF(2)-span of the generators, i.e. iff there is no degree-drefutation — soSome(L)certifies the lower boundNS-degree(F) > d, independently re-checkable by [check_ns_lower_bound] (no trust in the solver). The certificate is returned as the list of monomials on which Lis1. None means a degree-drefutation exists (no lower bound atd). Multi-word linear algebra, so the monomial basis is not size-capped — only num_vars ≤ 20` for the explicit basis enumeration.

ns_lower_bound_witness_on_basis

ns_lower_bound_witness restricted to a sub-basis of monomials: the functional L is sought only on monomials m with in_basis(m) (and L = 0 elsewhere), while the constraints ⟨L, m·p_C⟩ = 0 still range over all generators. Some(L) is a fully valid, check_ns_lower_bound-verifiable witness (the restriction only limits the search, not the check); None here means “no witness on this sub-basis” — which, unlike the full-basis version, does not imply a refutation exists. This exposes the structure of a lower bound: e.g. for pigeonhole, the partial-matching sub-basis already carries the certificate.

ns_lower_bound_witness_polys

ns_lower_bound_witness for an arbitrary polynomial generator system: a degree-d pseudo-expectation L with L(1) = 1 and L(m·g) = 0 for every admitted generator, returned as the monomials where L = 1. Some(L) certifies NS-degree > d for the system (re-checkable by check_ns_lower_bound_polys, zero trust in the solver); None means a degree-d refutation exists. Degree-bounded enumeration — num_vars ≤ 63.

ns_lower_bound_witness_polys_on_basis

ns_lower_bound_witness_polys restricted to a sub-basis: the functional L is sought only on monomials passing in_basis (L = 0 elsewhere), while the constraints ⟨L, m·g⟩ = 0 still range over all admitted generators — so any Some is a fully valid, check_ns_lower_bound_polys-verifiable witness, and None means only “no witness on this sub-basis”. The structure probe: which candidate supports carry a family’s lower bound (for pigeonhole this is how the hole-injective support was found and the classical partial-matching support was ruled out over GF(2)). Degree-bounded enumeration — num_vars ≤ 63.

ns_refutes_polys

Does a degree-d Nullstellensatz refutation exist over GF(2) for an arbitrary polynomial generator system — is 1 in the GF(2)-span of { m·g : deg(m·g) ≤ d }? The clause engine’s question asked of any generators, not just clause polynomials: the substrate for the linear encoding (exactly_one_linear_generators) and the symmetric-family machinery. The multiplier rule is exact — a product is admitted by its degree after multilinear collapse. (For clause polynomials this span equals the clause engine’s: a multiplier overlapping a positive literal kills the product, one overlapping a negative literal absorbs into a smaller multiplier — pinned by the differential test.) Degree-bounded enumeration, so it scales to num_vars ≤ 63.

nullstellensatz_basis_size

The width of the degree-d Nullstellensatz system over n variables: the count of multilinear monomials of degree ≤ d, Σ_{k≤d} C(n,k). At d = n this is exactly 2ⁿ — so the degree-n certificate that build_ns_certificate always produces (completeness: no unsatisfiable formula over n variables is “structureless”) lives in an exponentially large space. The certificate’s existence is an information-theoretic fact about the finite cube; it is not an efficient algorithm, and it says nothing about P vs NP — which is a statement about the asymptotic growth of a family of instances, not any fixed finite n (a fixed finite problem is decidable by table lookup, vacuously).

nullstellensatz_refutes

Does a degree-d Nullstellensatz refutation exist over GF(2)? Sound: such a certificate exists only when the formula is unsatisfiable. Complete at d = num_vars (full degree decides any instance). Bounded to num_vars ≤ 20 (the explicit monomial basis).

nullstellensatz_refutes_symmetric

Symmetry-reduced Nullstellensatz — the algebraic refutation collapsed by the formula’s symmetry. Full degree-d NS asks whether 1 lies in the GF(2)-span of the generators m·p_C, a Gaussian over up to C(n,≤d) monomial columns. When the formula has a symmetry group G, summing each generator’s G-orbit gives an invariant generator, and every invariant polynomial is constant on the monomial orbits (monomial_orbits) — so the same span check runs over just #orbits columns and #generator-orbits rows. For a symmetric family that is the difference between 2^Θ(n) and O(1).

partition_of_unity

The partition of unity over the n-cube: Σ_{a ∈ {0,1}ⁿ} δ_a, the sum of every corner’s point-indicator. It is the constant 1 for all n — the identity the constructive Nullstellensatz certificate (build_ns_certificate) rests on. Computed here by direct summation (for finite checks); pou_as_product gives the closed form that proves it ∀n.

php_is_hole_injective

Is a PHP monomial hole-injective — no two of its edges share a hole? Standard PHP forbids two pigeons in one hole but allows a pigeon in several holes, so the at-most-one clauses force the GF(2) pseudo-expectation to vanish exactly on hole-collision monomials — i.e. its support lies in the hole-injective monomials (partial functions hole→pigeon). This is looser than a partial matching (which also forbids pigeon repeats) and is the correct GF(2) support.

php_is_partial_matching

Is a PHP monomial a partial matching — an injective partial pigeon→hole map? PHP’s variable x_{p,h} sits at index p·holes + h (crate::families::php), so a monomial (a set of variables) is a partial matching iff no two of its variables share a pigeon or a hole. This is the support of the Razborov degree lower bound’s pseudo-expectation.

poly_degree

The degree of a multilinear GF(2) polynomial: its largest monomial’s popcount (0 for the zero polynomial and for the constant 1).

polynomial_calculus_refutes

Does a degree-d Polynomial Calculus refutation exist over GF(2)? PC is the dynamic strengthening of Nullstellensatz: start from the clause polynomials and close under (i) GF(2) linear combination and (ii) multiplication by a single variable, keeping every derived polynomial multilinear of degree ≤ d; the system is refuted iff the constant 1 is derived. Because an intermediate linear combination can cancel high-degree terms before the next multiply, degree-d PC certifies a superset of what degree-d Nullstellensatz can (which must hit each axiom with a single monomial in one shot). Sound — 1 is derivable only from an unsatisfiable system — and PC ⊇ NS, so it never refutes fewer. Complete at d = num_vars. Bounded to num_vars ≤ 20.

pou_as_product

The closed form of the partition of unity: the product Π_{v<n} ((1+x_v) + x_v) of the per-coordinate atoms. By distributivity Σ_a Π_i f_{i,a_i} = Π_i (f_{i,0} + f_{i,1}), this equals partition_of_unity — a sum of 2ⁿ products rewritten as a product of n sums. Since every atom is 1 (pou_atom), the product is 1 for every n. This is the ratchet to n = ∞: not 2ⁿ terms checked one cube at a time, but n identical unit factors.

pou_atom

The atom of the partition-of-unity recurrence on variable v: (1 + x_v) + x_v, which reduces to the constant 1 in the multilinear GF(2) ring (x_v + x_v = 0). This single identity is the engine of the whole n = ∞ ratchet: it is independent of n, so a product of n copies of it is 1 at every scale.

symmetric_group_generators

The generators of the full symmetric group Sₙ on n variables: the adjacent transpositions (i, i+1). Sₙ is the symmetry of a fully-symmetric formula (every variable interchangeable), and under it the monomial basis collapses to one orbit per degree — the sharpest instance of monomial_orbits’ compression.

Type Aliases

Mono

A multilinear monomial: the bitmask of the variables it contains (x² = x ⟹ squarefree). The u64 mask carries up to 63 variables; the clause engine’s explicit cube enumeration stops at 20, the degree-bounded polynomial engine (monomials_up_to_degree) uses the full range.

Poly

A multilinear polynomial over GF(2): the set of monomials with coefficient 1 (XOR/symmetric- difference semantics).