Algebraic UNSAT Certificates via Positivstellensatz Hierarchy
Built on Charles Dana's 2024 research: Logic Set L and Measureε from the Algorithme.ai SAT framework. The Positivstellensatz hierarchy searches for algebraic refutation certificates — elements l ∈ L where l(x) < 0 for all x ∈ {0,1}n.
curl -X POST https://posit.aws.monce.ai/solve \
-H "Content-Type: application/json" \
-d '{"clauses": [[1,2],[-1,-2],[1,-2],[-1,2]]}'
curl -X POST https://posit.aws.monce.ai/generate \
-H "Content-Type: application/json" \
-d '{"type": "tseitin", "n": 5, "seed": 42}'
Press Solve to start...
Given a CNF φ with clauses C1,...,Cm, each clause defines a function lk : {0,1}n → R[ε]. The Logic Set L is closed under conic combinations and products. If we find l ∈ L with Measureε(l) < 0, then φ is UNSAT — a machine-checkable algebraic certificate.
Level 1 uses Frank-Wolfe on the simplex. Level 2 adds pairwise clause products. Level 3 adds sparse triples. Each level strictly increases proof power.