Module sos 

Sum-of-Squares / Positivstellensatz refutation over ℚ — kept EXACT (no SDP, no floating point) by the LP slice of the cone. True SoS is a semidefinite program over the reals; that would forfeit our certified guarantee. Instead we take the diagonal (fixed-square-basis) Positivstellensatz, which is an exact rational linear program: a CNF is lifted to degree-2 pseudo-Boolean inequalities and the lift is refuted by exact Fourier–Motzkin / Farkas elimination.

The lift, over variables xᵢ and the products zᵢⱼ = xᵢ·xⱼ (i < j):

• box: 0 ≤ xᵢ ≤ 1;
• McCormick envelope of each product: zᵢⱼ ≥ 0, zᵢⱼ ≤ xᵢ, zᵢⱼ ≤ xⱼ, zᵢⱼ ≥ xᵢ+xⱼ−1 (the exact integral hull of zᵢⱼ = xᵢ ∧ xⱼ);
• clauses: Σ val(lit) ≥ 1, val(x)=x, val(¬x)=1−x;
• Sherali–Adams products: each clause times xⱼ and times 1−xⱼ (the degree-2 lift);
• squares: (xᵢ−xⱼ)² ≥ 0 and (1−xᵢ−xⱼ)² ≥ 0 — the genuine sum-of-squares terms, the ordered-field content that Nullstellensatz/Polynomial-Calculus (equality-only over GF(2)) cannot express.

Soundness: every constraint holds at every Boolean assignment, so a Boolean model of the CNF is a feasible point of the lift; therefore an infeasible lift (a Farkas refutation) certifies the CNF UNSAT. The elimination is exact i128 and fail-closed under load: it declines (reports no refutation) the moment a coefficient would exceed [MAG_CAP] or the row count would exceed [ROW_CAP], so it never returns an overflow-corrupted verdict. Incomplete at degree 2 (that is the whole point of the degree dial), and the square basis is symmetry-reducible — quotient it by the formula’s automorphisms to shrink the LP, the same “symmetry break to uncover more” that collapses the field cuts and the monomial basis.

Functions

check_sos_certificate

Independently re-check an SoS Farkas certificate from sos_certificate: recompute the degree-2 lift from the clauses, combine its polynomials with the certificate’s multipliers, and confirm the result cancels every variable and leaves a strictly positive constant — the self-contained contradiction 0 < d ≤ 0. It shares no arithmetic with the Fourier–Motzkin elimination that produced the certificate, so it is a genuine independent witness of the refutation (the SoS analog of crate::xorsat::is_refutation). Fails closed on a negative multiplier, an out-of-range row, an empty certificate, or any residual variable.

sos_certificate

The Farkas certificate of a degree-2 SoS refutation: the non-negative multipliers over the lift constraints whose combination is a positive constant ≤ 0. None if no degree-2 refutation is found. Re-checkable: combining the lift polynomials with these multipliers yields a bare positive constant.

sos_refutes

Does a degree-2 Positivstellensatz (diagonal SoS) refutation of the CNF exist over ℚ? Sound: a true result is a certified UNSAT. Declines (false) when no degree-2 refutation exists or the instance exceeds [MAX_VARS] / the elimination caps.