Research · Papers · The quadratic hull and its defects · ML-052
On the static quadratic hull as a general SAT preprocessor
If |F| < 2^(n-d), then I_≤d(R) = {0} and H_d(R) = F₂^n
Published 2026-08-29
For everyone
Plain summary
A static quadratic hull is a one-time filter that tests truth assignments against all degree-two polynomial equations satisfied by a target relation. ML-052 proves this filter cannot serve as a general preprocessor for Boolean satisfiability (SAT). For any clause with three or more literals, the single forbidden assignment leaves too few non-solutions to support any degree-two polynomial separator. As a result, the hull accepts the entire assignment space and eliminates nothing. Ordinary SAT solvers use unit propagation to force literals dynamically during search, extracting inferences that a static hull misses completely. The technique retains a narrow use as an encoding linter: on small, explicitly listed relations, it can extract valid quadratic invariants, flag coordinates that quadratic constraints cannot isolate, and verify whether auxiliary variables make an arithmetized representation exact. The underlying Reed–Muller minimum-distance bound is classical, and no novelty is claimed for the core algebraic argument.
Result
Let R ⊆ F_2^n be a relation of valid assignments with forbidden set F = F_2^n \ R. Let I_≤d(R) denote the space of polynomials in F_2[x_1, ..., x_n] of degree at most d that vanish on R, and let H_d(R) = {x ∈ F_2^n : p(x) = 0 for all p ∈ I_≤d(R)} be the degree-d hull.
If |F| < 2^(n-d), then I_≤d(R) = {0} and H_d(R) = F_2^n.
At d = 2, every k-literal clause with k ≥ 3 has |F| = 1 < 2^(n-2). The sole non-satisfying assignment cannot support a non-trivial quadratic separator, forcing H_2(R) = F_2^n. The static quadratic hull is therefore proved dead as a general SAT preprocessor.
The construction retains a local diagnostic role on explicit relations: computing H_2(R) identifies low-degree invariants, flags coordinates unconstrained by quadratic systems, and confirms whether auxiliary lifts achieve exact closure H_2(R') = R'.
Setting and definitions
Variables evaluate over the Galois field F_2. A relation R ⊆ F_2^n defines the valid truth assignments; F = F_2^n \ R is its complement. The vanishing space I_≤d(R) consists of all multilinear polynomials in F_2[x_1, ..., x_n] with deg(p) ≤ d such that p(r) = 0 for all r ∈ R. The degree-d semantic hull H_d(R) is the common vanishing locus of I_≤d(R).
Static denotes a one-pass construction evaluated once over the unconditioned relation. A quadratic hull specializes this to d = 2. A low-degree separator is an element p ∈ I_≤d(R) that evaluates to 1 on at least one point in F. The analysis compares semantic hulls against root unit propagation without asserting algorithmic equivalence between them.
Method
The result follows from the Reed–Muller code minimum-distance theorem: every non-zero polynomial p ∈ F_2[x_1, ..., x_n] of degree d has weight wt(p) ≥ 2^(n-d). Because any p ∈ I_≤d(R) satisfies supp(p) ⊆ F, the condition |F| < 2^(n-d) forces supp(p) = ∅, whence p = 0. The vanishing ideal contains only the zero polynomial, so H_d(R) = F_2^n.
The clause bounds were verified exhaustively across clause widths k ∈ {1, ..., 8}. The full derivations, verification certificates, and check scripts are provided in this paper's downloadable evidence pack.
Discussion
The barrier is the sparsity of the forbidden set. When |F| falls below 2^(n-d), the degree-d vanishing ideal collapses to zero. For d = 2, a clause of width k ≥ 3 produces a forbidden set of size 1, which sits strictly below the threshold 2^(n-2) for n ≥ 3. No degree-two polynomial can exclude the violating tuple without excluding valid assignments.
Static hulls and unit propagation operate along different axes. Unit propagation applies dynamically to partial assignments during DPLL/CDCL search, forcing literal values when k - 1 literals evaluate to false. A global static hull evaluates over the unconditioned relation and cannot simulate this contextual reduction. Computing the full extensional relation R of an implicit CNF instance to construct its hull would require solving the SAT instance beforehand.
For small, explicitly tabulated sub-relations, the hull acts as an arithmetization diagnostic. It finds all valid quadratic equations, flags underconstrained variables, and checks whether auxiliary extension variables yield an exact quadric formulation.
The register records no corrections, restorations, or scope modifications for ML-052. The Reed–Muller minimum-distance argument is classical, and no separate novelty is claimed.
For everyone — the takeaway
What this means
If a logic rule forbids only one assignment, you cannot write a degree-two equation over binary variables that catches that single violation without accidentally banning valid assignments. A SAT clause with three or more variables bans exactly one combination of inputs. A static quadratic filter always accepts the whole space, missing every violation. Real SAT solvers avoid this by propagating values step-by-step as decisions are made. Static quadratic hulls cannot replace a SAT solver, but they work well as diagnostic checks to verify whether small, hand-crafted algebraic circuits capture their target truth tables.
Attribution and prior art
Prior art: The Reed-Muller minimum-distance property used here is a standard, classical mathematical result, and no novelty is claimed for this component.
Register references
- ML-052
- 07-quadratic-hull-proof-complexity/quadratic_hull_preprocessor.py
- SAT-HULL-CERTIFICATE.json
- SAT_preprocessor_certificate.json
- REPORT.md §§7.1, 7.4, 8
- Reed–Muller minimum-distance ingredient is classical; no separate novelty position is stated.
Every artifact named above is bundled in, or hashed by, this paper's evidence pack below.
Evidence pack
Everything needed to check this entry against its receipts: the register text, a manifest with a SHA-256 hash for every named receipt, and 5 of 5 receipt files bundled (60 KB). Anything not bundled is still hashed in the manifest and lives in the compute-box working trees.
Changelog
Last reviewed 2026-08-29
- 2026-08-29Published on this site.