Abstract 1 Introduction 2 Our contributions 3 Outline of the techniques for proving the PC criterion 4 SoS𝜺 Criterion 5 SoS approximability of polynomial systems (SoS) 6 SoS (approximately) simulates PC 7 Proof of the PC criterion 8 Polynomial Calculus and semilattice polymorphism 9 Conclusions and research directions References

On the Degree Automatability of Sum-Of-Squares Proofs

Alex Bortolotti ORCID University of Applied Sciences and Arts of Southern Switzerland, IDSIA, Lugano, Switzerland Monaldo Mastrolilli ORCID University of Applied Sciences and Arts of Southern Switzerland, IDSIA, Lugano, Switzerland Luis Felipe Vargas ORCID University of Applied Sciences and Arts of Southern Switzerland, IDSIA, Lugano, Switzerland
Abstract

The Sum-of-Squares (SoS) hierarchy, also known as Lasserre hierarchy, has emerged as a promising tool in optimization. However, it remains unclear whether fixed-degree SoS proofs can be automated [O’Donnell (2017)]. Indeed, there are examples of polynomial systems with bounded coefficients that admit low-degree SoS proofs, but these proofs necessarily involve numbers with an exponential number of bits, implying that low-degree SoS proofs cannot always be found efficiently.

A sufficient condition derived from the Nullstellensatz proof system [Raghavendra and Weitz (2017)] identifies cases where bit complexity issues can be circumvented. One of the main problems left open by Raghavendra and Weitz is proving any result for refutations, as their condition applies only to polynomial systems with a large set of solutions.

In this work, we broaden the class of polynomial systems for which degree-d SoS proofs can be automated. To achieve this, we develop a new criterion and we demonstrate how our criterion applies to polynomial systems beyond the scope of Raghavendra and Weitz’s result. In particular, we establish a separation for instances arising from Constraint Satisfaction Problems (CSPs). Moreover, our result extends to refutations, establishing that polynomial-time refutation is possible for broad classes of polynomial time solvable constraint problems, highlighting a first advancement in this area.

Keywords and phrases:
Sum of squares, Polynomial calculus, Polynomial ideal membership, Polymorphisms, Gröbner basis theory, Constraint satisfaction problems, Proof complexity
Category:
Track A: Algorithms, Complexity and Games
Copyright and License:
[Uncaptioned image] © Alex Bortolotti, Monaldo Mastrolilli, and Luis Felipe Vargas; licensed under Creative Commons License CC-BY 4.0
2012 ACM Subject Classification:
Mathematics of computing Mathematical optimization
; Theory of computation Discrete optimization ; Computing methodologies Symbolic and algebraic algorithms
Related Version:
Full Version: https://arxiv.org/abs/2504.17756
Funding:
This research was supported by the Swiss National Science Foundation project 200021-207429 “Ideal Membership Problems and the Bit Complexity of Sum of Squares Proofs”.
Editors:
Keren Censor-Hillel, Fabrizio Grandoni, Joël Ouaknine, and Gabriele Puppis

1 Introduction

Semidefinite programming (SDP) relaxations have been a powerful technique for approximation algorithm design ever since the celebrated result of Goemans and Williamson [21]. With the aim to construct stronger and stronger SDP relaxations, the Sum-of-Squares (SoS) hierarchy has emerged as a systematic and versatile method for approximating many combinatorial optimization problems, see e.g. [35, 44, 20, 36]. However, fundamental questions remain unanswered. For instance, it is still unknown under what conditions SoS can be automated, meaning whether one can find a degree-d SoS proof in time nO(d), provided it exists. O’Donnell [41] observed that the prevailing belief regarding the automatability of SoS using ellipsoid algorithms is not entirely accurate. Issues may arise when the only degree-d proofs contain exceedingly large coefficients, thereby hindering the ellipsoid method from operating within polynomial time. In this paper, we establish novel conditions that ensure SoS automatability.

Polynomial optimization

Polynomial optimization asks for minimizing a polynomial over a given set of polynomial constraints. That is, given polynomials r,p1,,pm[x1,,xn], the task is to find (or approximate) the infimum of the following problem:

infxSr(x),whereS={xn|p1(x)==pm(x)=0}. (1)

Typically, S is defined by a set of equality constraints, in this case 𝒫={p1,,pm}, as well as a set of inequality constraints, 𝒬. For all applications considered here, however, it suffices to restrict to the case where 𝒬= and S is finite, enabling the modeling of various relevant combinatorial problems. Nonetheless, we emphasize that our results readily extend to the semialgebraic setting, where 𝒬. For further details, we refer to [9].

A common approach for solving (or approximating) a polynomial optimization problem is by means of sums of squares of polynomials, as we now explain.

Definition 1.1 (SoS Proof System).

Let 𝒫={p1=0,,pm=0} be a set of polynomial equations, and consider a polynomial r[x1,,xn]. An SoS proof of r0 (over S) from 𝒫 is an identity of the form r=i=1t0si2+i=1mhipi, where si,hi[x1,,xn]. Moreover, we say that the above SoS proof has degree at most d if deg(si2)d, for all i[t0], and deg(hipi)d for all i[s]. An SoS refutation of 𝒫 is an SoS proof of 10 from 𝒫.

The SoS hierarchy is based on the following observation: if there exists an SoS proof of rθ0 from 𝒫, then we have that minxSr(x)θ. Moreover, the supremum of the values θ such that there is an SoS proof of rθ0 from 𝒫 of degree d, is called d-th SoS relaxation, also known as the d-th Lasserre relaxation of problem (1) [35, 44]. It turns out that the d-th SoS relaxation can be formulated as an SDP of size nO(d).

SoS relaxations have gained increasing popularity and success; yet, they remain a relatively recent development. Fundamental questions about their properties and capabilities still lack definitive answers. O’Donnell [41] posed the open problem of identifying meaningful conditions that ensure that “small” SoS proofs can be found. We will consider systems 𝒫={p1=0,,pm=0} of polynomials and an “input” polynomial r of degree at most d, with the (mild) assumption that the bit complexity needed to represent 𝒫 and r is polynomial in n. Moreover, we assume that 𝒫 is explicitly Archimedean, i.e. there is N<2poly(nd) such that there exists a “small” SoS proof of Nxi20 from 𝒫 for any variable xi. We restate O’Donnell’s question as follows: Consider an explicitly Archimedean polynomial system 𝒫; under what conditions on 𝒫 does the following property hold?

(P)

Assume there exists an SoS proof of r0 from 𝒫 of degree 2d. Then, for every ε>0, there also exists an SoS proof of r+ε0 from 𝒫 with degree O(d) and coefficients bounded by 2poly(nd,lg1ε).

The assumption of explicitly Archimedeanity guarantees that if there exists an approximate SoS proof of rθ0, then there exists an (exact) SoS proof of rθ+ε0, up to any arbitrary precision ε. Moreover, explicit Archimedeanity implies that the SDP has no duality gap [30]. Therefore, it is often assumed in literature since numerical methods for solving SDPs are guaranteed to converge only when the duality gap is zero.

Nsatz criterion

Since O’Donnell [41] raised his question in 2017, very few papers have been published that address this issue. An initial elegant solution to this question is provided by Raghavendra and Weitz [48], which is based on the Nullstellensatz proof system [4], as we will now outline. For additional results from the literature related to this problem, see Section 1.1.

We denote the vector space of polynomials for variables x1,,xn up to degree d as [x1,,xn]d. Moreover, we denote by I(S)={p[x1,,xn]|p(x)=0xS} the vanishing ideal generated by S, and by Id(S)=I(S)[x1,,xn]d the d-truncated ideal.

Definition 1.2 (Nsatz Proof System).

Consider a system of polynomial equations 𝒫={p1=0,,pm=0}. A Nullstellensatz (Nsatz) proof of p=0 from 𝒫 is a sequence of polynomials (h1,,hm) such that the polynomial identity p=i=1mhipi holds. We say that the proof has degree d if maxi{deghipi}=d. We say that 𝒫 is Nsatz d-complete over S if for every pId(S), the identity p=0 can be derived using a degree-O(d) Nsatz proof from 𝒫.

Next, we recall the criterion proposed by Raghavendra and Weitz for the algebraic setting 111We remark that their criterion is formulated for the semialgebraic setting, i.e., when there are also inequalities.. Moreover, for the sake of clarity of the exposition, we present their result in the case S is finite. We define the algebraic variety S as the set of common zeros of 𝒫={p1=0,,pm=0}. We first observe that this criterion necessitates a technical condition on the solution set S, referred to as δ-spectrality, which we will outline below. Let 𝐯d represent the column vector whose entries correspond to the elements of the standard monomial basis of [x1,,xn]d. For αn, 𝐯d(α) denotes the vector of real numbers obtained by evaluating the entries of 𝐯d at α.

Definition 1.3.

Let S be a finite algebraic variety. We say that S is δ-spectrally rich up to degree d if every nonzero eigenvalue of the moment matrix 1|S|αS𝐯d(α)𝐯d(α) is at least δ.

This property holds for 1δ=2poly(nd) in many natural instances, for example when S{0,1}n, or more in general, when SDn for any finite domain D (see [9] and [48]).

Theorem 1.4 (Nsatz criterion [48]).

Let 𝒫 be a system of polynomial equalities over n variables with solution set S. Assume that

  1. (1)

    S is δ-spectrally rich up to degree d.

  2. (2)

    𝒫 is Nsatz d-complete over S.

Let r be a polynomial and assume there exists an SoS proof of r0 from 𝒫 of degree d. Then, there also exists an SoS proof of r0 from 𝒫 with degree O(d) and with absolute values of the coefficients bounded by 2poly(nd,lg1δ).

This criterion is applicable to various optimization problems, including Max-Clique, Matching, and Max-CSP [48]. However, the Nsatz criterion is subject to significant limitations. First, the criterion is sufficient but not necessary. Second, it is important to observe how the Nsatz criterion (see condition (2) in Theorem 1.4) is influenced by the complexity of a well-known problem known as the Ideal Membership Problem (IMP). This problem involves determining whether an input polynomial r belongs to the ideal generated by {p1,,pm}. We denote the IMP where the input polynomial r has degree at most d=O(1) as IMPd. The IMP was first studied by Hilbert [27] and is a fundamental algorithmic problem with significant applications in solving polynomial systems and polynomial identity testing (see, for example, [18]). In general, the IMP is notoriously intractable, and the results of Mayr and Meyer demonstrate that it is EXPSPACE-complete [39, 40]. It remains unclear under what conditions the IMP is tractable within the Nsatz proof system, specifically regarding when condition (2) in Theorem 1.4 is satisfied. More importantly, the limitations of the Nsatz proof system (see e.g. [20]) affect the applicability of Theorem 1.4. In simpler terms, it is intuitive to suggest that if we could replace the Nsatz proof system with a more powerful proof system, we would be able to broaden the applicability of the criterion to new problems.

Finally, a key limitation – and one of the main open problems left by Raghavendra and Weitz [48, 52] – is the inapplicability of the Nsatz criterion to SoS refutations.

For example the Nsatz criterion does not allow one to show that the following decision problem can be solved in polynomial time.

Problem 1.5 (Degree-d Sum-of-Squares Refutation for CSP).

Given a Constraint Satisfaction Problem (CSP) with constraints ϕ1(x)=0,,ϕm(x)=0 over a finite domain, decide whether:

  • YES: There exists a degree-d sum-of-squares (SoS) proof of the infeasibility of the system, i.e., a derivation of 10 from the axioms ϕ1(x)=0,,ϕm(x)=0 and the domain constraints.

  • NO: No such degree-d SoS proof exists.

Let us call this problem “SoS-CSP”. This is perhaps the most natural formulation of “the SoS algorithm for CSPs”. It is quite striking that we still do not know whether there exists or not a polynomial-time decider for SoS-CSP (even for certain restricted classes of problems).

1.1 References to the related literature

O’Donnell [41] raised the issue of SoS bit complexity in 2017, as discussed in Section 1. He also presented an example of a polynomial system with bounded coefficients that allows for a degree 2 SoS proof, which necessarily has doubly-exponential coefficients.

The aforementioned result (Theorem 1.4) by Raghavendra and Weitz [48] offered an initial elegant, albeit partial, solution. Raghavendra and Weitz expanded O’Donnell’s work and presented an example of a polynomial system containing the Boolean constraints and a polynomial that admits degree 2 SoS proof, but for which any SoS proof of degree O(n) must have coefficients of doubly-exponential magnitude in n.

Interestingly, Hakoniemi [26] demonstrated that both SoS and Polynomial Calculus (PC) refutations over Boolean variables encounter the same bit complexity issue. This finding also raises significant concerns regarding the frequently asserted degree automatability of PC.

Furthermore, strategies in [6, 14, 13, 38, 8] to address the problem of SoS bit complexity involve replacing the original input polynomial constraints 𝒫 with a new set of polynomials 𝒫(d) that satisfies the Nsatz criterion, and generally depends on the SoS degree d. This set 𝒫(d) is computed externally (by an algorithm specifically designed for this purpose 222In general such an algorithm cannot be simulated by SoS. We defer the interested reader to the full version of the paper [9] for details.), serving as the input for SoS in place of 𝒫. For example, in the semilattice case, if 𝒫 consists of m polynomials, the set 𝒫(d), used in [14, 38], is generated by a specific algorithm and has a size of mO(d); that is, 𝒫(d) depends on d and grows exponentially with the SoS degree d. This preprocessing step ensures that SoS retains “low” bit complexity, but only if 𝒫 is substituted with 𝒫(d). Essentially, the approach utilized in [6, 14, 13, 38, 8] is to apply the Nsatz criterion without enhancing or extending it, with the goal of replacing the initial input polynomial system with a new one that is computed externally and satisfies the Nsatz criterion. Our results demonstrate that all preprocessing steps employed in [6, 14, 38, 8] are unnecessary, as SoS achieves low bit complexity for any fixed d when 𝒫 is provided directly as input.

Recently, Gribling et al. [22] showed that, under specific algebraic and geometric conditions, SoS relaxations can be computed in polynomial time. However, as they noted, their algebraic conditions are more restrictive than d-completeness. Their geometric conditions apply to systems of only inequality constraints with full dimensional feasibility set. Additionally, Palomba et al. [42] showed that, under some mild conditions, sum-of-squares bounds for copositive programs can be computed in polynomial time. These results also yielded insights into the bit complexity of SoS proofs.

The quest of characterizing conditions for ensuring tractability of the SoS proof system fits into the more general context of real algebraic geometry, and in particular of the so-called effective Positivstellensatz, i.e., the study of the complexity for representing polynomials using rational sums of squares. To this end, we mention Baldi et al. [1], who recently proved an exponential upper bound on the coefficients’ bit complexity of sums of squares proofs in the general case of radical zero-dimensional ideals when the equality constraints form a graded basis. Furthermore, as observed, SoS feasibility can be reformulated as an SDP feasibility problem, which remains a well-known open question. In this context, we highlight the work of Pataki and Touzov [46], who showed that many SDP’s have feasible sets whose elements have large encoding size. Moreover, they initiated the study of characterizing the conditions under which SDP feasibility sets with large encoding sizes occur.

Several papers in the literature investigate the automatability of the SoS proof system in relation to degree lower bounds. Specifically, various instances have been studied where a set of polynomial equations 𝒫={p1,,pm} and a polynomial q satisfy the condition that “q0 on S”, but any SoS proof of this fact necessarily requires a high degree (see, e.g., [24, 31, 32, 33, 34, 37, 47]). Within the context of the Lasserre hierarchy, these examples correspond to polynomial optimization problems for which many rounds of the hierarchy are needed to reach optimality.

In contrast, our focus is on a different aspect of automatability: we aim to understand under what conditions a fixed-degree level of the Lasserre hierarchy can be computed in time polynomial in the input size (up to a prescribed precision). This shifts the question from degree necessity to degree tractability within a computational framework.

2 Our contributions

Our main contribution is to study and expand the class of polynomial systems for which finding degree-d SoS proofs can be automated. To this end, we first introduce a new criterion based on the Polynomial Calculus (PC) proof system which guarantees that property (P) holds, referred to as the PC criterion. This criterion holds both for SoS refutations and for SoS proofs over feasible systems over finite domains. Remarkably, as we will demonstrate, this criterion applies to a broad class of instances arising from Constraint Satisfaction Problems (CSPs) where the Nsatz criterion does not. Specifically, we will establish tractability results for a broad class of SoS-CSP, and, moreover, prove complete degree-d automatability beyond refutations for certain polynomial systems arising from CSP(Γ). The proof of the PC criterion combines several results, including a simulation of the PC proof system by the SoS proof system together with the development of a different criterion based on the SoS proof system, called the SoSε criterion.

The full version of this paper [9] contains all the details and proofs.

2.1 PC Criterion

We begin by introducing polynomial systems over finite domains, i.e., systems where each variable is restricted to assume values from a fixed set of k rational numbers ρ1,ρ2,,ρk. Given a polynomial system of equations 𝒫 and a finite domain D={ρ1,,ρk}, we say that 𝒫 is a polynomial system over finite domain D if it includes the following domain polynomials:

Dk(xi) =(xiρ1)(xiρ2)(xiρk)=0i[n]. (2)

These polynomials ensure that each variable x1,,xn is constrained to take values from D. Note that this formulation generalizes polynomial systems with Boolean variables, i.e., where the constraint xi2xi=0 enforces xi to be either 0 or 1.

Polynomial Calculus over (PC/), or in short Polynomial Calculus (PC), is a proof system used in computational complexity and proof complexity to study the efficiency of algebraic reasoning. It operates over polynomials and is particularly useful in analyzing the complexity of solving systems of polynomial equations. The goal is to derive the polynomial 1 (i.e., show inconsistency) or to demonstrate that a certain polynomial is implied by the given system. Originally introduced as a refutation system in [17], PC can be viewed as a degree-truncated version of Buchberger’s algorithm [29, 18]. Essentially, PC is a dynamic version of the Nsatz proof system, employing schematic inference rules to reason about polynomial equations. We emphasize that, for the remainder of the paper, we will consider PC in the broader sense of polynomial derivation (so not restricted to refutation) and with polynomials over the reals.

PC consists of the following derivation rules for polynomial equations (f=0),(g=0)𝒫, domain polynomial equations (Dk(xj)=0), variable xj, and numbers a,b

f=0Dk(xj)=0f=0g=0af+bg=0f=0xjf=0 (3)

A PC derivation of r=0 from 𝒫 is a sequence (r1=0,,rL=0) of polynomial equations iteratively derived by using (3) with r=rL. The size of a derivation is the sum of the sizes of the binary encoding of the polynomials in the derivation and the degree is the maximum degree of the polynomials in the derivation. A PC refutation is a derivation of 1=0.

Next, we present one of our main contributions, namely a framework for showing that Property (P) holds for certain polynomial systems over finite domains.

Theorem 2.1 (PC Criterion).

Let 𝒫 be a polynomial system over a finite domain D of k rational values, let S be its variety. Let 𝒢2d be a 2d-truncated Gröbner basis of I(S) according to the grlex order such that 𝒢2d2poly(nd). Assume that, for every g𝒢2d, there exist a PC derivation of g from 𝒫 of size poly(nd) and degree O(d).

Let r be a polynomial and assume there exists an SoS proof of r0 from 𝒫 of degree 2d. Then, for every ε>0, there exists an SoS proof of r+ε0 of degree O(d) such that the absolute values of the coefficients of every polynomial appearing in the proof are bounded by 2poly(nd,lg1ε).

Moreover, suppose 𝒫 is Nsatz d-complete over S. It follows that, for every g𝒢2d, the identity g=0 admits a degree-O(d) Nsatz proof from 𝒫. Further, PC is known to be strictly stronger than Nsatz [17], thus implying that our criterion is also more powerful than the Nsatz criterion. The separation between the Nsatz and the PC criteria is strict and it will be further discussed in Section 2.3.

The proof of Theorem 2.1 combines multiple techniques, which we will present in greater detail in Section 3 and in Section 7. A key component of this proof is the development of a different criterion, the SoSε criterion. As we will see, this criterion provides a more general framework that extends beyond finite domains (see Example˜5.6). Nevertheless, the strong connection between PC and Buchberger’s algorithm makes the PC criterion an effective tool for many instances where the IMPd can be efficiently solved [18].

Two main applications from CSPs

In the following, we present our main two applications of Theorem 2.1. In both cases we focus on restricted classes of Constraint Satisfaction Problems (CSPs), denoted as CSP(Γ), where constraints are limited to relations from a specified set Γ. These language restrictions have proven effective for analyzing computational complexity classifications and other algorithmic properties of CSPs, leading to recent breakthroughs in [11, 53, 54] (see, e.g., [3, 12, 16] and [9] for further details and necessary background).

2.2 First main application: refutation for bounded width CSPs

All known tractable Constraint Satisfaction Problems CSP(Γ) for a fixed constraint language Γ are solvable using two fundamental algorithmic principles. The first relies on the few subpowers property (see e.g. [3]). The second, local consistency checking, is the most widely known and natural approach for solving CSPs [2, 3, 11].

We consider the class of constraint languages Γ for which CSP(Γ) has bounded width, meaning that it can be solved by a local consistency checking algorithm (see e.g. [2, 3]). Identifying and characterizing such languages is crucial for understanding the tractability of constraint satisfaction problems [2, 3]. Note that for languages that rely on the few subpowers property in general SoS requires high degree for refutation [3, 2, 23].

As a corollary of Theorem 2.1, we establish the polynomial-time feasibility of the SoS refutations for the whole class SoS-CSP(Γ) problems (see ˜1.5) for which CSP(Γ) has bounded width.

Corollary 2.2.

For constraint languages Γ over finite domains for which CSP(Γ) has bounded width, the SoS-CSP(Γ) ˜1.5 can be solved in polynomial time for any fixed degree d.

Proof sketch.

For refutations, Theorem 2.1 requires that there exists a PC derivation of 1=0 from 𝒫 of size poly(nd) and degree O(d). The claim follows by observing that the local consistency algorithm can be simulated by a truncated Buchberger’s algorithm (that we call PC). Thus, any information obtained by enforcing local consistency, and therefore, by definition, by deciding any bounded width language, can be obtained by performing a truncated Buchberger’s algorithm [29, 10].

Note that both the decision and search versions of ˜1.5 with bounded width are solvable in polynomial time for any fixed degree d, as a consequence of Theorem 2.1.

Further, we mention that in [51] it was obtained a similar result in the context of the Sherali-Adams proof system. However, this result applies only to a fixed limited form of P, namely the Boolean canonical linear program. As remarked in Section 1.1, our focus is on deriving SoS proofs directly from 𝒫 with variables over general finite domains without any preprocessing. To this end, in Corollary 2.2, we demonstrate that for any system of equations 𝒫 over a finite domain that defines a bounded-width relation, finding SoS refutations directly derived from 𝒫 can be automated.

2.3 Second main application: strong separations arising from CSPs

As second application of Theorem 2.1, we examine constraint languages (and polynomial equations) that are closed under the semilattice and dual discriminator polymorphisms333In the context of CSPs, a polymorphism is a special kind of function that helps us understand the structure of the constraints. Specifically, it is a function that combines multiple solutions of a CSP in a way that still satisfies the constraints. Polymorphisms are useful because they reveal patterns in the constraints, and studying them can help determine how easy or hard a CSP is to solve. We refer to [9, 3] for a formal definition. (see, e.g., [3] and [9] for the necessary background). Propositional formulas from HORN-SAT or 2-SAT can be easily translated into system of polynomial equations that are semillatice or dual discriminator closed, respectively. Moreover, these two classes extend HORN-SAT and 2-SAT formulas, respectively, to general finite domain cases and have held a significant role in the theory of Constraint Satisfaction Problems of the form CSP(Γ); see, e.g., [3, 12] and references therein.

Theorem 2.3.

For a system 𝒫 of polynomial equations over n variables that is closed under the semilattice (or dual discriminator) polymorphism, then the PC criterion (Theorem 2.1) applies.

Note that these classes of problems are known to be bounded width (see e.g. [3]). Therefore, by Corollary 2.2 the refutation ˜1.5 can be solved in polynomial time. However, Theorem 2.3 establishes a significantly stronger result. Indeed, Theorem 2.3 indicates that any degree d SoS proof of p0, for any polynomial p, can be computed in nO(d) time with arbitrary precision (not only degree-d SoS proofs for 10, as required by refutation).

We emphasize that Buss and Pitassi [15] show that the Nsatz proof system necessitates a degree Θ(logn) proof for the induction principle INDn, a polynomial inference rule that can be formalized as a derivation in either HORN-SAT or 2-SAT formulae. As a result, if 𝒫 is closed under the semilattice (or dual discriminator) polymorphism, it cannot be Nsatz d-complete for any d=o(logn). Thus, Theorem 2.1, Theorem 2.3 and [15] establish a clear separation between the PC criterion and the Nsatz criterion.

Polynomial Calculus (PC) is a rule-based, dynamic extension of Nullstellensatz (see e.g. [20]). Due to its dynamic nature, it can sometimes achieve a refutation of significantly lower degree through cancellations than would be possible with the static Nullstellensatz system. A notable example is the induction principle INDn mentioned above, which has degree 2 refutations in PC. By contrast, its Nullstellensatz degree has been shown to be Θ(logn) [15].

We demonstrate that PC, in addition to solving refutation for the very special case of INDn with low degree, also addresses the much more general Ideal Membership Problem IMPd in nO(d) time for two families of problems that significantly generalize HORN-SAT and 2-SAT in multiple respects and apply to all finite rational domains. This also demonstrates that PC is complete and free from bit complexity issues for these problems (Hakoniemi recently raised concerns regarding the bit complexity in PC [26], see also Section 9).

This result is not only intrinsically interesting but also closely aligned with the main goal of this article. Indeed, the PC criterion demonstrates that solvability via Polynomial Calculus and the bit complexity of Sum-of-Squares are deeply interconnected. Finally, we emphasize that it is not implied by the recent result of Bulatov and Rafiey [14]; more details are given in Section 8 and in the full version of the paper [9].

The proof of this broad generalization is technically complex and lengthy, necessitating a dedicated space with the necessary preliminaries. Consequently, given space constraints, we outline the proof only for the semilattice case in Section 8, while the full discussion – including a detailed review, the proof, the underlying intuition and the literature review – is deferred to the full version [9].

This paper aims to deepen our understanding of the bit complexity issue and to explore the conditions under which it arises. For instance, we demonstrate that all preprocessing steps aimed at replacing 𝒫 with a new set 𝒫 to satisfy the Nsatz criterion, as used in [14, 38, 7, 6, 8] to circumvent the bit complexity issues of SoS for semilattice and dual discriminator polymorphisms, are unnecessary. Specifically, SoS, when applied directly to 𝒫 as input, achieves low bit complexity for any fixed d (refer to [9] for a more detailed discussion). This result appears to support and extend the hypothesis that CNF formulas do not exhibit a bit complexity issue, an open question posed by Hakoniemi [26] (see also Section 9).

3 Outline of the techniques for proving the PC criterion

Below we outline the main techniques that will be used in the proof of the PC criterion.

  1. 1.

    SoS𝜺 criterion (Section˜4). We start by presenting a general criterion, called the SoSε criterion, which guarantees that Property (P) is satisfied, and thus that SoS can be automated. This criterion, which is a simple generalization of the Nsatz criterion [48] (see Theorem 1.4), serves as a foundation and basic tool for presenting our main contributions. The key distinction is that the SoSε criterion requires an approximate version of completeness, making it more flexible and thus stronger than Theorem 1.4, as emphasized in Section˜4.

  2. 2.

    SoS approximability of polynomial systems (Section˜5). A main difference between the Nsatz criterion and the SoSε criterion is that the latter requires completeness only approximately. This relaxation allows to leverage the SoS proof system to yield a provably stronger criterion. With this aim, in Section Section˜5 we present the notion of SoS-approximation between polynomial systems, which turns out to be a powerful tool for showing SoSε completeness, and applying the SoSε criterion.

  3. 3.

    SoS approximately simulates PC (Section 6). In general, PC and SoS are incomparable [25]. However, in the presence of domain restrictions, this is not necessarily true. In a surprising result, Berkholz [5] showed that over Boolean variables, SoS simulates PC for refutations, while for the converse there is a strict separation (see e.g. [20]). A primary contribution of this paper is the extension of Berkholz’s result to general polynomial derivation in which the variable domains are finite rational sets (see Section 6). We highlight that, although the overall structure of the proof partially mirrors that in [5], there are notable differences. In particular, new ideas and techniques are introduced in the simulation of the multiplication rule of PC.

In the following sections, we explore these three concepts in more detail. Then, in Section 7, we combine these techniques to prove the PC criterion (Theorem 2.1).

4 SoS𝜺 Criterion

First, we introduce the SoSε criterion which guarantees that Property (P) holds and is a simple generalization of the Nsatz criterion [49] (see Theorem 1.4).

We start by introducing the notion of SOSε-completeness, which is a strengthening of the d-completeness for Nsatz. We set S=maxαSα, where α is the usual Euclidean norm in n. Let p=αcαxα, we define p=maxα|cα|. Similarly, for a set of polynomial we have 𝒫=maxp𝒫p.

Definition 4.1 (SOSε-completeness).

We say that 𝒫 is SoSε-d-complete over S (or simply SoSε-complete) if, for every polynomial in the 2d-truncated vanishing ideal qI2d(S) and every ε>0, there exists an SoS proof of q+ε0 of degree O(d) from 𝒫 with absolute value of the coefficients bounded by 2poly(nd,lgq,lg1ε).

We proceed by stating the SoSε criterion. In essence, the criterion reduces the analysis of the existence and efficiency of SoS proofs to the ideal generated by the polynomial constraints.

Theorem 4.2 (SoSε criterion).

Consider a polynomial system 𝒫={p1=0,,pm=0} with finite variety S such that S2poly(nd). Assume that

  1. 1)

    S is δ-spectrally rich up to degree d, and

  2. 2)

    𝒫 is SoSε-complete over S.

Let r be a polynomial and assume there exists an SoS proof of r0 from 𝒫 of degree 2d. Then, for every ε>0, there exists an SoS proof of r+ε0 of degree O(d) such that the absolute values of the coefficients of every polynomial appearing in the proof are bounded by 2poly(nd,lg1δ,lg1ε).

The main obstacle for applying the SoSε criterion is proving SOSε-completeness, analogous to the case when applying the Nsatz criterion. We are able to overcome this obstacle for our purposes. Specifically, in Section˜5 we develop novel approximation techniques for showing SOSε-completeness. Moreover, the exploitation of these techniques will also lead to the proof of the PC criterion.

SoS𝜺 completeness vs Nsatz completeness

We now highlight some differences distinguishing the two notions of completeness.

Radicality. When the ideal generated by the input polynomials 𝒫 is not radical, the Nsatz proof system is inherently weak and the Nsatz criterion becomes inapplicable, as the d-completeness property cannot be satisfied. In contrast, we demonstrate that the SoSε criterion is more robust and may still be effective for non-radical ideals (see Example˜5.6).

Role of ε in the criteria. We highlight that our criterion asks for an approximated proof of the nonnegativity of the elements in the truncated ideal I2d(S). This seemingly subtle difference has a significant impact on the application of the criterion. Indeed, we will encounter cases (see e.g. Example˜5.6) where for some qI2d(S) there is no SoS proof for q0 but there exists one for q+ε0 satisfying the criterion conditions. This shows that not only replacing the proof system with stronger one (Nsatz with SoS) plays a role, but also extending it to an approximate form. We further note that allowing this approximation in the condition has an impact in the result of the criterion. Whereas the Nsatz criterion shows the existence of an SoS proof of r0 with bounded coefficients, the SoSε criterion guarantees the existence of a proof of r+ε0 with bounded coefficients. However, following the discussion in the introduction, this second property is enough to guarantee the polynomial-time computability (up to arbitrary precision) and essentially does not compromise the quality of the computed solutions.

5 SoS approximability of polynomial systems (SoS)

In this section we develop techniques for showing when a polynomial system is SOSε-complete. We will consider multiple polynomial systems 𝒬 preserving geometric and bit complexity properties of 𝒫, namely

  1. A1.

    Same zero set S.

  2. A2.

    Same degree order: deg(q)=O(d), q𝒬, where d is the maximum degree of the polynomials in 𝒫.

  3. A3.

    Polynomial bit complexity: the bit complexity for representing 𝒬 is polynomial in n.

We now present the notion of SoS approximation between polynomial systems with same zero set, which turns out to be a powerful tool for showing SOSε-completeness. We will also demonstrate that SoS-approximability provides a powerful tool for showing that a polynomial system 𝒫 is SOSε-complete. We refer to [9] for a complete exposition.

Definition 5.1 (SoS approximation).

Let 𝒫={p1=0,p2=0,,pm=0} and 𝒫={p1=0,p2=0,,pl=0} be two polynomial systems with the same variety. We say that 𝒫 SoS-approximates 𝒫, and it is denoted by 𝒫SoS𝒫, if for every p𝒫 and every ε>0 there exist SoS proofs

p+ε0 from 𝒫 andp+ε0 from 𝒫

with degree O(d) and with coefficients bounded by 2poly(nd,lg1ε).

Notably, the relation SoS induces an inheritance property of the SOSε-completeness.

Theorem 5.2.

Let 𝒫1 and 𝒫2 be polynomials systems with zero set S. Assume that 𝒫1 is SOSε-complete and that 𝒫2 is explicitly Archimedean. If 𝒫1SoS𝒫2, then 𝒫2 is SOSε-complete.

Furthermore, under the mild assumption of explicit Archimedeanity, approximations can be “chained” together via a transitivity property.

Lemma 5.3 (Transitivity).

Let 𝒫1,𝒫2 and 𝒫3 be three systems of polynomials with zero set S. Assume that 𝒫3 is explicitly Archimedean. If 𝒫1SoS𝒫2 and 𝒫2SoS𝒫3, then 𝒫1SoS𝒫3.

We define the α-power of 𝒫 as the set 𝒫α={p1α1,,pmαm}, where α=(α1,,αm)m. The next result shows that α-powers of a polynomial set approximate the set itself.

Proposition 5.4.

Let αn, with |α|=O(d). Then, 𝒫SoS𝒫α.

It follows that the problem of showing that an explicitly Archimedean system 𝒫 is SOSε-complete can be reduced to identifying SoSε-complete polynomial systems 𝒬 such that 𝒬SoS𝒫. A broad class of such reductions arises from Gröbner basis theory for which we have the following result. Here we use the fact that, by definition, a Gröbner basis 𝒢 is d-complete, thus SOSε-complete.

Proposition 5.5.

Let 𝒫 be an explicitly Archimedean polynomial system and let 𝒢2d be a 2d-truncated Gröbner basis of I(S) according to the grlex order. Assume that 𝒢2d2poly(nd). If there exists a multi-index α with |α|=O(d) such that 𝒢αSoS𝒫, then 𝒫 is SOSε-complete.

Finally, we provide an example of a polynomial system 𝒫 for which the the ideal generated 𝒫 is non-radical and thus both the Nsatz and the PC criteria are inapplicable, yet the SoSε criterion remains applicable through SoS approximations. This example demonstrates that the SoS criterion can be extended beyond polynomial systems over finite domains and that it could potentially lead to new interesting results.

Example 5.6 (Example of separation | Non-radical ideal).

Let 𝒫={x12+x22++xn2}, then we have S={(0,0,,0)}. Observe that x1=0 does not have a Nsatz proof, thus the Nsatz criterion does not apply. Clearly the reduced Gröbner basis of I(S) is 𝒢={x1,,xn}. Moreover, it is immediate to see that 𝒢(2,2,,2)SoS𝒫. Hence, by Proposition˜5.5 it follows that 𝒫 is SOSε-complete. Note that x10 does not have a SoS proof from 𝒫. This further confirms that introducing an additive error in the definition of SOSε-completeness enables us to address the non-radical case, in contrast to the Nsatz criterion.

6 SoS (approximately) simulates PC

Berkholz [5] related different approaches for proving the unsatisfiability of a system of real polynomial equations. Over Boolean variables, he showed that SoS simulates PC refutation: any PC refutation of degree d can be converted into an SoS refutation of degree 2d, with only a polynomial increase in size. In the non-Boolean setting, there are systems of equations that are easier to refute for PC than for SoS [25]. Grigoriev and Vorobjov [25] show that the simulation of PC by SoS does not hold in the non-Boolean case, namely when the Boolean axioms xj2xj=0 are omitted. For example, the so-called telescopic system of equations, {yx1=1,x12=x2,,xn12=xn,xn=0}, has a PC refutation of degree n, but it requires exponential refutation degree in SoS [25]. It is worth noting that a similar (although much weaker than the one present in Lemma 6.1) generalization of Berkholz’s result was considered in [50], when the variables take the values ±1, and in [45], for a variation of PC endowed with a “radical rule” and a “sum-of-squares rule”. However, it is not known if SoS can simulate PC in the (non-Boolean) general domain setting, namely when variables can take values from a general finite set of values. In this section, we address the existing knowledge gap by extending Berkholz’s result to general domains. This complements the results in [25, 5].

The overall structure of the proof partially mirrors that in [5], but with notable differences. In particular, new ideas and techniques are introduced in the simulation of the multiplication rule of PC. For all technical details, we refer to the full version of the paper [9]. In summary, we first derive the following lemma.

Lemma 6.1.

Let 𝒫 be a system of polynomial equations over a finite domain D with |D|=k. Assume that r=0 has a PC derivation of degree d and size S from 𝒫. Then r20 has an SoS proof of degree 2(d+k1) with coefficients of size poly(k,S).

Furthermore, note that the result holds for the particular case of refutations, i.e. when r=1. Indeed, if there exists a PC refutation of 𝒫, i.e., a derivation of 1=0, then Lemma 6.1 implies that there exists an SoS refutation 10 with only polynomial increasing.

Then, employing Lemma 6.1, we prove that SoS approximates PC as a proof system in the context of polynomial systems over finite domains. Specifically, if there exists a PC derivation of r=0 with degree d and size S, then for every ε>0, we have SoS proofs of r+ε0 and r+ε0 with degree O(d+k) and coefficients bounded by 2poly(k,S,lg1ε).

Theorem 6.2.

SoS approximates PC with degree linear in the domain size k.

Proof.

Assume there is a PC derivation of r=0 from 𝒫. Then the polynomial systems 𝒫, 𝒫{r} and 𝒫{r2} have the same zero set. Moreover, by Lemma 6.1, it follows that 𝒫{r2}SoS𝒫. Further, by Proposition˜5.4, it follows that 𝒫{r}SoS𝒫{r2}. Thus, by transitivity of Lemma˜5.3, we have that 𝒫{r}SoS𝒫, i.e. there exist SoS proofs of r+ε0 and r+ε0 from 𝒫 of degree O(2(d+k1)) and coefficients bounded by 2poly(k,S,lg1ε).

7 Proof of the PC criterion

Now we are able to prove the PC criterion (Theorem 2.1) by combining the techniques develop in the last sections. We first state two preliminary lemmas about polynomial systems over finite domains. See the full version [9] for complete details.

Lemma 7.1.

Let 𝒫 be a polynomial system of equations over finite domain D. Then 𝒫 is explicitly Archimedean.

Lemma 7.2.

Let 𝒫 be a polynomial system of equations over finite domain D. If 𝒫 has non-empty zero set, i.e. S, then S is δ-spectrally rich up to degree d for δ>2poly(nd).

Proof of Theorem 2.1..

We divide the proof into two cases depending on whether S is empty or not:

  1. 1.

    If S=, then 𝒢2d={1}, which corresponds to the case of refutations. By assumption, there exists a PC derivation of 1=0 from 𝒫 of size poly(nd) and degree O(d). Then, by Lemma 6.1, we have a proof of 10 from 𝒫 of degree O(d), and coefficients bounded by 2poly(nd), as desired.

  2. 2.

    If S, then we apply Theorem 4.2 (SoSε criterion). By Lemma 7.2, S is δ-spectrally rich up to degree d for some δ>2poly(nd), it remains to show that 𝒫 is SoSε-complete over S. By assumption, there are PC derivations for all elements in 𝒢2d of size poly(nd). Then, by Lemma 6.1, for all g𝒢2d, we have an SoS proof of g20 from 𝒫 of degree O(d), and coefficients bounded by 2poly(nd). Clearly, we also have a proof of g20 of degree O(d) and coefficients bounded by 2poly(nd). Then, we have that 𝒢(2,,2)SoS𝒫. Finally, by Proposition 5.5 and by Lemma 7.1 𝒫 is explicitly Archimedean, we obtain that 𝒫 is SoSε-complete, completing the proof.

8 Polynomial Calculus and semilattice polymorphism

In this section we provide the outline of the Proof of Theorem 2.3 for the semilattice part. The necessary background and full details can be found in [9] (see also [3, 14, 38] for the necessary background).

We consider the complexity of IMPd(Γ) for constraint languages Γ closed under a semilattice operation ψ (either meet or join). There are two kinds of semilattice operations (see e.g. [19]). A join-semilattice, also known as an upper-semilattice, refers to a partially ordered set that possesses a join (or least upper bound) for every nonempty finite subset. Conversely, a meet-semilattice, or lower-semilattice, is a partially ordered set characterized by having a meet (or greatest lower bound) for any nonempty finite subset. Algebraically, semilattices can be defined as pairs 𝒟=(D,ϕ), where D is a domain and ϕ is the semilattice operation join or meet. Note that both operations are associative, commutative and idempotent binary operations.

In the following, we show that standard PC is d-complete and efficient for constraint languages that are closed under a semilattice polymorphism. Our result greatly simplifies known approaches [14, 38] and unifies them into one simple PC-based algorithm. Further details explaining the substantial differences with what is already known are given and discussed in Remark 8.2.

The input to IMPd(Γ) consists of any given set of polynomials that defines the combinatorial ideal I𝒞 corresponding to a semilattice closed language Γ:

𝒫={fR1(XR1),,fR(XR),fD(x1),,fD(xn)}, (4)
I𝒞=𝒫 (5)

where, fRi(XRi) corresponds to the interpolating polynomial of variables {XRi} assuming value 0 for every tuple in Ri. Similarly, fD(xi) is the univariate polynomial that interpolates domain D. We want to show that PC is capable of computing the d-truncated Gröbner basis (in grlex order) in polynomial time for any fixed d.

Our main technical result is as follows.

Theorem 8.1.

Let Γ be a finite constraint language over a domain D. Consider an instance 𝒞 of CSP(Γ). If Γ is closed under a semilattice polymorphism, then O(d)-degree PC  can compute in nO(d) time the reduced d-truncated Gröbner basis 𝒢d (in grlex order) of the combinatorial ideal I𝒞, for any degree d and where n is the number of variables.

Proof outline.

Schematically, Theorem 8.1 is proven by the following arguments:

  1. 1.

    First we prove Theorem 8.1 for the Boolean case, where the domain D={0,1}. That is, we show that bounded-degree PC computes the d-truncated Gröbner basis of the combinatorial ideal I𝒞 if Γ is a semilattice-closed language over the Boolean domain. The known [38] algorithm to efficiently compute the d-truncated Gröbner basis consists of “guessing” the truncated Gröbner basis in polynomial time. Here, the main technical difficulty is that this guessing “trick” is not immediately simulable in an efficient way by PC. We show that the latter is possible. The algorithm in [38] essentially reduces the IMP for a given polynomial f in the 2d-truncated Gröbner basis to the (contrapositive) problem of checking whether “non-vanishing assignments” of variables for f belong to the variety. In this work, we are able to PC-derive f by polynomially formulating “non-vanishing assignments” into an infeasible system of Horn-type polynomials. We then combine algebraic and logical reasoning, leading us to efficient PC refutations of the new system by means of simulation of refutation proofs. By accurately using the PC ability for refutation, we can then retrieve a PC derivation of f. This technique may be of independent interest.

  2. 2.

    We reduce the general case (with arbitrary finite domain D) to the Boolean case. The reduction is achieved by encoding the domain D using strings over {0,1}. The encoding is given by a novel bijective map that preserves the semilattice structure. The strength of our bijection is that it ensures a one-to-one correspondence between the solution spaces of the original CSP over D and the reduced Boolean problem, which allows us to reduce the (search version of) IMPd(Γ) to the (search version of) IMPO(d)(Γ01), where Γ01 is a Boolean constraint language derived from Γ. Crucially, the preservation of the semilattice structure ensures that IMPO(d)(Γ01) remains solvable in polynomial time by PC.

Theorem 8.1 in conjunction with Theorem 2.1 implies Theorem 2.3 for semilattice structures.

 Remark 8.2.

We emphasize that a reduction to the Boolean domain case has also been used to prove that the decision version of IMPd(Γ) is tractable for such constraint languages Γ (see [14, Th. 5.10] for more details). However the mapping used in [14] is by the means of pp-interpretability (see [43]), and it is not guaranteed that one can recover proofs for the finite domain under this reduction. In particular, the very first obstacle is given by the fact the mapping π in the definition of pp-interpretability [14, Def. 3.12] is not guaranteed to be a bijection. In fact, this difficulty of transforming the Boolean case proof to the finite general domain case led to the development of a specific method [14, Th. 6.5] for the search version of the problem. Moreover, it is far from evident that it can be simulated by PC, as their methods also apply to 3Lin(2), for which linear (thereby, sharp) lower bounds on the degrees of SoS refutations are known [23]. It follows that bounded degree SoS and PC over the reals cannot simulate the algorithm in [14, 6, 8]. We refer to [9] for a more detailed discussion.

9 Conclusions and research directions

In this paper it is shown that for two classes of problems that generalize HORN-SAT and 2-SAT a PC proof of degree d can be found in time nO(d), if it exists (see also [6] for related results). This is obtained by first showing that a (truncated) Gröbner basis for the graded lexicographic order can be computed by PC in polynomial time for any fixed d (and therefore with polynomial bit complexity). By a simple polynomial division argument, the latter implies that for these two classes there are no bit-complexity issues. Furthermore, both HORN-SAT and 2-SAT, along with their generalizations to finite domains – semilattice and dual-discriminator closed languages, respectively – fit within the framework of bounded width languages [28]. As a step towards understanding the boundary of tractability of the PC criterion, it would be interesting to explore how PC can be applied to solve the IMPd(Γ) for bounded width languages. Moreover, results regarding the tractability of the IMPd, even when using restricted form of algorithms such as those encapsulated in the Polynomial Calculus proof system, would be valuable on their own right.

Similar to SoS, it has often been stated that a PC refutation of degree d can be found in time nO(d), if it exists. For PC over finite fields, this is already clear from the algorithm provided in [17]. However, in the case of PC over reals or rationals, the search for proofs can potentially result in bit complexity issues as recently shown by Hakoniemi in [26]. Indeed, in [26] it is shown that there is a set of polynomial constraints Qn on Boolean variables that has both SoS and PC over rationals refutations of degree 2, but for which any SoS or PC refutation over rationals must have exponential bit-complexity. The author remarks that the constraints in Qn do not arise from any CNF, and raise the open question to understand whether the two measures of bit-complexity and monomial-size are polynomially equivalent for CNFs. Our PC criterion does not apply to other CNF problems like 3Lin(2), where PC and SoS are known to be not complete for any fixed d. Moreover, we remark that 3Lin(2) problems do not arise from bounded width languages [2]. As an intermediate step for the open question raised in [26], it would be interesting to understand the bit complexity of problems with these CNF constraints.

In this paper, we have made partial advancements in the understanding of the bit complexity of SoS, an issue that has only recently garnered attention and remains in its early stages of research. Since it was first raised 2017, progress has been relatively limited. In this section, we have offered some insights that we hope will stimulate further exploration and enhance our understanding of this fundamental problem.

References

  • [1] Lorenzo Baldi, Teresa Krick, and Bernard Mourrain. An effective positivstellensatz over the rational numbers for finite semialgebraic sets, 2024. arXiv:2410.04845.
  • [2] Libor Barto and Marcin Kozik. Constraint satisfaction problems solvable by local consistency methods. J. ACM, 61(1), January 2014. doi:10.1145/2556646.
  • [3] Libor Barto, Andrei Krokhin, and Ross Willard. Polymorphisms, and How to Use Them. In Andrei Krokhin and Stanislav Zivny, editors, The Constraint Satisfaction Problem: Complexity and Approximability, volume 7 of Dagstuhl Follow-Ups, pages 1–44. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl, Germany, 2017. doi:10.4230/DFU.Vol7.15301.1.
  • [4] Paul Beame, Russell Impagliazzo, Jan Krajícek, Toniann Pitassi, and Pavel Pudlák. Lower bound on Hilbert’s Nullstellensatz and propositional proofs. In 35th Annual Symposium on Foundations of Computer Science, Santa Fe, New Mexico, USA, 20-22 November 1994, pages 794–806, 1994. doi:10.1109/SFCS.1994.365714.
  • [5] Christoph Berkholz. The Relation between Polynomial Calculus, Sherali-Adams, and Sum-of-Squares Proofs. In Rolf Niedermeier and Brigitte Vallée, editors, 35th Symposium on Theoretical Aspects of Computer Science (STACS 2018), volume 96 of Leibniz International Proceedings in Informatics (LIPIcs), pages 11:1–11:14, Dagstuhl, Germany, 2018. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. doi:10.4230/LIPIcs.STACS.2018.11.
  • [6] Arpitha P. Bharathi and Monaldo Mastrolilli. Ideal membership problem for boolean minority and dual discriminator. In Filippo Bonchi and Simon J. Puglisi, editors, 46th International Symposium on Mathematical Foundations of Computer Science, MFCS 2021, August 23-27, 2021, Tallinn, Estonia, volume 202 of LIPIcs, pages 16:1–16:20. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2021. doi:10.4230/LIPIcs.MFCS.2021.16.
  • [7] Arpitha P. Bharathi and Monaldo Mastrolilli. Ideal membership problem over 3-element csps with dual discriminator polymorphism. SIAM J. Discret. Math., 36(3):1800–1822, 2022. doi:10.1137/21M1397131.
  • [8] Arpitha P. Bharathi and Monaldo Mastrolilli. Ideal membership problem for boolean minority and dual discriminator. SIAM Journal on Discrete Mathematics, 39(1):206–230, 2025. doi:10.1137/23M1556010.
  • [9] Alex Bortolotti, Monaldo Mastrolilli, and Luis Felipe Vargas. On the degree automatability of sum-of-squares proofs, 2025. arXiv:2504.17756.
  • [10] Andrei Bulatov. Personal communication, 2023.
  • [11] Andrei A. Bulatov. A dichotomy theorem for nonuniform CSPs (best paper award). In 58th IEEE Annual Symposium on Foundations of Computer Science, FOCS 2017, Berkeley, CA, USA, October 15-17, 2017, pages 319–330, 2017.
  • [12] Andrei A. Bulatov. Constraint satisfaction problems: Complexity and algorithms. ACM SIGLOG News, 5(4):4–24, November 2018. doi:10.1145/3292048.3292050.
  • [13] Andrei A. Bulatov and Akbar Rafiey. On the complexity of csp-based ideal membership problems. CoRR, abs/2011.03700, 2020. arXiv:2011.03700.
  • [14] Andrei A. Bulatov and Akbar Rafiey. On the complexity of csp-based ideal membership problems. In Stefano Leonardi and Anupam Gupta, editors, STOC ’22: 54th Annual ACM SIGACT Symposium on Theory of Computing, Rome, Italy, June 20 - 24, 2022, pages 436–449. ACM, 2022. doi:10.1145/3519935.3520063.
  • [15] Samuel R. Buss and Toniann Pitassi. Good degree bounds on Nullstellensatz refutations of the induction principle. J. Comput. Syst. Sci., 57(2):162–171, 1998. doi:10.1006/JCSS.1998.1585.
  • [16] Hubie Chen. A rendezvous of logic, complexity, and algebra. ACM Comput. Surv., 42(1):2:1–2:32, December 2009. doi:10.1145/1592451.1592453.
  • [17] Matthew Clegg, Jeff Edmonds, and Russell Impagliazzo. Using the Groebner basis algorithm to find proofs of unsatisfiability. In Proceedings of the Twenty-Eighth Annual ACM Symposium on the Theory of Computing, 1996, pages 174–183, 1996. doi:10.1145/237814.237860.
  • [18] David A. Cox, John Little, and Donal O’Shea. Ideals, Varieties, and Algorithms: An Introduction to Computational Algebraic Geometry and Commutative Algebra. Springer Publishing Company, Incorporated, 4th edition, 2015.
  • [19] B. A. Davey and H. A. Priestley. Introduction to Lattices and Order. Cambridge University Press, 2 edition, 2002.
  • [20] Noah Fleming, Pravesh Kothari, and Toniann Pitassi. Semialgebraic proofs and efficient algorithm design. Foundations and Trends in Theoretical Computer Science, 14(1-2):1–221, 2019. doi:10.1561/0400000086.
  • [21] Michel X. Goemans and David P. Williamson. Improved approximation algorithms for maximum cut and satisfiability problems using semidefinite programming. J. ACM, 42(6):1115–1145, November 1995. doi:10.1145/227683.227684.
  • [22] Sander Gribling, Sven Polak, and Lucas Slot. A note on the computational complexity of the moment-sos hierarchy for polynomial optimization. In Proceedings of the 2023 International Symposium on Symbolic and Algebraic Computation, ISSAC ’23, pages 280–288, New York, NY, USA, 2023. Association for Computing Machinery. doi:10.1145/3597066.3597075.
  • [23] Dima Grigoriev. Linear lower bound on degrees of positivstellensatz calculus proofs for the parity. Theoretical Computer Science, 259(1):613–622, 2001. doi:10.1016/S0304-3975(00)00157-2.
  • [24] Dima Grigoriev, Edward A. Hirsch, and Dmitrii V. Pasechnik. Complexity of semialgebraic proofs. Moscow Mathematical Journal, 2(4):647–679, 2002.
  • [25] Dima Grigoriev and Nicolai N. Vorobjov Jr. Complexity of null-and positivstellensatz proofs. Ann. Pure Appl. Log., 113(1-3):153–160, 2001. doi:10.1016/S0168-0072(01)00055-0.
  • [26] Tuomas Hakoniemi. Monomial size vs. bit-complexity in sums-of-squares and polynomial calculus. In 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021, Rome, Italy, June 29 - July 2, 2021, pages 1–7. IEEE, 2021. doi:10.1109/LICS52264.2021.9470545.
  • [27] David Hilbert. Ueber die vollen invariantensysteme. Mathematische Annalen, 42:313–373, 1893. URL: http://eudml.org/doc/157652.
  • [28] Peter G. Jeavons and Martin C. Cooper. Tractable constraints on ordered domains. Artificial Intelligence, 79(2):327–339, 1995. doi:10.1016/0004-3702(95)00107-7.
  • [29] Christopher Jefferson, Peter Jeavons, Martin J. Green, and M. R. C. van Dongen. Representing and solving finite-domain constraint problems using systems of polynomials. Annals of Mathematics and Artificial Intelligence, 67(3):359–382, March 2013. doi:10.1007/s10472-013-9365-7.
  • [30] Cédric Josz and Didier Henrion. Strong duality in lasserre’s hierarchy for polynomial optimization. Optimization Letters, 10(1):3–10, January 2016. doi:10.1007/S11590-015-0868-5.
  • [31] Adam Kurpisz, Samuli Leppänen, and Monaldo Mastrolilli. On the hardest problem formulations for the 0/1 lasserre hierarchy. Math. Oper. Res., 42(1):135–143, 2017. doi:10.1287/MOOR.2016.0797.
  • [32] Adam Kurpisz, Samuli Leppänen, and Monaldo Mastrolilli. An unbounded sum-of-squares hierarchy integrality gap for a polynomially solvable problem. Math. Program., 166(1–2):1–17, November 2017. doi:10.1007/s10107-016-1102-7.
  • [33] Adam Kurpisz, Samuli Leppänen, and Monaldo Mastrolilli. Tight sum-of-squares lower bounds for binary polynomial optimization problems. ACM Trans. Comput. Theory, 16(1), March 2024. doi:10.1145/3626106.
  • [34] Adam Kurpisz, Samuli Leppänen, and Monaldo Mastrolilli. Sum-of-squares hierarchy lower bounds for symmetric formulations. Mathematical Programming, 182(1-2):369–397, 2020. Cited by: 4. doi:10.1007/s10107-019-01398-9.
  • [35] Jean B. Lasserre. An explicit exact sdp relaxation for nonlinear 0-1 programs. In Karen Aardal and Bert Gerards, editors, Integer Programming and Combinatorial Optimization, pages 293–303, Berlin, Heidelberg, 2001. Springer Berlin Heidelberg. doi:10.1007/3-540-45535-3_23.
  • [36] Monique Laurent. Sums of Squares, Moment Matrices and Optimization Over Polynomials, pages 157–270. Springer New York, New York, NY, 2009. doi:10.1007/978-0-387-09686-5_7.
  • [37] Monaldo Mastrolilli. High degree sum of squares proofs, Bienstock-Zuckerberg hierarchy, and Chvátal-Gomory cuts. SIAM J. Optim., 30(1):798–822, 2020. doi:10.1137/17M1150712.
  • [38] Monaldo Mastrolilli. The complexity of the ideal membership problem for constrained problems over the boolean domain. ACM Trans. Algorithms, 17(4):32:1–32:29, 2021. doi:10.1145/3449350.
  • [39] Ernst W. Mayr. Membership in polynomial ideals over q is exponential space complete. In B. Monien and R. Cori, editors, STACS 89, pages 400–406, Berlin, Heidelberg, 1989. Springer Berlin Heidelberg. doi:10.1007/BFB0029002.
  • [40] Ernst W. Mayr and Albert R. Meyer. The complexity of the word problems for commutative semigroups and polynomial ideals. Advances in Mathematics, 46(3):305–329, 1982. doi:10.1016/0001-8708(82)90048-2.
  • [41] Ryan O’Donnell. SOS Is Not Obviously Automatizable, Even Approximately. In Christos H. Papadimitriou, editor, 8th Innovations in Theoretical Computer Science Conference (ITCS 2017), volume 67 of Leibniz International Proceedings in Informatics (LIPIcs), pages 59:1–59:10, Dagstuhl, Germany, 2017. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. doi:10.4230/LIPIcs.ITCS.2017.59.
  • [42] Marilena Palomba, Lucas Slot, Luis Felipe Vargas, and Monaldo Mastrolilli. Computational complexity of sum-of-squares bounds for copositive programs, 2025. doi:10.48550/arXiv.2501.03698.
  • [43] Dona Papert. Congruence Relations in Semi-Lattices. Journal of the London Mathematical Society, s1-39(1):723–729, January 1964. doi:10.1112/jlms/s1-39.1.723.
  • [44] Pablo A. Parrilo. Semidefinite programming relaxations for semialgebraic problems. Mathematical Programming, 96(2):293–320, 2003. doi:10.1007/s10107-003-0387-5.
  • [45] Fedor Part, Neil Thapen, and Iddo Tzameret. First-order reasoning and efficient semi-algebraic proofs. In 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1–13, 2021. doi:10.1109/LICS52264.2021.9470546.
  • [46] Gábor Pataki and Aleksandr Touzov. How do exponential size solutions arise in semidefinite programming? SIAM Journal on Optimization, 34(1):977–1005, 2024. doi:10.1137/21M1434945.
  • [47] Aaron Potechin. Sum of Squares Lower Bounds from Symmetry and a Good Story. In Avrim Blum, editor, 10th Innovations in Theoretical Computer Science Conference (ITCS 2019), volume 124 of Leibniz International Proceedings in Informatics (LIPIcs), pages 61:1–61:20, Dagstuhl, Germany, 2019. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. doi:10.4230/LIPIcs.ITCS.2019.61.
  • [48] Prasad Raghavendra and Benjamin Weitz. On the Bit Complexity of Sum-of-Squares Proofs. In Ioannis Chatzigiannakis, Piotr Indyk, Fabian Kuhn, and Anca Muscholl, editors, 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017), volume 80 of Leibniz International Proceedings in Informatics (LIPIcs), pages 80:1–80:13, Dagstuhl, Germany, 2017. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. doi:10.4230/LIPIcs.ICALP.2017.80.
  • [49] Prasad Raghavendra and Benjamin Weitz. On the bit complexity of sum-of-squares proofs. In 44th International Colloquium on Automata, Languages, and Programming, ICALP, Poland, pages 80:1–80:13, 2017. doi:10.4230/LIPICS.ICALP.2017.80.
  • [50] Dmitry Sokolov. (Semi)algebraic proofs over ±1 variables. In Konstantin Makarychev, Yury Makarychev, Madhur Tulsiani, Gautam Kamath, and Julia Chuzhoy, editors, Proccedings of the 52nd Annual ACM SIGACT Symposium on Theory of Computing, STOC 2020, Chicago, IL, USA, June 22-26, 2020, pages 78–90. ACM, 2020. doi:10.1145/3357713.3384288.
  • [51] Johan Thapper and Stanislav Živnỳ. The limits of sdp relaxations for general-valued csps. ACM Transactions on Computation Theory (TOCT), 10(3):1–22, 2018. doi:10.1145/3201777.
  • [52] Benjamin Weitz. Polynomial Proof Systems, Effective Derivations, and their Applications in the Sum-of-Squares Hierarchy. PhD thesis, EECS Department, University of California, Berkeley, May 2017.
  • [53] Dmitriy Zhuk. A proof of CSP dichotomy conjecture (best paper award). In 58th IEEE Annual Symposium on Foundations of Computer Science, FOCS 2017, Berkeley, CA, USA, October 15-17, 2017, pages 331–342, 2017. doi:10.1109/FOCS.2017.38.
  • [54] Dmitriy Zhuk. A proof of the CSP dichotomy conjecture. J. ACM, 67(5):30:1–30:78, 2020. doi:10.1145/3402029.