An Algebraic Approach to MaxCSP
Ilario Bonacina
UPC Barcelona Tech
Jordi Levy
IIIA-CSIC
Aug 15, 2025
SAT’25, Glasgow, UK
Polynomial Calculus for MaxSAT/MaxCSP over multivalued domains:
a proof-construction strategy.
MaxSAT/MaxCSP on polynomials
Input: a set of polynomials \(P=\{p_1,\dots,p_m\}\subseteq \mathbb F[\vec x]\)
Goal: find the maximum # of \(p_i\)s with a common zero in \(\mathbb F\)
(equivalently: find the minimum # \(k_P\) of \(p_i\) not set to zero)
Toy example 1
\(P=\{\ 1+x,\qquad y,\qquad -x-y,\qquad x^2+1\ \}\)
\(P\subset \mathbb Q[x,y]\)
\(k_P=\ ?\)
\(P\subset \mathbb F_3[x,y]\)
\(k_P=\ ?\)
\(P\subset \mathbb F_4[x,y]\)
\(k_P=\ ?\)
Answers: 2, 2, 1
This talk:
an algebraic system (/algorithm) to certify the correctness of \(k_P\) but only for finite fields
What can we encode nicely?
- (Max)SAT instances can be encoded as sets of polynomials:
\(x\lor y\lor \lnot z\) \(\to \{\) \(\bar x \bar yz\)\(,\ x^2-x,\ y^2-y,\ z^2-z, 1-x-\bar x,1-y-\bar y, 1-z-\bar z\ \}\) - Some problems have natural non-Boolean encodings
3-COLORING
\(G=(V,E)\) is 3-colorable
\(\Updownarrow\)
\(VC(G)=\{x_v^2+x_vx_w+x_w^2-1 \mid (v,w)\in E\}\subset \mathbb F_3[\vec x]\)
has a common zero.
Theorem: A set of polynomials \(P\) has no common zeros (in an algebraically closed extension)
\(\Updownarrow\)
\(1\in \langle P\rangle\)
\(\Updownarrow\)
from \(P\) using the inference rules \(\quad\displaystyle\frac{p\quad q}{p+q}\) \(\quad\displaystyle\frac{p}{pq}\quad\) we can derive \(1\)
In Polynomial Calculus \(pq\) is written explicitly as a polynomial.
Polynomial Calculus:
is behind Gröbner bases computations
(used in practice e.g. for verification of multiplier circuits, coloring of graphs, …)is connected with the quest for l.b.s for \(AC_0[\oplus]\)-Frege
is stronger than Resolution
(with natural encoding, otherwise possibly incomparable [Mouli’24])The strength (and understanding) of the system varies a lot
- \(\{0,1\}\)-valued variables (somewhat understood)
- \(\{+1,-1\}\)-valued (not-so understood)
- \(\{1,2\}\)-valued (not a single size l.b.!!)
can be adapted to work for MaxSAT [Bonacina, Bonet, Levy SAT’23]
Theorem ([Bonacina, Bonet, Levy SAT’23]): from a multiset \(P\subset \mathbb F_2[\vec x]\) with cost \(k_P\) over Boolean assignments, using the substitution rules
\[ \displaystyle\frac{p\quad q}{p+q\quad pq\quad pq} \]
and
\[ \displaystyle\frac{p}{pq\quad p(q-1)} \]
and
\[ \displaystyle\frac{p}{q}\quad \text{if }p-q\in \langle x_1^2-x_1,\dots,x_n^2-x_n\rangle \]
we can obtain1 a multiset containing \(1\) with multiplicity \(k_P\)
(and the remaining polynomials with a common zero)
Theorem ([Bonacina, Bonet, Levy SAT’23]): from a multiset \(P\subset \mathbb F_\kappa[\vec x]\) with cost \(k_P\) over Boolean assignments, using the substitution rules
\[ \displaystyle\frac{p\quad q}{p+q\quad pq\quad p((p+q)^{\kappa-1}-1)} \]
and
\[ \displaystyle\frac{p}{pq\quad p(q^{\kappa-1}-1)} \]
and
\[ \displaystyle\frac{p}{q}\quad \text{if }p-q\in \langle x_1^2-x_1,\dots,x_n^2-x_n\rangle \]
we can obtain1 a multiset containing \(1\) with multiplicity \(k_P\)
(and the remaining polynomials with a common zero)
Theorem (this work): from a multiset \(P\subset \mathbb F_\kappa[\vec x]\) with cost \(k_P\) over assignments in \(\mathbb F_\kappa\), using the substitution rules
\[ \displaystyle\frac{p\quad q}{p+q\quad pq\quad p((p+q)^{\kappa-1}-1)} \]
and
\[ \displaystyle\frac{p}{pq\quad p(q^{\kappa-1}-1)} \]
and \[ \displaystyle\frac{p}{q}\quad \text{if }p-q\in \langle x_1^\kappa-x_1,\dots,x_n^\kappa-x_n\rangle \]
we can obtain1 a multiset containing \(1\) with multiplicity \(k_P\)
(and the remaining polynomials with a common zero)
Toy example 1 — cont’d.
\(P\phantom{_1}=\{\ 1+x,\quad y,\quad -x-y,\quad x^2+1\ \}\) \(\subset \mathbb F_3[x,y]\)
\(\displaystyle\frac{p}{q}\quad \text{if }p-q\in \langle x_1^3-x_1,\dots,x_n^3-x_n\rangle\)
\(\displaystyle\frac{p}{pq\quad p(q^2-1)}\)
\(\displaystyle\frac{p\quad q}{p+q\quad pq\quad p((p+q)^2-1)}\)
\(P_1=\{\ 1+x,\quad y, \quad -x-y, \quad (x^2+1)^2, \quad (x^2+1)((x^2+1)^2-1)\ \}\)
\(P_2=\{\ 1+x,\quad y, \quad -x-y, \quad 1\ \}\)
\(P_3=\{\ 1+x+y,\quad (1+x)y,\quad y((1+x+y)^2-1), \quad -x-y, \quad 1\ \}\)
\(P_4=\{\ 1,\quad (1+x+y)(-x-y),\quad (1+x)y,\quad y((1+x+y)^2-1), \quad 1\ \}\)
\(k_P=2\)
Toy Example 2
A proof in the system that \(K_4\) can be \(3\)-colored violating exactly one edge constraint.
\(p_{uv}=x_u^2+x_ux_v+x_v^2-1\in \mathbb F_3[x_u,x_v]\)
Theorem (this work): from a multiset \(P\subset \mathbb F_\kappa[\vec x]\) with cost \(k_P\) over assignments in \(\mathbb F_\kappa\), using the substitution rules
\[ \displaystyle\frac{p\quad q}{p+q\quad pq\quad p((p+q)^{\kappa-1}-1)} \]
and
\[ \displaystyle\frac{p}{pq\quad p(q^{\kappa-1}-1)} \]
and \[ \displaystyle\frac{p}{q}\quad \text{if }p-q\in \langle x_1^\kappa-x_1,\dots,x_n^\kappa-x_n\rangle \]
we can obtain1 a multiset containing \(1\) with multiplicity \(k_P\)
(and the remaining polynomials with a common zero)
Proof sketch (for simplicity for \(\mathbb F_3[x_1,\dots,x_n])\):
Definition: A set of polynomials \(S\) is \(x\)-saturated if
every assignment can be modified in just \(x\) to an assignment satisfying the polynomials in \(S\) depending on \(x\).
Toy Example 3
- Is \(\{\ 1+x,\ y,\ -x-y\ \}\) \(y\)-saturated?
- Is \(\{1+x,xy, (x^2-1)(y-1)\}\) \(y\)-saturated?
Answers: No, Yes
Main Lemma: (Non-trivial!)
Let \(R_x(p)\)\(\stackrel{def}=p|_{x=0}\cdot p|_{x=1}\cdot p|_{x=-1}\).
If for all polynomials \(p_1,p_2,p_3\in S\) depending on \(x\) \[
\left.\begin{array}{l}
R_x(p_1)\\
R_x(p_1+p_2)\\
R_x(p_1-p_2)\\
R_x(p_1+p_2+p_3)\\
R_x(p_1-p_2-p_3)
\end{array}\right\}
\in \langle x_1^3-x_1,\dots,x_n^3-x_n\rangle
\] then \(S\) is \(x\)-saturated.
Lemma (saturation): From \(P\) it is possible to obtain efficiently in the calculus an \(x\)-saturated set of polynomials.
A proof-contruction strategy (\(\sim\) [Bonet, Levy, Manyà ’07])
- saturate the initial polynomials \(P\) w.r.t. \(x_1\)
- saturate the obtained polynomials non depending on \(x_1\) w.r.t. \(x_2\)
- saturate the obtained polynomial non depending on \(x_2\) w.r.t. \(x_3\)
- …
- in the end:
- \(\ell\) polynomials not depending on any variables (i.e. non-zero constants)
- and the Main Lemma ensures the rest of polynomials are satisfiable,
hence \(\ell=k_P\). \(\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\)🍉
Thanks!
- Our work shows completeness of MaxCSP Polynomial Calculus on multivalued variables
- Might be useful in cases when Gröbner bases computations are useful in practice (future work)
- Open: MaxCSP Polynomial Calculus on char 0 fields or rings with zero-divisors
Polynomial Calculus for MaxSAT/MaxCSP over multivalued domains:
a proof-construction strategy.