We present posit, an algebraic proof system for certifying unsatisfiability of Boolean formulas in conjunctive normal form (CNF). The system is grounded in the Logic Set L, a constructive algebraic framework introduced in Dana (2024), where each clause of a CNF formula φ defines a function lk : {0,1}n → R[ε]. The set L is closed under conic combination and pointwise product. If there exists l ∈ L such that l(x) < 0 for all x ∈ {0,1}n, then φ is unsatisfiable — yielding a machine-checkable algebraic certificate.
We implement a three-level hierarchy: Level 1 (conic combinations, solved via Frank-Wolfe), Level 2 (pairwise products), and Level 3 (sparse triple products). The system is preceded by polynomial-time preprocessing (BCP, 2-SAT equivalence/reverse, resolution) and a Tarjan SCC-based 2-SAT solver. We demonstrate that Level 2 certificates can prove Tseitin formulas unsatisfiable in under 150ms — an instance family known to require exponential-length resolution proofs. The system is deployed as a public API at posit.aws.monce.ai. Zero external dependencies; pure Python.
The Boolean satisfiability problem (SAT) asks whether a propositional formula in CNF admits a satisfying assignment. By the Cook-Levin theorem, SAT is NP-complete: every problem in NP reduces to it in polynomial time. The complementary problem — certifying that a formula is unsatisfiable — is coNP-complete and lies at the heart of formal verification, hardware design, and proof complexity.
Modern SAT solvers based on CDCL (Conflict-Driven Clause Learning) are remarkably effective in practice, but their UNSAT proofs are resolution proofs: sequences of derived clauses culminating in the empty clause. Resolution is a complete proof system, but it is not always efficient. Tseitin formulas over expander graphs, for instance, require exponential-length resolution proofs (Ben-Sasson & Wigderson, 1999), despite admitting short proofs in stronger systems.
Algebraic proof systems — Nullstellensatz, Positivstellensatz, and Sum-of-Squares (SOS) — operate in a fundamentally different regime. Instead of syntactically deriving clauses, they search for algebraic certificates: polynomial identities or inequalities that witness unsatisfiability. These systems can be exponentially more powerful than resolution on structured instances.
In this paper, we develop posit, a practical algebraic UNSAT certifier based on the Logic Set L framework introduced in Dana (2024). We make the following contributions:
1. We formalize the Logic Set L as a Positivstellensatz certificate system over the Boolean cube and prove its key closure properties (Theorems 1-3).
2. We implement a three-level hierarchy with polynomial-time certificate search at each level, using Frank-Wolfe optimization on the probability simplex.
3. We combine algebraic certification with classical preprocessing (BCP, TSER, Tarjan 2-SAT) into a unified pipeline.
4. We demonstrate empirically that Level 2 certificates suffice for Tseitin formulas, confirming the theoretical advantage of algebraic systems over resolution.
A CNF formula φ over variables x1, ..., xn is a conjunction of m clauses C1 ∧ ... ∧ Cm, where each clause Ck is a disjunction of literals. A literal is a variable xt or its negation ¬xt. An assignment x ∈ {0,1}n satisfies φ if every clause has at least one true literal.
We work in the polynomial ring R[ε] restricted to evaluations at ε ∈ (0,1). An element Q ∈ R[ε] is a real polynomial Q(ε) = ∑k ak εk. The key property: for ε sufficiently small, the sign of Q(ε) is determined by its lowest-degree nonzero coefficient. This gives R[ε] a natural ordering compatible with the "infinitesimal" interpretation of ε.
where xl = xt if literal l = t (positive), and xl = 1 − xt if literal l = ¬t (negative). When Ck is satisfied by x, at least one factor vanishes and lk(x) = ε > 0. When Ck is unsatisfied, every factor equals 1 and lk(x) = ε − 1 < 0.
Equivalently, using the linear form from Dana (2024): lk(x)(ε) = ck(x) + ε, where ck(x) = bk + ∑t ak,t xt with bk = −1 + |{l ∈ Ck : l < 0}| and ak,t = +1 if t ∈ Ck, −1 if ¬t ∈ Ck, 0 otherwise.
We organize the search for refutation certificates into three levels of increasing expressiveness. Each level d considers elements of L constructible using products of at most d clause functions.
At Level 1, we search for nonneg weights λ1, ..., λm ≥ 0 (on the probability simplex) such that:
Since ck(x) is linear in x, the maximum decomposes per variable:
This is a convex optimization problem, solved via the Frank-Wolfe algorithm on the simplex. Each iteration computes the worst-case assignment x* (the one maximizing the weighted sum), then moves the weight toward the clause most violated at x*. Convergence is O(1/T) in T iterations.
Level 2 augments the basis with pairwise products lk · lj. The product (ck(x) + ε)(cj(x) + ε) captures clause interactions: when one clause is satisfied and one is not, the product's constant term is negative. This is precisely the mechanism that Level 1 cannot express, because conic combinations of individual clause values cannot encode clause-pair correlations.
The Frank-Wolfe search extends over the augmented basis {l1, ..., lm, l1l2, l1l3, ...}, with m + m(m−1)/2 elements. For n ≤ 20, we enumerate all 2n assignments to evaluate the worst case exactly.
Level 3 adds triple products lk lj li, restricted to triples where at least two pairs share a variable. This sparsification keeps the basis manageable (O(m2) rather than O(m3)) while capturing the most structurally relevant interactions.
Before algebraic certification, posit applies polynomial-time preprocessing to simplify the formula. The preprocessing loop repeats until a fixpoint score (counting clauses of length > 2, weighted by variables and literals) stabilizes:
BCP — Boolean Constraint Propagation: unit clause propagation and pure literal elimination, the standard DPLL basis.
TSER — Two-SAT Equivalence and Reverse: from binary clause pairs (a ∨ b) ∧ (¬a ∨ ¬b), deduce a ⇔ ¬b. Propagate equivalences transitively via union-find, then substitute canonical representatives. This discovers hidden variable identities that other techniques miss.
Resolution — Adjacent clause pairs differing by exactly one literal resolve to a shorter clause.
Subsumption — Remove clauses subsumed by shorter clauses.
2-SAT solver — When all remaining clauses have length ≤ 2 (score = 0), solve via Tarjan's SCC algorithm in linear time.
The preprocessing originates from polyn.py (Dana, 2024), a handwritten SAT preprocessor. The score metric measures "distance from P": when score reaches 0, the instance is pure 2-SAT, decidable in polynomial time.
Given a candidate l ∈ L, the Measureε (Dana & Boureau, 2024) provides a scalar assessment of how strongly l certifies UNSAT:
For l(x)(ε) = ∑k ak(x) εk, the integral evaluates to ∑k ak(x) εk/(k+1), which is itself a polynomial in ε. If Measureε(l) < 0 for any ε ∈ (0,1), then l(x) < 0 for all x, certifying UNSAT. The certificate is machine-checkable: given the weights and clause indices, any verifier can recompute the value independently.
The Logic Set L, with conic and product closure, is a restricted Positivstellensatz certificate system over the Boolean cube. The classical Positivstellensatz (Stengle, 1974) states that a system of polynomial inequalities is infeasible iff there exist sum-of-squares certificates witnessing the infeasibility. Over {0,1}n, the Boolean axioms xt2 = xt bound the degree.
Level d of our hierarchy corresponds roughly to degree d in the Positivstellensatz: Level 1 uses only linear combinations of clause polynomials; Level 2 adds quadratic terms (products of two clauses); Level 3 adds cubic terms. The key differences from the standard Sherali-Adams or SOS hierarchies are:
(i) Our basis elements are clause functions lk(x) = ck(x) + ε, with the ε perturbation from R[ε]. This allows the certificate to distinguish "barely satisfied" (l = ε ≈ 0) from "unsatisfied" (l = ε − 1 ≈ −1), which purely constant-term systems cannot.
(ii) The search is performed via Frank-Wolfe on the simplex, which is first-order and derivative-free in the primal variables, avoiding the semidefinite programming required by SOS.
We evaluate posit on several instance families. All timings are from a single core on a t3.medium EC2 instance (2 vCPU, 4GB RAM, eu-west-3). The implementation is pure Python with zero external dependencies.
| Instance | n | m | Status | Method | Time |
|---|---|---|---|---|---|
| [x] ∧ [¬x] | 1 | 2 | UNSAT | Preprocessing | <1ms |
| XOR-UNSAT | 2 | 4 | UNSAT | Preprocessing | <1ms |
| PHP(3,2) | 6 | 9 | UNSAT | Preprocessing | 1ms |
| Tseitin(4 nodes) | 5 | 12 | UNSAT | L2: Pairwise products | 134ms |
| Random 3-SAT (n=10, r=5) | 10 | 50 | UNSAT | Preprocessing | 2ms |
| UNSAT core (n=5) | 5 | 7 | UNSAT | Preprocessing | <1ms |
| PHP(4,3) | 12 | 22 | UNKNOWN | L3 exhausted | 86s |
| Random 3-SAT (n=20, r=5) | 20 | 100 | UNKNOWN | Too large for L | 11ms |
Tseitin formulas encode XOR constraints on graph edges with odd parity, guaranteeing unsatisfiability. They are a canonical hard family for resolution: Ben-Sasson and Wigderson (1999) showed that any resolution proof of a Tseitin formula on an (n, d)-expander requires Ω(2n/d) steps.
Level 2 of posit certifies Tseitin(4) UNSAT in 134ms with an algebraic certificate (objective = −0.066). Preprocessing alone reduces the formula but cannot derive the empty clause. The pairwise product terms capture the XOR structure: each pair of complementary clauses produces a product whose constant term is negative, and the Frank-Wolfe search finds weights that make the total negative everywhere.
This confirms, in a working implementation, the theoretical prediction that algebraic proof systems are exponentially more powerful than resolution on Tseitin formulas.
PHP(4,3) remains UNKNOWN after Level 3 search (86 seconds). This is expected: the pigeonhole principle is known to require degree Ω(n) in Positivstellensatz/SOS (Grigoriev, 2001), and our Level 3 provides at most degree 3. Higher levels (d = 4, 5, ...) would eventually certify it, but the basis size grows as O(md), making this impractical without further structural insights.
Most instances in our benchmark are resolved by preprocessing alone. BCP + TSER + resolution are sufficient for PHP(3,2), random 3-SAT at high clause/variable ratio, and direct contradictions. The preprocessing score metric (counting clauses of length > 2) provides an effective "distance from P" measure: score 0 means pure 2-SAT, decidable by Tarjan's algorithm.
Posit descends from a line of work on SAT and classification:
AUMA (Dana, 2023) — MSc thesis at Ecole Polytechnique, supervised by Erwan Le Pennec. Established that any f : {0,1}n → R is representable as a weighted MAXSAT instance via Fourier decomposition on the Boolean cube. The O(2n/2) local search algorithm and Boolean encodings (φN, φR, φC) for arbitrary domains.
P=NP.pdf (Dana, 2024) — Introduced the Logic Set L, clause functions lk, R[ε] structure, and Measureε. Proved UNSAT on a 10-variable instance in 60 seconds. The ⟨LC⟩ conjecture on the intersection of Logic Sets. Written after hours at Algorithme.ai with GPT assistance on structure.
polyn.py (Dana, 2024) — Handwritten SAT preprocessor: BCP, 2-SAT expansion, TSER, resolution, subsumption. The "POWERFUL AF" comment on TSER was prescient.
Snake (Dana, 2024-2026) — SAT-based explainable classifier. The Dana Theorem: any indicator function over a finite discrete domain can be encoded as a CNF in polynomial time. Snake's oppose() is the constructive proof.
Posit closes the loop: Snake builds SAT from data (classification), posit refutes SAT algebraically (verification). Together they prove that you can construct formulas in polynomial time (Dana Theorem) and certify some of them in polynomial time (Positivstellensatz hierarchy).
Posit demonstrates that the Logic Set L, first sketched in a 2024 startup pitch document, yields a working algebraic proof system that can certify UNSAT where resolution cannot. The key engineering insight is that Frank-Wolfe optimization on the simplex turns the algebraic certificate search into a well-conditioned convex program, tractable in pure Python for n ≤ 20.
Open problems:
1. Scaling. The current implementation enumerates 2n assignments. For n > 20, we need either symbolic evaluation (exploiting clause sparsity) or sampling-based bounds on Measureε.
2. Optimal ε. The choice of ε affects certificate strength. Our experiments use ε ∈ {0.01, 0.1}; a principled selection rule (perhaps via the polynomial's discriminant) could improve hit rates.
3. Higher levels. Level 4+ certificates would handle PHP and other hard families, but the O(md) basis growth needs sparsification — potentially guided by polyauma's Fourier probing.
4. Proof complexity characterization. What is the exact relationship between L-certificates of level d and degree-d Positivstellensatz/SOS proofs? A precise simulation theorem would position L within the proof complexity hierarchy.
5. The ⟨LC⟩ question. Dana (2024) asked whether ∩x L(x) is nonempty for every UNSAT formula. This is equivalent to asking whether L is a complete proof system. We conjecture yes at sufficiently high level, but the constructive bound on the required level remains open.
Live API: posit.aws.monce.ai
Zero dependencies. Pure Python. 1500 lines.
Charles Dana — Tulane University / Monce SAS — 2024-2026