An Algebraic Approach to MaxCSP

The Constraint Satisfaction Problem (CSP) is the problem of, given a set of constraints on variables, finding an assignment satisfying all of them. $\mathrm{SAT}$ can be seen as the restriction of this problem to Boolean, ​i.e., $0/1$-valued, variables and constraints given as clauses. MaxCSP and $\mathrm{MaxSAT}$ are their respective optimization versions, where we find assignments maximizing the number of satisfied restrictions. CSP could be tackled via translations to $\mathrm{SAT}$, see for instance, [21]. MaxCSP could be tackled via translations to $\mathrm{MaxSAT}$, but this kind of reduction is more subtle since we have to preserve not only satisfiability, but also the number of violated constraints. As a result, in some problems, it may be more efficient to try to solve the original problem using CSP techniques directly, instead of these translations.

In this paper, we consider the natural adaptation of the notions of MaxCSP and $\mathrm{MaxSAT}$ to sets of polynomials and we show how to use an algebraic framework to tackle optimization problems on sets of polynomials over multi-valued variables. Sets of polynomials over many-valued variables can be used to encode CSP and MaxCSP more directly, avoiding the translation to $\mathrm{SAT}$.

Given a set of polynomials $P$, we want to determine the maximum number of polynomials in $P$ that can be simultaneously evaluated to zero under a common assignment of the variables. Unlike $\mathrm{SAT}$ and $\mathrm{MaxSAT}$ that rely on Boolean encodings, using sets of polynomials allows to use a direct multi-valued encoding of MaxCSP problems that are more expressive, concise, and closer in nature to possible underlying algebraic properties of the original problem at hand.

The algebraic framework we use is an adaptation of Polynomial Calculus ($\mathrm{PC}$) introduced in [9]. $\mathrm{PC}$ is the proof system underlying the reasoning power of algorithms to compute Gröbner bases [7, 6, 12], and, from a theoretical point of view, $\mathrm{PC}$ is well-studied in connection with big open questions in Complexity Theory. From a practical point of view, the interest in $\mathrm{PC}$ stems from the fact that it is stronger and more versatile than Resolution, the proof system underlying the Conflict-Driven-Clause-Learning paradigm of state-of-the-art $\mathrm{SAT}$-solvers [20, 1]. Moreover, algorithms computing Gröbner bases are useful in practice in the context of coloring of graphs [18, 10, 11] and verification of multiplier circuits [16, 14, 15, 13]. The previous applications use polynomials over multi-valued or Fourier encoding, ​i.e., using variables such that $x^{\kappa }=1$. Unlike the case of $\mathrm{PC}$ over Boolean variables, $\mathrm{PC}$ over multi-valued variables is not so well understood. Some well-known principles, such as Tseitin formulas have short (polynomial size) proofs in $\mathrm{PC}$ over $\pm 1$-variables, while they do not have short proofs over $\mathrm{PC}$ with Boolean variables. Recently, it has also been shown that there are unsatisfiable formulas having polynomial size refutation in $\mathrm{PC}$ over Boolean variables, while requiring exponential size in $\mathrm{PC}$ over $\pm 1$-valued [19].

Recently, Bonacina, Bonet and Levy [2, 3] introduced an algebraic calculus (${\mathrm{wPC}}_{\kappa }$) for certifying the optimum value in optimization problems on polynomials over the finite field ${𝔽}_{\kappa }$. This is a generalization of $\mathrm{PC}$ to the context of optimization and not only satisfiability. The authors proved the completeness of the calculus in the case of polynomials over Boolean variables.

In this work, we consider polynomials over non-Boolean encodings and therefore we give a theoretical ground for extending the applicability of the algorithms using algebraic reasoning and many-valued variables from the context of CSPs to MaxCSPs. For the sake of clarity, we omit the possible generalization to the case of weights and the presence of hard constraints, for instance coming from a Fourier encoding (i.e. using polynomials $x^{\mathrm{\ell }}-1$ to limit the possible values taken), although all the content of this paper will adapt easily to those cases.

The main contribution of this work is the completeness of the calculus ${\mathrm{wPC}}_{\kappa }$ over arbitrary sets of polynomials in ${𝔽}_{\kappa }$ (Theorem 5.1). This argument loosely follows the structure of the completeness of ${\mathrm{wPC}}_{\kappa }$ over polynomials forced to take Boolean values in [3] but requires several non-trivial adaptations. This gives an algorithmic procedure that is efficient in some cases, see Section 6.

As a proof of concept, we also show how to apply the calculus ${\mathrm{wPC}}_3$ to certify Max-$3$-colorability of graphs exploiting the use of non-Boolean variables (see Section 4).

For a natural number $n\in \mathbb{N}$, let $[n]=\{1,\mathrm{\dots },n\}$. Capital letters typically denote sets and multi-sets, for instance, $X$ usually denotes a set of variables. With $p,q,f$ we typically denote polynomials. $\kappa$ will always denote the number of elements of a generic finite field.

Bonacina, Bonet and Levy in [3] introduced Polynomial Calculus for $\mathrm{MaxSAT}$ (${\mathrm{wPC}}_{\kappa }$) as a way to use a system stronger than MaxSAT-Resolution to solve $\mathrm{MaxSAT}$. For simplicity, we omit the treatment of weighted polynomials and sets of polynomials as “hard” constraints. We also omit the case of negative weights and therefore what we call ${\mathrm{wPC}}_{\kappa }$ is ${\mathrm{𝗐𝖯𝖢}}_{\mathbb{N},{𝔽}_{\kappa }}$ in [3].

The system ${\mathrm{wPC}}_{\kappa }$ can be used to certify that for a multi-set of polynomials $P\subset {𝔽}_{\kappa }[X]$, $\mathrm{cost}(P)⩾s$. Indeed, a ${\mathrm{wPC}}_{\kappa }$ derivation from $P$ of $s$ copies of the constant polynomial $1$ implies that $\mathrm{cost}(P)⩾s$. Or, equivalently, a ${\mathrm{wPC}}_{\kappa }$ derivation of $s$ non-zero constant polynomials, since by the prod rule from any non-zero constant we can derive the polynomial $1$ multiplying by its inverse (for an example of application, see last inference step in Example 3.3). In ${\mathrm{wPC}}_{\kappa }$ it is also possible to certify that $\mathrm{cost}(P)=s$: if on top of the $s$-many polynomials identically $1$ we give an assignment which is a common zero of the polynomials obtained alongside the $1$s.

To clarify the rules for ${\mathrm{wPC}}_{\kappa }$, we give an equivalent, but more explicit, set of rules for $\kappa =3$:

where $p,q\in {𝔽}_3[X]$. The rule prod in (3) is strongly sound essentially because for any assignment $\alpha$ exactly one among $q(\alpha )$ and $q{(\alpha )}^2-1$ is zero. The rule sum in (3) is strongly sound by case analysis: the less trivial case to check is when we have an assignment $\alpha$ such that $\mathrm{cost}(\{p,q\},\alpha )=2$, i.e. $p(\alpha )\in \{1,-1\}$ and $q(\alpha )\in \{1,-1\}$. In this case, the cost of the conclusions of the rule is also $2$ because $p(\alpha )q(\alpha )\ne 0$ and, over the assignments $\alpha$s we are considering, exactly one among $p(\alpha )+q(\alpha )$ and $q(\alpha )-p(\alpha )$ is zero.

To illustrate the calculus ${\mathrm{wPC}}_3$ and the use of the rules from (3) and (1) we give a couple of examples.

Bonacina, Bonet and Levy in [3] proved that the rules in (2) are strongly sound. This is just a case analysis on the values of $p(\alpha )$, $q(\alpha )$ on an assignment $\alpha$ and uses the fact that $p(\alpha )+q(\alpha )\ne 0$ if and only if ${(p(\alpha )+q(\alpha ))}^{\kappa -1}=1$. As a consequence, the system ${\mathrm{wPC}}_{\kappa }$ is sound.

A converse of Theorem 3.6 (i.e., that the calculus ${\mathrm{wPC}}_{\kappa }$ is also complete) is also true, under the additional assumption that the initial polynomials $P$ are on Boolean $0/1$-valued variables [3].

In Section 5 (Theorem 5.1), we complete and extend the completeness result in [3] showing a converse of Theorem 3.6 for an arbitrary $\kappa$ without any additional assumption. Therefore allowing the use of ${\mathrm{wPC}}_{\kappa }$ beyond multi-sets of polynomials over Boolean variables. As Example 3.5 shows, using Boolean or multi-valued variables might result in completely different complexities of the problem at hand.

A calculus for optimization on polynomials on arbitrary variables allows using direct encoding of MaxCSPs. Moreover, the algebraic language offers the possibility to concisely encode many natural constraints used in CSP.

One notable example is the Vertex Coloring Problem (VCP), which we analyze in detail in this section. Given an undirected graph $G=(V,E)$, the Vertex Coloring Problem (VCP) is the problem of finding a labeling of the vertices of $G$ such that no vertices along an edge share the same label. Deciding if a given graph is $3$-colorable, i.e. colorable with a set of $3$ labels, is one of the classical $\mathrm{NP}$-complete problems.

Max-$3$-Coloring, the problem of maximizing the number of edges that connect $3$-colored vertexes with distinct labels, is a more difficult problem. Max-$2$-Coloring is exactly MaxCUT, which is $\mathrm{NP}$-complete, whereas $2$-Coloring is in $\mathrm{P}$.

To show that a given graph $G$ is not say $3$-colorable we can associate to the VCP on $G$ a CNF formula which is satisfiable iff $G$ is $3$-colorable. Alternatively, we can associate the VCP on $G$ to a set of polynomials with a common solution iff $G$ is $3$-colorable. To encode the VCP algebraically, we need to express restrictions of the form $x\ne y$. There are several ways of doing this. Using polynomials with coefficients in ${𝔽}_3$, it can be encoded as $x^2+xy+y^2-1$. This polynomial evaluates to zero when $x\ne y$.

This immediately generalizes to expressing the nogood $⟨v_1,\mathrm{\dots },v_{\mathrm{\ell }}⟩$ for variables $⟨x_1,\mathrm{\dots },x_{\mathrm{\ell }}⟩$, i.e. the fact that at least for one index $i$, $x_i\ne v_i$. This can be done using the polynomial ${\prod }_{i=1}^{\mathrm{\ell }}(x_i^2+v_i{x}_i+v_i^2-1)$ which evaluates to zero exactly when there is an index $i$ such that $x_i\ne v_i$.

Alternatively, for instance, the constraint $x\ne y$ for $3$-coloring can be encoded using Fourier variables in ${𝔽}_4$ as $\{x^3-1,y^3-1,x^2+xy+y^2-1\}$, where the first two polynomials are hard constraints and the third one is a soft constraint. Both the encoding in ${𝔽}_3$ and the encoding in ${𝔽}_4$ with Fourier variables generalize easily to $\mathrm{\ell }$-coloring. In this work, for simplicity, we only consider the encoding with variables in ${𝔽}_3$.

In this section, we prove the converse of Theorem 3.6.

The proof of Theorem 5.1 follows the structure of [3, Theorem 4.1] which was ultimately inspired by [5]. Informally, the argument goes by the following algorithmic procedure. Take an ordering on the variables $X=\{x_1,\mathrm{\dots },x_n\}$, then on the polynomials depending on $x_1$ try to infer as many non-trivial polynomials without $x_1$ as possible using the sum and prod rules. This would be, intuitively, the notion of saturation (Definition 5.6). Then repeat the process one variable at a time. At the end of the process, we will have obtained $s$-many copies of the polynomial $1$ together with several other polynomials. The process will have preserved the $\mathrm{cost}$ along the way, while the remaining polynomials are satisfiable, by the structural properties of the saturation. To make this very high-level structure of the argument formal, first, we need to formalize the notion of when a polynomial depends on a variable $x$.

For instance, the polynomial $x^3-x-1\in {𝔽}_3[x]$ does not depend on $x$, since $x^3-x-1\equiv -1$ over ${𝔽}_3$.

The following proposition gives an equivalent characterization for when a polynomial does not depend on a variable.

For $p\in {𝔽}_{\kappa }[X]$, we use the notation $p_{x\mapsto a}$, where $x\in X$, to denote the polynomial $p$ where each occurrence of $x$ has been substituted with $a\in {𝔽}_{\kappa }$, and we use the notation

In particular, for $p\in {𝔽}_3[X]$ and $x\in X$,