On Solving MAX-SAT Using Sum of Squares

1. Introduction

In this paper, we investigate semidefinite programming (SDP) approaches for the satisfiability (SAT) problem, maximum satisfiability (MAX-SAT) problem, and their variants. Given a logical proposition built from a conjunction of clauses, SAT asks whether there exists a truth assignment to the variables such that all clauses are satisfied. The optimization variant of SAT, known as MAX-SAT, is to determine a truth assignment that satisfies the largest number of clauses.

SAT is a central problem in mathematical logic and computer science and finds various applications, including software or hardware verification (Marques-Silva and Sakallah 2000) and planning in artificial intelligence (Kautz and Selman 1999). Cook (1971) proves that SAT is $\mathcal{N}\mathcal{P}$-complete. SAT is the first problem proven to be $\mathcal{N}\mathcal{P}$-complete, which implies that any problem contained in the complexity class $\mathcal{N}\mathcal{P}$ can be efficiently recast as a SAT instance. Thus, algorithms for SAT can also solve a wide variety of other problems, such as timetabling (Asín Achá and Nieuwenhuis 2014, Gattermann et al. 2016) and product line engineering (Mendonca et al. 2009).

SDP approaches to SAT are proposed first by de Klerk et al. (2000) and later extended by Anjos (2004a, b; 2005; 2006; 2007). Goemans and Williamson (1995) are first to apply SDP to MAX-SAT. They show that, for a specific class of MAX-SAT instances known as MAX-2-SAT (in MAX-k-SAT, each clause is a disjunction of at most k variables), MAX-SAT is equivalent to optimizing a multivariate quadratic polynomial, which is naturally well-suited for semidefinite relaxations. In the same paper, Goemans and Williamson (1995) propose a 0.878-approximation algorithm for MAX-2-SAT based on SDP. This result is later improved to 0.940 in Lewin et al. (2002). Further, Karloff and Zwick (1997) obtain an optimal 7/8 approximation algorithm for MAX-3-SAT, and Halperin and Zwick (2001) obtain a nearly optimal approximation algorithm for MAX-4-SAT. In van Maaren et al. (2008), the authors exploit sum of squares (SOS) optimization to compute bounds for MAX-SAT.

Despite the great success in designing approximation algorithms using SDP, most modern MAX-SAT solvers do not exploit SDP. A possible reason for this is the fact that medium- to large-size SDP problems are computationally challenging to solve. Interior point methods, the conventional approach for solving SDPs, struggle from large memory requirements and prohibitive computation time per iteration already for medium-size SDPs. Recently, first order methods, such as the alternating direction method of multipliers (Gabay and Mercier 1976, Boyd et al. 2011) and the Peaceman–Rachford splitting method (PRSM) (Peaceman and Rachford 1955) show a great success in solving SDPs (see, e.g., Oliveira et al. 2018, de Meijer and Sotirov 2021, Graham et al. 2022). Motivated by these results, we design a MAX-SAT solver that incorporates SDP bounds and the PRSM within a branch-and-bound (B&B) scheme.

In particular, we further exploit the SOS approach from van Maaren et al. (2008) to derive SOS-based SDP relaxations that provide strong upper bounds to the optimal MAX-SAT solution. The derived SDP relaxations are strengthened SDP duals of the Goemans and Williamson (1995) MAX-SAT relaxation. The strength of the upper bounds and the required time to compute the relaxations depend on the chosen monomial basis. We experiment with different monomial bases and propose a class of bases that provide good trade-offs between these effects. Moreover, we derive several properties of monomial bases that are exploited in the design of our solver. We extend the SOS approach to weighted partial MAX-SAT, a variant of MAX-SAT in which clauses are divided into soft and hard clauses. Here, the goal is to maximize the weighted sum of soft clauses, satisfying all the hard clauses. We strengthen SDP bounds for weighted partial MAX-SAT using the SAT resolution rule. To the best of our knowledge, we are the first to exploit SDP for solving weighted partial MAX-SAT.

We show that the Peaceman–Rachford splitting method is well-suited for exploiting the structure of the SOS-based SDP relaxations. Therefore, we implement the PRSM to (approximately) solve large-scale SDP relaxations and obtain upper bounds for the (weighted partial) MAX-SAT. The resulting algorithm is very efficient; for example, it can compute upper bounds with matrix variables of order 1,800 in less than two minutes and for matrices of order 2,400 in less than four minutes. Our numerical results show that the upper bounds are strong, in particular, when larger monomial bases are used. We also exploit the output of the PRSM to efficiently compute lower bounds for the MAX-SAT problem.

We design an SOS-SDP–based MAX-SAT solver (named SOS-MS) that exploits SOS-based SDP relaxations and the PRSM. SOS-MS is one of the first SDP-based MAX-SAT solvers. The only alternative SDP-based solver is the MIXSAT algorithm (Wang and Zico Kolter 2019) that is designed to solve MAX-2-SAT instances. SOS-MS is able to solve (weighted partial) MAX-k-SAT instances for $k\le 3$. To solve a MAX-SAT instance, SOS-MS has to approximately solve multiple SDP subproblems. A crucial component of SOS-MS is, therefore, its ability to quickly construct the program parameters of the required SDPs, that is, the process of parsing. We design an efficient parsing method, which is also applicable to other problems and publicly available. Another efficient feature of our solver is warm starts. Namely, our solver uses the approximate PRSM solution at a node as warm starts for the corresponding children’s node. We are able to solve a variety of MAX-SAT instances in a reasonable time, solving some instances faster than the best solvers in the 11th Evaluation of Max-SAT Solvers (MSE-2016). Moreover, we solve three previously unsolved MAX-3-SAT instances from the MSE-2016. To our knowledge, we are first to use SDP for solving weighted partial MAX-SAT. Our results provide new perspectives on solving MAX-SAT and all its variants by using SDPs.

Our paper provides various theoretical results. We propose a family of semidefinite feasibility problems and show that one member of this family provides the rank-two guarantee. That is, whenever the semidefinite relaxation admits a feasible matrix of rank two or less, the underlying SAT instance is satisfiable. This result relates to a similar rank-two guarantee result by Anjos (2004a). The rank value can be seen as a measure of the strength of the relaxation. We also provide a parametric family of semidefinite relaxations for the (weighted partial) MAX-SAT. This parameter can be finely tuned to determine the strength of the relaxation, and any such relaxation can easily be incorporated within SOS-MS. This allows the solver to be adapted per (class of) problem instances.

Further, we show how the SOS approach to MAX-SAT of van Maaren et al. (2008) and the, here generalized, moment relaxations of SAT from Anjos (2004a, b; 2005; 2006; 2007) are related. This is done by exploiting the duality theory of the moment and SOS approaches. Our result generalizes a result by van Maaren et al. (2008), who show the connection between the two approaches only for restricted cases. By exploiting duality theory, we also relate the SOS relaxations for the partial MAX-SAT problem to SAT relaxations from Anjos (2004a).

Finally, we investigate MAX-SAT resolution, a powerful technique used by many MAX-SAT solvers (Abramé and Habet 2014) in relation to the SDP approach to MAX-SAT. Standard MAX-SAT solvers use resolution to determine upper bounds on the MAX-SAT solution, whereas SOS-MS determines upper bounds through SDP. We show how resolution is related to the monomial basis. We also show how SAT resolution can be exploited for weighted partial MAX-SAT.

This paper is organized as follows. We provide notation and preliminaries in Section 1.1 and assumptions in Section 1.2. Section 2 provides an overview of the Goemans and Williamson (1995) approach to MAX-SAT. Section 3 first outlines previous SDP approaches to SAT and then generalizes them. Section 4 provides the details of the SOS theory applied to MAX-SAT. We also derive various properties of monomial bases in that section. Section 5 concerns the combination of MAX-SAT resolution and SOS. In Section 6, we show how two SDP approaches to (MAX-)SAT (i.e., Anjos 2004a, van Maaren et al. 2008) are connected. Section 7 introduces the PRSM for SOS.¹ We extend the SOS approach to weighted partial MAX-SAT and connect the resulting program to the relaxations in Anjos (2004a) in Section 8. Online Appendix E provides an overview and pseudocode of our solver SOS-MS. Online Appendix F presents numerical results that include SOS-SDP bounds and performance of SOS-MS. Concluding remarks are given in Section 9.

1.1. Preliminaries and Notation

For any $n\in \mathbb{N}$, we write $[n]=\{1,\dots ,n\}$. We denote by $\varphi$ a propositional formula, in variables x₁ up to x_n and assume that $\varphi$ is in conjunctive normal form (CNF). That is, $\varphi$ is given by a conjunction of m clauses,

We mostly use n to refer to the number of variables and m to refer to the number of clauses. Each clause C_j is a disjunction of (possibly negated) variables. We define each clause C_j as a subset of $[n]$, indicating the variables appearing in C_j. Moreover, we define $I_j^{+}\subseteq C_j$ as the set of unnegated variables appearing in C_j. Similarly, $I_j^{-}\subseteq C_j$ is defined as the set of negated variables appearing in C_j. Thus, the clause associated with C_j reads

We refer to both x_i and $\neg x_i$ as literals. For example, the literal $\neg x_i$ is true if x_i is false. We denote the length of a clause by ${\mathcal{\ell }}_j$; thus, ${\mathcal{\ell }}_j≔|C_j|$. We say that $\varphi$ constitutes a (MAX-)k-SAT instance if ${\text{max}}_{j\in [m]}{\mathcal{\ell }}_j=k$.

The SAT problem is to decide, given $\varphi$, whether a satisfying truth assignment to the variables x_i, $i\in [n]$ exists. The MAX-SAT problem is to find an assignment that satisfies the largest number of clauses. We associate to each clause a vector $a_j\in {\{0,\pm 1\}}^n$, having entries $a_{j,i}$ according to

We write ${\mathcal{S}}^n$ for the set of symmetric n × n matrices and ${\mathcal{S}}_{+}^n$ for the cone of symmetric positive semidefinite matrices of size n × n. If the context is clear, the superscript n is omitted. We denote by ${\mathbf{1}}_n\in {\mathbb{R}}^n$ and ${\mathbf{0}}_n\in {\mathbb{R}}^n$ vectors of all ones and zeroes, respectively (subscripts are omitted when the context is clear). The identity matrix of order n is written as I_n. Matrix ${\mathbf{0}}_{m\times n}$ denotes the zero matrix of m rows and n columns. For $X,Y\in \mathcal{S}$, we define the trace inner product as $〈X,Y〉≔\text{Tr}(XY)$. We write $X⪰Y$ if and only if $X-Y\in {\mathcal{S}}_{+}$. The Frobenius norm of a symmetric matrix X is given by ${\Vert X\Vert }_F=\sqrt{〈X,X〉}$. For $X\in \mathcal{S}$ and $\mathcal{M}\subseteq \mathcal{S}$, we set

as the projection of X onto $\mathcal{M}$. For $X\in {\mathbb{R}}^{n\times n}$, diag$(X)\in {\mathbb{R}}^n$ denotes the vector equal to the diagonal of X. For $x\in {\mathbb{R}}^n$, we write $\Vert x\Vert ≔\sqrt{x^{\top }x}$ andfor some $\alpha \subseteq [n]$. We evaluate the empty product as one. Note that (5) differs from the more common notation in SOS literature, in which the α are considered as vectors in ${\mathbb{N}}^n$; see, for example, Lasserre (2007).

1.2. Assumptions

In the rest of this work, we assume that all logical propositions $\varphi$ on n variables and m clauses satisfy the following three properties:

1. For all $j\in [m],\hspace{0.17em}|C_j|\ge 2$.

2. For all $j\in [m],\hspace{0.17em}{I}_j^{+}\cap I_j^{-}=\varnothing$.

3. Each variable is contained in at least two clauses along with $\varphi$ being in CNF.

Property 1 can be assumed for SAT instances. If a SAT instance contains a clause C_j with $|C_j|=1$ (such a clause is known as a unit clause), the literal in C_j must be satisfied. The variable corresponding to this literal can, thus, be given an appropriate truth value, and $\varphi$ can be reduced (such a reduction of $\varphi$ is referred to as unit resolution). For MAX-SAT instances, it is possible that an optimal truth assignment might leave unit clauses unsatisfied. We note, however, that the MAX-SAT benchmark instances we consider satisfy all these assumptions.

In Online Appendix B, we show that properties 2 and 3 can be assumed without loss of generality (w.l.o.g.).

2. MAX-SAT Formulation and Relaxation

We outline the approach of Goemans and Williamson (1995) for formulating MAX-SAT as a polynomial optimization problem. We also present their SDP relaxation for MAX-2-SAT.

Let $x_1,\hspace{0.17em}{x}_2,\hspace{0.17em}\dots ,x_n$ be the variables of the MAX-SAT instance given by a logical proposition $\varphi$. We, thus, assume that $\varphi$ is given in conjunctive normal form, see (1), and contains m clauses. As customary in the SDP SAT literature, we associate +1 with true and –1 with false. An assignment of the x_i values in $\{\pm 1\}$ is referred to as a truth assignment. As proposed by Goemans and Williamson (1995), we define a truth function $v:{\{\pm 1\}}^n\to \{0,1\}$ such that, given a logical proposition $\varphi \prime$ evaluated for some truth assignment, $v(\varphi \prime )=1$ if and only if $\varphi \prime$ is satisfied and zero otherwise. This property uniquely determines v; that is, $v(x_i)=\frac{1+x_i}{2}\hspace{0.17em}\text{and}\hspace{0.17em}v(\neg x_i)=\frac{1-x_i}{2}.$ And, in general, for a clause $C_j\subseteq [n]$ of length ${\mathcal{\ell }}_j$, we have

for a_j as in (3) and both $a_j^{\gamma }$ and $x^{\gamma }$ as in (5). The last equality in (6) follows from the product expansion of $v(C_j)$ as shown in proposition 1 in Anjos (2006). In Goemans and Williamson (1995), an extra variable $x_0\in \{\pm 1\}$ is defined with the purpose of deciding the truth value; that is, $\varphi \prime$ is true if and only if $v(\varphi \prime )=x_0$. We set $x_0=1$ without loss of generality for sake of clarity. The MAX-SAT problem given by $\varphi$ is to maximize the following polynomial:subject to $x_i\in \{\pm 1\}$ for all i and for appropriate $v_{\varphi }^{\alpha }\in \mathbb{R}$ and $x^{\alpha }$ as in (5). Observe that $v_{\varphi }$ is a kth degree polynomial if $\varphi$ represents a MAX-k-SAT instance. A MAX-2-SAT instance, thus, corresponds to a quadratic polynomial and is, therefore, well-suited for approximation by SDP. We return to $v_{\varphi }$ in Section 6.

Assuming now that $\varphi$ represents a MAX-2-SAT instance on n variables, the corresponding MAX-2-SAT can be formulated as

where $〈W,X〉$ describes the quadratic polynomial $v_{\varphi }$. Observe that the constraints of (8) enforce X to satisfy $X=x{x}^{\top }$ for some $x\in {\{\pm 1\}}^{n+1}$. The size of this vector x is one more than the number of variables n to account for the additional truth value variable x₀.

A semidefinite relaxation of (8) is obtained by omitting the integrality constraint or, equivalently, nonconvex rank-one constraint. This constitutes the well-known Goemans and Williamson (1995) SDP relaxation of MAX-2-SAT. That is,

Goemans and Williamson (1995) show that the optimal matrix for (9) can be used to obtain a 0.878-approximation algorithm to MAX-2-SAT. Assuming $\mathcal{P}\ne \mathcal{N}\mathcal{P}$, for any $\epsilon >0$ there exists no $(\frac{21}{22}+\epsilon )$ approximation algorithm to MAX-2-SAT (Håstad 2001). Karloff and Zwick (1997) introduce a canonical way of obtaining SDP relaxations for any MAX-SAT that is exploited to obtain approximation algorithms to MAX-3-SAT and MAX-4-SAT in Karloff and Zwick (1997) and Halperin and Zwick (2001), respectively. To solve MAX-2-SAT instances, rather than approximate, Wang and Zico Kolter (2019) propose the MIXSAT algorithm, which combines (9) with a B&B scheme.

3. SAT as a Semidefinite Feasibility Problem

In this section, we first present a brief overview of the work done by de Klerk et al. (2000) and Anjos (2004a, b; 2005; 2006; 2007). Their relaxations of SAT involve semidefinite feasibility problems: infeasibility of the semidefinite program implies unsatisfiability of the corresponding SAT instance. The difference between relaxations is the size of the SDP variable and the method of encoding the structure of the SAT instance in the SDP relaxation. Then, we propose a family of semidefinite feasibility problems that contains relaxations from Anjos (2004a, b; 2005; 2006; 2007) and de Klerk et al. (2000) as special cases and show that a particular member of the family provides a rank-two guarantee; see Theorem 1.

We reconsider first Program (9), which attempts to satisfy the maximum number of clauses through its objective function. For SAT specifically, one might move the clause satisfaction part from the objective to the feasible set of a semidefinite program. This idea is first proposed by de Klerk et al. (2000) and later extended by Anjos (2004a). To be precise: de Klerk et al. (2000) propose the so-called GAP relaxation, or GAP for short, which is a semidefinite feasibility problem, given by

for a_j as in (3). It is noted in de Klerk et al. (2000) that, for ${\mathcal{\ell }}_j\le 2$, the corresponding inequalities in GAP relaxation may be changed to equalities. The GAP relaxation is suited for instances that contain a clause of length two. If ${\mathcal{\ell }}_j\ge 3,\hspace{0.17em}\forall j\in [m]$, then $(Y,y)=(I,\mathbf{0})$ is always feasible for GAP whether the underlying SAT instance is satisfiable or not.

We now state the SDP relaxations of SAT by Anjos (2004a, b; 2005; 2006; 2007) that are not restricted to the lengths of the clauses in instances. Let $\varphi$ be a proposition on n variables and m clauses and $x\in \{\pm 1\}$ the truth assignment to the variables. Consider a family of subsets $\mathcal{F}=\{{\alpha }_1,\dots ,{\alpha }_s\}$, let $\mathbf{x}={(x^{{\alpha }_1},\hspace{0.17em}\dots ,x^{{\alpha }_s})}^{\top }$, and define $Y≔\mathbf{x}{\mathbf{x}}^{\top }$. It is clear that $\text{rank}(Y)=1$, diag$(Y)=\mathbf{1}$, and $Y⪰0$. Later, to obtain a semidefinite relaxation of SAT, we omit the rank-one constraint.

We index the matrix Y with the elements of $\mathcal{F}$ and define for all subsets γ contained in some clause of $\varphi$ the expression

where $△$ is the symmetric difference operator, which is induced by the fact that, for $x\in {\{\pm 1\}}^n$, we have $Y_{\alpha ,\beta }=x^{\alpha }{x}^{\beta }=x^{\alpha △\beta }=x^{\gamma }$; see (5). In general, $Y(\varnothing )$ refers to a diagonal entry of Y; hence, $Y(\varnothing )=1$. We may have $Y(\gamma )=Y_{\varnothing ,\gamma }$, and we assume that, for all γ contained in a clause of $\varphi$, we can always find α and β as in (10).

The expression $Y(\gamma )$ can refer to multiple entries of Y. By construction of Y, these entries are equal. Stated formally, we have $Y\in {\cap }_{j\in [m]}{\mathrm{\Delta }}_j$, where

Observe that the sets Δ_j do not capture all equalities present in Y because of the restriction ${\alpha }_1△{\beta }_1={\alpha }_2△{\beta }_2\subseteq C_j$. In this section, we choose to include only the equalities captured by Δ_j. This keeps our work in line with previous relaxations by Anjos (2004a), and these equalities suffice to prove the main theorem in this section; see Theorem 1. In Section 6, we consider an SDP relaxation of SAT that considers all equalities present in Y.

If x is a satisfying assignment to $\varphi$, then $v(C_j)=1$ (see (6)) for all $j\in [m]$. We can rewrite this constraint in terms of $Y(\gamma )$; see (10). We now omit the rank-one constraint on Y to obtain the following semidefinite feasibility program, denoted by $R_{\mathcal{F}}(\varphi )$:

The program $R_{\mathcal{F}}(\varphi )$ contains both the GAP relaxation and the relaxations proposed by Anjos (2004b) as special cases. Specifically, one obtains the GAP relaxation from $R_{\mathcal{F}}(\varphi )$ by taking $\mathcal{F}=\{\alpha \subseteq [n]||\alpha |\le 1\}$. de Klerk et al. (2000) prove that, whenever GAP is feasible for a 2-SAT instance, the 2-SAT instance is satisfiable. Note that 2-SAT is decidable in linear time (Aspvall et al. 1979) unlike the NP-complete k-SAT with $k\ge 3$.

The GAP relaxation can be considered as a semidefinite program in the first level of the well-known Lasserre (2001) hierarchy. Anjos (2004b) proposes semidefinite relaxations of SAT in approximately levels two and three of the Lasserre (2001) hierarchy by only adding a subset of products of variables to the moment relaxation. For example, Anjos (2004a) proposes the R₂ relaxation, which can be obtained from $R_{\mathcal{F}}(\varphi )$ by taking

Anjos (2004a) proves that the R₂ relaxation attains a rank-two guarantee on 3-SAT instances: whenever the SDP admits a feasible matrix of rank two or lower, the corresponding SAT instance is satisfiable. We now prove that, for a different $\mathcal{F}$ than (12), the resulting relaxation $R_{\mathcal{F}}(\varphi )$ provides the same rank-two guarantee.

Theorem 1.

Let $\varphi$ be a 3-SAT instance and $\mathcal{F}=\{\alpha \subseteq [n]|\alpha \subseteq C_j\hspace{0.17em}\text{for} \text{some} j,|\alpha |\ne 1\}$. Let Y be the matrix variable of $R_{\mathcal{F}}(\varphi )$ indexed by elements of $\mathcal{F}$. If $R_{\mathcal{F}}(\varphi )$ admits a feasible rank-two matrix, then $\varphi$ is satisfiable.

Proof.

See Online Appendix A. □

4. Sum of Squares and MAX-SAT

In Section 4.1, we first provide an overview of the approach of van Maaren et al. (2008) for deriving relaxations for MAX-SAT. Their approach exploits SOS optimization, which has received much attention in the literature (see, e.g., Lasserre 2007, Laurent 2009, Scheiderer 2009, Parrilo and Thomas 2020). Relaxations depend on a basis that is used to compute them. We introduce a parametric family of monomial bases with increasing complexity. In Section 4.2, we derive several properties of monomial bases that are later used in our computations.

4.1. General Overview

For a given logical proposition $\varphi$ on n variables and m clauses, the value

for $a_{j,i}$ as in (3) equals the number of unsatisfied clauses by truth assignment $x\in {\{\pm 1\}}^n$. Hence, we are interested in minimizing $F_{\varphi }$ over ${\{\pm 1\}}^n$, on which $F_{\varphi }$ is nonnegative. Let $\mathbb{R}[x]$ be the set of real polynomials in x. We defineas the set of SOS polynomials modulo $\mathcal{I}$, where $\mathcal{I}$ is the vanishing ideal of ${\{\pm 1\}}^n$. That is,

By Putinars Positivstellensatz (Putinar 1993), $\mathcal{V}$ is the set of nonnegative polynomials on ${\{\pm 1\}}^n$. Generally, optimization over $\mathcal{V}$ is intractable because of its size, which is why we consider

where x is some monomial basis. Because $M⪰0$, it follows that all polynomials of ${\mathcal{V}}_{\mathbf{x}}$ are nonnegative on ${\{\pm 1\}}^n$. Therefore, ${\mathcal{V}}_{\mathbf{x}}\subseteq \mathcal{V}$, and we may approximate the minimum of $F_{\varphi }$ by

The description of ${\mathcal{V}}_{\mathbf{x}}$ shows that computing this lower bound can be done via SDP.

It is important to note that, in the quotient ring of $\mathbb{R}[x]$ modulo $\mathcal{I}$, all terms $x_i^2\equiv 1$, and thus, it suffices to consider only monomials in x for which the highest power is at most one. Thus, we can write

where $p_{\varphi }^{\alpha }\in \mathbb{R}$ for all $\alpha \subseteq [n]$ and $x^{\alpha }$ as in (5). For the constant term of $F_{\varphi }(x)$, we have

We say that monomial basis x represents a logical proposition $\varphi$ if matrix $\mathbf{X}\equiv \mathbf{x}{\mathbf{x}}^{\top }\hspace{0.17em}\mathrm{mod}\hspace{0.17em}\mathcal{I}$ contains all monomials $x^{\alpha }$ for which $p_{\varphi }^{\alpha }\ne 0$. We index this matrix X and the matrix M from (16) with subsets $\alpha \subseteq [n]$ for which $x^{\alpha }\in \mathbf{x}$. Note that for such $\alpha ,\beta \subseteq [n]$, we have

For $\alpha \subseteq [n]$, we write $x^{\alpha }\in \mathbf{X}$ if X has an entry equal to $x^{\alpha }$ (modulo $\mathcal{I}$). van Maaren et al. (2008) propose multiple monomial bases x, among them basis SOS_p, given by

It is stated in van Maaren et al. (2008) that SOS_p represents 2-SAT and 3-SAT instances. Whereas this is true, this basis also represents 4-SAT instances (see Lemma 2). We additionally define for $\mathbf{Q}\in \mathbb{N}$, as an extension to SOS_p, the basis

Basis $SO{S}_p^{\mathbf{Q}}$ takes basis SOS_p and adds all the $\left(\begin{array}{c}\mathbf{Q}\\ 2\end{array}\right)$ quadratic terms of the Q variables appearing in the highest number of clauses of $\varphi$. Any basis x is considered to have duplicate monomials removed, and so, for small values of Q, bases $SO{S}_p^{\mathbf{Q}}$ and SOS_p might coincide.

We also define the basis $SO{S}_s^{\theta }$ for $\theta \in [0,1]$, which is suited for (MAX-)2-SAT instances. This basis consists of all the monomials of degrees one and zero plus a percentage θ of all quadratic monomials appearing in SOS_p. The included quadratic monomials are those that appear in SOS_p and attain the highest monomial weight w, which is defined as $w(x^{\alpha })≔{\sum }_{i\in \alpha }w(i)$, where $w(i)≔|\{C\in \varphi |i\in C\}|$ for $i\in [n]$. This results in the following chain of inclusions:

We now define, for all $\gamma \subseteq [n]$ such that $x^{\gamma }\in \mathbf{X}$, a set of ordered pairs as follows:

Set ${\mathbf{x}}^{\gamma }$ contains the index pairs $(\alpha ,\beta )$ such that ${\mathbf{X}}_{\alpha ,\beta }\equiv x^{\gamma }$. Therefore, $F_{\varphi }\equiv {\mathbf{x}}^{\top }M\mathbf{x}$ if and only if

Constraints of this form are sometimes referred to as coefficient matching conditions in SOS literature (Zheng et al. 2017). We define

as the set of matrices satisfying the coefficient matching conditions for all monomials except $x^{\varnothing }$.

Note that M is constrained to be symmetric, which is reflected in the definition of ${\mathbf{x}}^{\gamma }$, because $(\alpha ,\beta )\in {\mathbf{x}}^{\gamma }$ if and only if $(\beta ,\alpha )\in {\mathbf{x}}^{\gamma }$. Moreover, ${\mathbf{x}}^{\varnothing }$ contains the index pairs of the diagonal entries of M, which correspond to zero-degree monomials in X. Hence, if $F_{\varphi }-\lambda \equiv {\mathbf{x}}^{\top }M\mathbf{x}$, then $p_{\varphi }^{\varnothing }-\lambda =〈I,M〉$; see (17) and (19). To maximize the lower bound on $F_{\varphi }$ (see (17)), we maximize λ, which is, thus, equivalent to minimizing $〈I,M〉$. We can, therefore, compute this lower bound by solving the following SDP:

We note that, for the purpose of solving ${\mathtt{P}}_{\varphi }$ through interior point methods, program ${\mathtt{P}}_{\varphi }$ is strictly feasible: for any feasible matrix M, matrix M + I is strictly feasible. The existence of any such feasible matrix M follows from the nonnegativity of $F_{\varphi }$ on ${\{\pm 1\}}^n$. We postpone the derivation of the dual of ${\mathtt{P}}_{\varphi }$ to Section 6, in which we also show its strict feasibility in Theorem 2.

4.2. Properties of $SO{S}_p^{\mathbf{Q}}$

We provide several properties of monomial bases that are exploited within the PRSM; see Section 7.

Denote by $|{\mathbf{x}}^{\gamma }|$ the cardinality of the set ${\mathbf{x}}^{\gamma }$; see (24). Because of the symmetry of X (see (20)), $|{\mathbf{x}}^{\gamma }|$ is an even number and greater than or equal to two. In particular, when $|{\mathbf{x}}^{\gamma }|=2$, say ${\mathbf{x}}^{\gamma }=\{(\alpha ,\beta ),(\beta ,\alpha )\}$, we have

Thus, whenever $|{\mathbf{x}}^{\gamma }|=2$, the constraint involving ${\mathbf{x}}^{\gamma }$ in ${\mathcal{M}}_{\varphi }$ (see (26)), simply fixes two entries of M. van Maaren et al. (2008) refer to these constraints arising from $|{\mathbf{x}}^{\gamma }|=2$ as unit constraints. In section 7 of van Maaren et al. (2008), the authors empirically show that a high percentage of the constraints of ${\mathcal{M}}_{\varphi }$ are unit constraints. van Maaren et al. (2008) propose as future work the development of an SDP solver that is able to exploit the large number of unit constraints. We propose an algorithm for approximately solving ${\mathtt{P}}_{\varphi }$ in Section 7 that is able to do so.

The following lemma describes the subsets γ that induce unit constraints.

Lemma 1.

Let $\varphi$ be a (MAX-)SAT instance on n variables and m clauses and x a monomial basis that contains at least all of the monomials induced by the SOS_p basis; see (21). Then, for all $\gamma \subseteq [n]$, we have $|{\mathbf{x}}^{\gamma }|=2\Rightarrow p_{\varphi }^{\gamma }=0$, where $p_{\varphi }^{\gamma }$ is a coefficient of $F_{\varphi }(x)$; see (18).

Proof.

See Online Appendix A. □

Lemma 1 implies that, in an implementation that uses the SOS_p basis, it is not required to store the coefficients corresponding to unit constraints (because these all equal zero), but only the indices restricted by the unit constraints. The converse of Lemma 1 is generally not true. That is, there can exist many subsets $\gamma \subseteq [n]$ for which $p_{\varphi }^{\gamma }=0$, but $|{\mathbf{x}}^{\gamma }|>2$.

Lemma 2.

Let $\varphi$ be an SAT instance on n variables and x its monomial basis according to $SO{S}_p^{\mathbf{Q}}$ for some $\mathbf{Q}\in \mathbb{N}$. Let $\gamma \subseteq [n]$. Then,

1. $|\gamma |\in \{1,2\}\Rightarrow |{\mathbf{x}}^{\gamma }|\le 2n$.

2. $|\gamma |\in \{3,4\}\Rightarrow |{\mathbf{x}}^{\gamma }|\le 6$.

3. $|\gamma |>4\Rightarrow |{\mathbf{x}}^{\gamma }|=0$.

Proof.

See Online Appendix A. □

Part 3 of Lemma 2 shows that the $SO{S}_p^{\mathbf{Q}}$ bases are only suited for (MAX-)k-SAT when $k\le 4$.

5. Resolution and Monomial Bases

In this section, we consider resolution in combination with the SOS approach to MAX-SAT. Resolution is a technique from mathematical logic and widely employed by MAX-SAT solvers (Prasad et al. 2005). Resolution takes as inputs two clauses of a proposition $\varphi$ and returns a set of new clauses named the resolvent clauses. The resolvent clauses transform $\varphi$ into $\varphi \prime$ by either replacing the original clauses or adding the resolvent clauses to $\varphi$ (depending on which resolution rule is used). We show in this section that the MAX-SAT resolution rule might not be beneficial for the SOS approach applied to MAX-SAT and can even decrease its effectiveness. However, in Section 8.2, we show how to benefit from the SAT resolution rule in partial MAX-SAT.

We show this using an example. For $k\ge 3$, we define the following proposition on k variables:

It is clear that ${\varphi }_k$ is unsatisfiable. If one satisfies the initial two unit clauses and performs unit resolution, more unit clauses appear. Repeating this process leads to an all-false truth assignment, leaving clause $x_2\vee x_3$ unsatisfied. Therefore, any truth assignment leaves at least one clause unsatisfied, and hence, ${\text{min}}_{x\in {\{\pm 1\}}^k}{F}_{{\varphi }_k}=F_{{\varphi }_k}(-{\mathbf{1}}_k)=1$ for $F_{{\varphi }_k}$ as in (13). In the following lemma, we show that the SOS_p basis (see (21)), suffices for proving optimality of this assignment.

Lemma 3.

For all $k\ge 3$, we have $\text{max}\{\lambda |F_{{\varphi }_k}-\lambda \in {\mathcal{V}}_{\mathbf{x}}\}=1$, where $\mathbf{x}={\mathit{\text{SOS}}}_p({\varphi }_k)$, and ${\mathcal{V}}_{\mathbf{x}}$ as in (16).

Proof.

See Online Appendix A. □

Let us now present the MAX-SAT resolution rule (see, e.g., Abramé and Habet 2014). For clauses C₁ and C₂ of some proposition $\varphi$, on literals x, z_i, $i\in [s]$ and y_i, $i\in [t]$ construct the clauses below the horizontal line:

The MAX-SAT resolution rule states that one may replace clauses C₁ and C₂ in $\varphi$ with a subset of the $1+s+t$ resolvent clauses below the horizontal line. Namely, clauses that are trivially satisfied, such as $x\vee \neg x$, are not part of this subset. We refer to the resulting new proposition, obtained after resolution, as $\varphi \prime$. In Bonet et al. (2007), theorem 4, it is proven that $F_{\varphi }=F_{\varphi \prime }$; see (13). Note that, in Bonet et al. (2007), definition 6, function $F_{\varphi }$ is stated in terms of $\{0,1\}$ variables.

For standard MAX-SAT solvers, one of the goals of resolution is to create new unit clauses, which are used to compute upper bounds on the MAX-SAT solution (Abramé and Habet 2014). For our SDP approach, assuming a fixed monomial basis, the sets ${\mathcal{M}}_{\varphi }$ and ${\mathcal{M}}_{\varphi \prime }$ (see (26)), depend only on the coefficients of $F_{\varphi }$ and $F_{\varphi \prime }$. Because $F_{\varphi }=F_{\varphi \prime }$, these coefficients are equal, and thus, ${\mathcal{M}}_{\varphi }={\mathcal{M}}_{\varphi \prime }$. Note that the feasible set of ${\mathtt{P}}_{\varphi }$ is defined in terms of ${\mathcal{M}}_{\varphi }$. Hence, it follows that, if given the same basis, program ${\mathtt{P}}_{\varphi }$ equals program ${\mathtt{P}}_{\varphi \prime }$. This equivalence of programs suggests that MAX-SAT resolution does not change our approach; however, we find that, in general, ${\mathit{\text{SOS}}}_p(\varphi )\ne {\mathit{\text{SOS}}}_p(\varphi \prime )$; see (21). We investigate the effect of this difference.

Returning to the example of ${\varphi }_k$ in (28), let us define $C_q=\neg x_q\vee x_{q+1}$. Observe that, for $3\le q\le k-1,\hspace{0.17em}{C}_q\in {\varphi }_k$ (assuming k > 3). Let us fix some q, $3\le q\le k-3$, and consider the clauses $C_q,\hspace{0.17em}{C}_{q+1},\hspace{0.17em}{C}_{q+2}\in {\varphi }_k$. We perform resolution as

We perform resolution again on the third new clause obtained in (30) and $C_{q+2}$ to obtain

and, here, the resolution rule states that one may replace the original clauses C₁, C₂, and C₃ with the six new resolvent clauses obtained from (30) and (31) (the third resolvent from (30) is not counted because it is replaced in the resolution in (31)).

Observe that the SOS_p basis generates six quadratic monomials for the new resolvent clauses, whereas originally, only three quadratic monomials are generated for C_q, $C_{q+1}$, and $C_{q+2}$. We now define ${\varphi }_k^{\prime }$ for $k\ge 6$ as the logical proposition, obtained by taking ${\varphi }_k$ and performing resolution as in (30) and (31) for each triple of clauses $\{C_q,\hspace{0.17em}{C}_{q+1},\hspace{0.17em}{C}_{q+2}\}$ for each $q\in \{3,\hspace{0.17em}6,\hspace{0.17em}9,\dots ,k-3\}$ (let us assume here that k is a multiple of three). Note that proposition ${\varphi }_k^{\prime }$ constitutes a MAX-4-SAT instance, and therefore, basis SOS_p is applicable. Let us compare the sizes of the resulting SOS_p bases, denoted as $|{\mathit{\text{SOS}}}_p|$. We have $|{\mathit{\text{SOS}}}_p({\varphi }_k)|=2k<3k-3=|{\mathit{\text{SOS}}}_p({\varphi }_k^{\prime })|.$

Thus, compared with ${\mathit{\text{SOS}}}_p({\varphi }_k)$, basis ${\mathit{\text{SOS}}}_p({\varphi }_k^{\prime })$ adds approximately k monomials. None of these monomials strengthens the bound because ${\mathit{\text{SOS}}}_p({\varphi }_k)$ is already sufficient for proving optimality by Lemma 3. It is clear that having a larger basis without offering a stronger bound is inefficient because solving ${\mathtt{P}}_{\varphi }$ requires more time for larger matrices.

The example of ${\varphi }_k^{\prime }$ and ${\varphi }_k$ shows that not all monomials are (equally) useful in determining bounds. It also shows that resolution can decrease the effectiveness of the SOS approach to MAX-SAT by providing “bad” monomial bases or it can occur that the SOS_p basis misses “good” monomials. Our proposed basis $SO{S}_p^{\mathbf{Q}}$ (see (22)) attempts to solve this issue.

6. Relating Sum of Squares and Method of Moments

In this section, we show how the SOS-SDP relaxation of van Maaren and van Norden (2005) and van Maaren et al. (2008) and moment relaxations of Anjos (2004a, b; 2005; 2006; 2007) are related. The relaxations of Anjos as described in Section 3 are first introduced in Anjos (2004a) and can be considered as extensions of the GAP relaxation via the well-known Lasserre (2001) hierarchy. van Maaren and van Norden (2005) propose the SOS approach to (MAX-)SAT. Subsequently, van Maaren and van Norden (2005) show that the SOS relaxation, using monomial basis SOS_pt that is larger than SOS_p (see (21)) outperforms the R₃ relaxation of Anjos (2005) in deciding on the satisfiability of 3-SAT instances. The R₃ relaxation is known to dominate the R₂ relaxation; see (12). Anjos (2007) strengthened his R₃ relaxation further and left it as future work to determine which SDP relaxation was the strongest.

We complete that work here by showing a simple relation between the two approaches. In particular, Anjos’ relaxations can be considered as method of moments in the Lasserre (2001) hierarchy. It is well-known that method of moments is dual to SOS optimization (see Lasserre 2001), and we work out the details here. Let us first derive the dual of the SOS program ${\mathtt{P}}_{\varphi }$ (see Theorem 2) and then relate it to the here proposed strengthened version of Anjos’ relaxations.

To this end, we require the following intermediate result on $v_{\varphi }$; see (7).

Lemma 4.

Let $\varphi ={\bigwedge }_{j=1}^m{C}_j$ be a logical proposition, $v_{\varphi }={\sum }_{\alpha \subseteq [n]}{v}_{\varphi }^{\alpha }{x}^{\alpha }$ (see (7)), and $F_{\varphi }={\sum }_{\alpha \subseteq [n]}{p}_{\varphi }^{\alpha }{x}^{\alpha }$; see (18). Then, $v_{\varphi }=m-F_{\varphi }.$ and $v_{\varphi }^{\alpha }=-p_{\varphi }^{\alpha }$ for all nonempty $\alpha \subseteq [n]$.

Proof.

See Online Appendix A. □

Let x be a given monomial basis, $S\in {\mathcal{S}}^{|\mathbf{x}|}$. Matrix S is indexed by all $\alpha \subseteq [n]$ for which $x^{\alpha }\in \mathbf{x}$. To simplify the comparison between the SOS approach and the relaxations of Anjos (2004a), we define the set

for a proposition $\varphi$ on n variables and m clauses. Note that ${\mathcal{X}}_{\varphi }\subseteq {\cap }_{j\in [m]}{\mathrm{\Delta }}_j$ (see (11)) because Δ_j only restricts entries $S_{\alpha ,\beta }$ whenever α and β are jointly contained in a single clause. We use ${\mathcal{X}}_{\varphi }$ in the following theorem.

Theorem 2.

Let $\varphi$ be a logical proposition and x a monomial basis. The SOS program ${\mathtt{P}}_{\varphi }$ defined by $\varphi$ and x is equivalent to

$$\begin{array}{l}\text{max}\hspace{1em}〈C,S〉\hspace{1em}\text{s}.\text{t}.\hspace{1em}S\in {\mathcal{X}}_{\varphi }\cap {\mathcal{S}}_{+},\hfill \end{array}$$(33)

where ${\mathcal{X}}_{\varphi }$ is given by (32) and $C\in {\mathcal{S}}^{|\mathbf{x}|}$, indexed by the subsets $\alpha \subseteq [n]$ for which $x^{\alpha }\in \mathbf{x}$, is any matrix that satisfies ${\sum }_{(\alpha ,\beta )\in {\mathbf{x}}^{\gamma }}{C}_{\alpha ,\beta }=v_{\varphi }^{\gamma },\hspace{0.17em}\hspace{0.17em}\forall \gamma \ne \varnothing ,\hspace{0.17em}{\mathbf{x}}^{\gamma }\ne \varnothing$ for $v_{\varphi }^{\gamma }$ as in (7). Moreover, (33) is strictly feasible.

Proof.

We rewrite program ${\mathtt{P}}_{\varphi }$ by splitting the matrix variable M as follows:

$$v≔\text{min}〈I,M〉\hspace{1em}\text{s}.\text{t}.\hspace{1em}M=Z,\hspace{0.17em}M\in {\mathcal{M}}_{\varphi },\hspace{0.17em}Z\in {\mathcal{S}}_{+},$$(34)

where ${\mathcal{M}}_{\varphi }$ as in (26). We dualize the constraint M = Z, and set

$$g(S)≔\underset{M\in {\mathcal{M}}_{\varphi },Z⪰0}{\text{min}}〈I,M〉+〈S,M-Z〉,$$

for some $S\in \mathcal{S}$. Clearly, $g(S)\le v$ for all S, and we, thus, look to maximize g(S); that is,

$$\begin{array}{l}\underset{S}{\text{max}}g(S)=\underset{S}{\text{max}}[\underset{M\in {\mathcal{M}}_{\varphi }}{\text{min}}〈I+S,M〉+\underset{Z⪰0}{\text{min}}\hspace{0.17em}〈S,-Z〉]=\underset{S⪯0}{\text{max}}\underset{M\in {\mathcal{M}}_{\varphi }}{\text{min}}〈I+S,M〉\\ =\underset{S⪰0}{\text{max}}\underset{M\in {\mathcal{M}}_{\varphi }}{\text{min}}〈I-S,M〉.\end{array}$$(35)

We now determine the set ${\mathcal{X}}_{\varphi }$ such that, whenever $S\in {\mathcal{X}}_{\varphi }$, the minimization over $M\in {\mathcal{M}}_{\varphi }$ in (35) is bounded. Observe that ${\mathcal{M}}_{\varphi }$ places no restrictions on the diagonal. To guarantee a bounded minimum, set ${\mathcal{X}}_{\varphi }$ should restrict $\text{diag}(I-S)=\mathbf{0}$. Each off-diagonal element of a matrix in ${\mathcal{M}}_{\varphi }$ is restricted by a single constraint of the form (25). Therefore, solving (35) for M can be done by considering separately the elements of M restricted by a single constraint. That is,

$$\underset{M\in \mathcal{S}}{\text{min}}\hspace{1em}{\displaystyle \sum _{\gamma \in \mathbf{X}}\hspace{0.17em}}\hspace{0.17em}{\displaystyle \sum _{(\alpha ,\beta )\in {\mathbf{x}}^{\gamma }}-}{S}_{\alpha ,\beta }{M}_{\alpha ,\beta }\hspace{1em}\text{s}.\text{t}.\hspace{1em}{\displaystyle \sum _{(\alpha ,\beta )\in {\mathbf{x}}^{\gamma }}{M}_{\alpha ,\beta }}=p_{\varphi }^{\gamma },$$(36)

where ${\mathbf{x}}^{\gamma }$ and X are defined in (24) and (20), respectively. This minimization problem is bounded if and only if

$$S_{\alpha ,\beta }=S_{\alpha \prime ,\beta \prime },\hspace{0.17em}\hspace{0.17em}\forall (\alpha ,\beta ),\hspace{0.17em}(\alpha \prime ,\beta \prime )\in {\mathbf{x}}^{\gamma }\hspace{0.17em}\hspace{0.17em}\forall x^{\gamma }\in \mathbf{X},$$(37)

or equivalently, $S_{\alpha ,\beta }=S_{\alpha \prime ,\beta \prime }$ for all possible index pairs $(\alpha ,\beta )$ and $(\alpha \prime ,\beta \prime )$ that satisfy $\alpha △\beta =\alpha \prime △\beta \prime$. It follows that ${\mathcal{X}}_{\varphi }$ is given by (32). Now, for fixed $S\in {\mathcal{X}}_{\varphi }\cap {\mathcal{S}}_{+}$, any matrix $M\in {\mathcal{M}}_{\varphi }$ obtains the same value in (35). Note also that, w.l.o.g., we may fix $M={\mathcal{P}}_{{\mathcal{M}}_{\varphi }}(\mathbf{0})$, that is, the projection of the zero matrix onto ${\mathcal{M}}_{\varphi }$ (see Lemma 5), which has zero diagonal. This yields the equivalent program of the form (33) for $C=-M=-{\mathcal{P}}_{{\mathcal{M}}_{\varphi }}(\mathbf{0})$. Written explicitly, $C_{\alpha ,\beta }=-p_{\varphi }^{\gamma }/|{\mathbf{x}}^{\gamma }|$ for all $\alpha ,\beta \subseteq [n]$ such that $\alpha △\beta =\gamma$ (i.e., $(\alpha ,\hspace{0.17em}\beta )\in {\mathbf{x}}^{\gamma }$). This, combined with Lemma 4, proves the claim on matrix C. Finally, observe that the identity matrix of appropriate size is strictly feasible for (33). □

We define, for $S\in {\mathcal{X}}_{\varphi }$ and each clause C_j, the function $v^{\text{SDP}}(S,C_j)$, which is obtained by taking (6) and replacing each $x^{\gamma }$ by $S_{\alpha ,\beta }$ for some $(\alpha ,\beta )\in {\mathbf{x}}^{\gamma }$. By (37), we are allowed to pick any such $(\alpha ,\beta )$. By Lemma 4, for any nonempty $\gamma \subseteq [n],\hspace{0.17em}S\in {\mathcal{X}}_{\varphi }$ and C as in Theorem 2, we have

Hence, maximizing $〈C,S〉$ is equivalent to maximizing the semidefinite relaxation of $v_{\varphi }$ (see (7)), which equals ${\sum }_{j\in [m]}{v}^{\text{SDP}}(S,C_j)$.

Moreover, in the relaxations of Anjos (2004a) outlined in Section 3, the matrix variable is restricted to satisfy $v^{\text{SDP}}(S,C_j)=1$. Now, we can easily observe the difference between the SOS-SDP relaxations and those proposed by Anjos. We present the equivalent dual formulation of the SOS approach on the left-hand side and the latter (in slightly adapted form) on the right.

Note again the difference between (40) and the relaxations described in Section 3, resulting from using set ${\mathcal{X}}_{\varphi }$ instead of the intersection of the Δ_j; see (11). Thus, we compare the SOS approach with a strengthened variant of the relaxation proposed by Anjos. In Section 8.3, we determine the dual of (40).

Program (39) proves the unsatisfiability of $\varphi$ if $v^{*}<m$ (with some margin of error because of numerical precision), whereas (40) does so whenever the program is infeasible. These programs are not equivalent in this sense: we empirically find instances $\varphi$ for which $v^{*}\ge m$, whereas (40) is infeasible. Neither program can directly prove satisfiability. However, solutions to both programs can be used to guide the search toward satisfying assignments (should they exist); see Online Appendix C.

If (40) admits a feasible matrix $S^{*}$, then matrix $S^{*}$ is clearly also feasible for (39) and attains an objective value of m. Consequently, in this case, we have $v^{*}\ge m$. Thus, if (40) does not prove unsatisfiability of $\varphi$, then neither does (39). In Online Appendix F, we show that (39) can be computed efficiently by applying the PRSM to its dual.² It is currently unclear whether a good algorithm for solving (40) exists, and if so, how efficient it would be. Previous numerical experiments on (40) use general purpose SDP solvers. An immediate improvement might be to use an SDP feasibility problem solver (see Henrion and Malick 2011, Drusvyatskiy et al. 2017).

Finally, the objective value of (39) is more useful for MAX-SAT: if the underlying instance is infeasible, $v^{*}$ provides an upper bound to the number of satisfiable clauses, which is useful in a B&B scheme. Program (40) might also show unsatisfiability of the same instance, but its infeasibility offers no additional value as to how unsatisfiable the instance is.

7. The Peaceman–Rachford Splitting Method for MAX-SAT

In this section, we introduce the Peaceman–Rachford splitting method (Peaceman and Rachford 1955) for solving SOS-SDP problems and apply it to the MAX-SAT SOS program ${\mathtt{P}}_{\varphi }$. Conventionally, interior point methods are used to solve SDP problems. However, for medium- and large-size instances, interior point methods suffer from a large computation time and memory demand, which has recently motivated researchers to consider first order methods, such as the PRSM. For recent applications of PRSM to SDP, see, for example, de Meijer and Sotirov (2021) and Graham et al. (2022).

Section 7.2 and Online Appendix C provide details on obtaining valid upper and lower bounds from the output of the PRSM algorithm.

7.1. The PRSM for SOS Relaxations of MAX-SAT

We start from the reformulation of ${\mathtt{P}}_{\varphi }$ given in (34). The augmented Lagrangian function of (34) with respect to (w.r.t.) the constraint M = Z for a penalty parameter $\beta >0$ is

Here, $S\in {\mathcal{S}}^n$ is the Lagrange multiplier and ${\Vert ·\Vert }_F$ denotes the Frobenius matrix norm; see Section 1.1.

The PRSM now entails iteratively optimizing over the variables Z and M separately and updating S twice per cycle. We write superscript k to denote the the value of the variable at iteration k:

Here, ${\mathcal{M}}_{\varphi }$ is as in (26), and $\mathcal{P}$ is the projection operator as in (4). We use that

see, for example, Oliveira et al. (2018). In an implementation of (42), one should not store matrix S^k directly but, rather, the matrix $\frac{1}{\beta }{S}^k$; see Online Appendix G. When $X\in \mathcal{S}$ has eigenvalues λ_i and corresponding eigenvectors v_i, it is well-known that the projection onto the positive semidefinite cone is given by

Depending on the number of positive eigenvalues of X, one of these expressions is cheaper to compute. The next lemma shows how to compute a projection onto ${\mathcal{M}}_{\varphi }$.

Lemma 5.

Let matrices $M,\hspace{0.17em}\widehat{M}\in \mathcal{S}$, indexed by subsets of $[n]$ such that $\widehat{M}={\mathcal{P}}_{{\mathcal{M}}_{\varphi }}(M)$, where the projection operator ${\mathcal{P}}_{{\mathcal{M}}_{\varphi }}(·)$ is given by (4). Then, $\text{diag}(\widehat{M})=\text{diag}(M)$ and

$${\widehat{M}}_{\delta ,\mu }=M_{\delta ,\mu }-\frac{1}{|{\mathbf{x}}^{\gamma }|}\left({\displaystyle \sum _{(\alpha ,\beta )\in {\mathbf{x}}^{\gamma }}{M}_{\alpha ,\beta }}-p_{\varphi }^{\gamma }\right),$$(45)

for $(\delta ,\mu )\in {\mathbf{x}}^{\gamma },\hspace{0.17em}\gamma \ne \varnothing$. In particular, when $|{\mathbf{x}}^{\gamma }|=2$, (45) reduces to ${\widehat{M}}_{\delta ,\mu }={\widehat{M}}_{\mu ,\delta }=p_{\varphi }^{\gamma }/2$.

Proof.

See Online Appendix A. □

Because of the presence of many unit constraints (see (27)), these projections are computationally cheap to compute, and hence, the PRSM is well-suited to exploit this. Finally, it is proven (He et al. 2016) that (42) converges for $({\gamma }_1,\hspace{0.17em}{\gamma }_2)\in \mathcal{D}$, where

The values that we choose for $({\gamma }_1,{\gamma }_2)$ and other parameters are given in Online Appendix F.

7.2. Upper Bounds, Lower Bounds, and Early Stopping

After each PRSM iterate k, we obtain a triple $(Z^k,M^k,S^k)$ and the resulting $〈I,M^k〉.$ Although this value converges to the optimal solution of the SDP, the convergence is (typically) not monotonic, and therefore, this value does not necessarily provide a valid upper bound for the problem. In this section, we describe how to obtain a valid upper bound from the output of the PRSM.

Observe that the feasible set of ${\mathtt{P}}_{\varphi }$ depends on the chosen monomial x through ${\mathcal{V}}_{\mathbf{x}}$; see (16). Hence, by (17), we have

for $p_{\varphi }^{\varnothing }$ as in (19). From this, it follows that the maximum number of satisfiable clauses of $\varphi$ is bounded from above byfor m equal to the number of clauses in $\varphi$. Because the number of satisfied clauses is an integer, the bound (48) can be improved by rounding down the result.

Ideally, the PRSM algorithm (42) computes the upper bound (48) by finding the optimal M in the set ${\mathcal{M}}_{\varphi }\cap S_{+}$ (up to some given numerical precision). However, in practice, one terminates the PRSM algorithm before this optimal M is found. Let matrix M^k then be defined as in (42) and let ${\lambda }_{\text{min}}(M^k)$ be its smallest eigenvalue. Note that

and so ${\tilde{M}}^k$ is feasible for ${\mathtt{P}}_{\varphi }$. Thus, a valid upper bound at iteration k is obtained as follows:

In Online Appendix C, we outline a method for determining lower bounds when using the PRSM.

8. Weighted Partial MAX-SAT

In this section, we extend the SOS approach from MAX-SAT to weighted partial MAX-SAT. We also show that the dual formulation of the SOS program for certain partial MAX-SATs equals the relaxations by Anjos (2005).

In weighted MAX-SAT, each clause is given a weight, and the objective is to maximize the sum of the weights of the satisfied clauses. In partial MAX-SAT, clauses are divided into soft and hard clauses. The aim is to maximize the number of satisfied soft clauses, satisfying all the hard clauses. The combination of weighted and partial MAX-SAT is clear and referred to as weighted partial MAX-SAT (Li and Manya 2021).

Consider again a logical proposition $\varphi$. Let $w_j\in \mathbb{R}$ be the weight associated to clause C_j. The generalization of (13) for (unweighted) MAX-SAT to weighted MAX-SAT follows by setting

and then minimizing $F_{\varphi }^{\mathcal{W}}$ for $x\in {\{\pm 1\}}^n$. This minimization can be approximated by SOS optimization, using directly the semidefinite program ${\mathtt{P}}_{\varphi }$.

For weighted partial MAX-SAT, consider a logical proposition $\varphi$ on n variables, m soft clauses C_j, and q hard clauses $C_p^{\mathbf{H}}$. To each hard clause $C_p^{\mathbf{H}},\hspace{0.17em}p\in [q]$, we associate the polynomial $f_p={\prod }_{i\in [n]}(1-a_{p,i}{x}_i)$, similar to (51). Note that f_p vanishes for all truth assignments that satisfy clause $C_p^{\mathbf{H}}$. Similar to (14) and (16), we define the sets

Let $\mathbf{S}\mathbf{A}\mathbf{T}\subseteq {\{\pm 1\}}^n$ be the set of all truth assignments satisfying the hard clauses (which we assume to be nonempty). From Putinar (1993), it follows that

where “+” denotes the Minkowski sum of sets. We proceed by writing the lower bound in (53) as an explicit SDP for which we introduce the following sets: ${\mathbf{H}}^{\gamma }≔\{p\in [q]|\gamma \in C_p^{\mathbf{H}}\}$ for $\gamma \subseteq [n]$. Set ${\mathbf{H}}^{\gamma }$ contains all p for which f_p, when expanded, contains the term $\pm x^{\gamma }$. The sign here is determined by the parity of $|\gamma \cap I_p^{+}|$; see (2). Additionally, we define as analogue to ${\mathcal{M}}_{\varphi }$ (see (26)), the set ${\mathcal{M}}_{\varphi }^{\mathbf{H}}$. This set contains all matrices M and vectors c such that $F_{\varphi }^{\mathcal{W}}-\lambda \equiv {\mathbf{x}}^{\top }M\mathbf{x}+{\sum }_{p\in [q]}{c}_p{f}_p\hspace{1em}\mathrm{mod}\hspace{0.17em}\mathcal{I}$. It is, therefore, defined as

This allows us to adapt ${\mathtt{P}}_{\varphi }$ to weighted partial MAX-SAT as follows:

We approximately solve (55) by the PRSM; see Section 8.1. Let us elaborate on how to adapt the monomial bases to (weighted) partial MAX-SAT. We make no distinction between soft and hard clauses for the SOS_p basis; see (21). For basis $SO{S}_s^{\theta }$ (see (23)), we determine the variable weights as $w(i)≔{\sum }_{\{j|i\in C_j\}}{w}_j+{\sum }_{\{p|i\in C_p^{\mathbf{H}}\}}\overline{w}$ for $\overline{w}$ the mean of all soft clause weights w_j. For basis $SO{S}_p^{\mathbf{Q}}$, we add all $\left(\begin{array}{c}\mathbf{Q}\\ 2\end{array}\right)$ quadratic terms of the Q variables that attain the highest value of w(i). For unweighted partial MAX-SAT instances, we consider all w_j to equal one.

8.1. The PRSM for SOS Relaxations of Weighted Partial MAX-SAT

We show here how to solve (55) by the PRSM. We first rewrite (55) by introducing the matrix variable Z (see also (34)):

Then, the augmented Lagrangian function of (56) w.r.t. Z = M and for a penalty parameter $\beta >0$ is $L_{\beta }(Z,M,S,c)≔L_{\beta }(Z,M,S)+{\mathbf{1}}^{\top }c$; see (41). The PRSM is iteratively and separately optimizing over $(M,c)\in {\mathcal{M}}_{\varphi }^{\mathbf{H}}$ and $Z\in {\mathcal{S}}_{+}$ and updating S twice per cycle, similarly to (42). However, in this case, the M-subproblem from (42) is replaced by the (M, c)-subproblem.

We now show that minimization over $(M,c)\in {\mathcal{M}}_{\varphi }^{\mathbf{H}}$ can be performed efficiently. By derivations similar to (43), we have

where $X≔Z-(S+I)/\beta$. This is a convex quadratic program (QP) that we solve in two steps. First, consider the matrix entries $M_{\alpha ,\beta }$ with $(\alpha ,\beta )\in {\mathbf{x}}^{\gamma }$ (see (24)) and ${\mathbf{H}}^{\gamma }=\varnothing$. Because ${\mathbf{H}}^{\gamma }=\varnothing$, these entries are unaffected by the c_p variables. This implies that these $M_{\alpha ,\beta }$ variables are not coupled with the other entries of M, and one can minimize separately over such $M_{\alpha ,\beta }$. This separate minimization problem can be solved by applying Lemma 5. Second, the remaining QPcan be simplified by the following observation. If $M^{*}$ is an optimal solution to (57), then $(\alpha ,\beta ),(\alpha \prime ,\beta \prime )\in {\mathbf{x}}^{\gamma }\Rightarrow M_{\alpha ,\beta }^{*}-X_{\alpha ,\beta }=M_{\alpha \prime ,\beta \prime }^{*}-X_{\alpha \prime ,\beta \prime }$. Hence, (58) can be simplified by substituting each term ${\sum }_{(\alpha ,\beta )\in {\mathbf{x}}^{\gamma }}{(M_{\alpha ,\beta }-X_{\alpha ,\beta })}^2$ with a single squared variable. We solve the resulting QP either by solving the Karush–Kuhn–Tucker conditions using the lower-upper decomposition or via MOSEK ApS (2023). The solving method depends on the underlying QP.

8.2. Strengthening the Bounds

We demonstrate a simple technique for improving the upper bounds given by Program (55). This technique is based on the SAT resolution rule, which is given as follows. For two hard clauses of some proposition $\varphi$, on literals x, z_i, $i\in [s]$ and y_i, $i\in [t]$, construct the clause below the horizontal line:

In contrast to the MAX-SAT resolution rule (29), the SAT resolution rule states that one may add the clause below the horizontal line to $\varphi$ without changing its (un)satisfiability (we say that the new clause is implied by the original two clauses). We may apply this SAT resolution rule to the hard clauses of a partial MAX-SAT instance to generate more hard clauses. As each new clause induces a new variable c_p, the bound of Program (55) can only improve. One may also regard SAT resolution as extending the set ${\mathcal{H}}_{\mathbf{x}}$ (see (52)), by including terms of the form $c_p{x}^{\alpha }{f}_p$ for some $\alpha \subseteq [n]$, where $c_p\in \mathbb{R}$.

Additionally, SAT resolution can generate hard unit clauses. This is advantageous because hard unit clauses reduce the number of variables in MAX-SAT; see Section 1.2.

8.3. Duality in Partial MAX-SAT

Now, we consider a partial MAX-SAT with only hard clauses. Solving such instances is, thus, equivalent to determining the satisfiability of the given hard clauses. We show that, by taking the dual of the resulting SOS program, one obtains (a stronger version of) the relaxations of Anjos (2004a) given by (40).

We define, for $A\in {\mathcal{S}}^n,\hspace{0.17em}\text{vec}(A)\in {\mathbb{R}}^{n^2}$ the vector whose entries are the columns of A stacked together. We start from Program (55) and perform variable splitting on M, similar to (34). We take the dual g(S) of this formulation, similar to (35), and consider the problem

for ${\mathcal{X}}_{\varphi }$ as in (32). The steps that show $S\in {\mathcal{X}}_{\varphi }\cap {\mathcal{S}}_{+}$ is necessary for the expression to be finite are provided in the proof of Theorem 2. We rewrite the inner minimization problem in (60) asand proceed to show under which conditions this value is bounded. Observe that the coefficients $p_{\varphi }^{\gamma }=0$ (see (54)) because there are no soft clauses. Moreover, the set ${\mathcal{M}}_{\varphi }^{\mathbf{H}}$ places only linear constraints on the entries of M and c. Therefore, there exists a matrix D that satisfies

Hence, (61) is bounded if and only if $[\begin{array}{c}\text{vec}{(S)}^{\top }\hspace{0.17em}{\mathbf{1}}^{\top }\end{array}]$ is contained in the row space of D. This is precisely the requirement that $v^{\text{SDP}}(S,C_p^{\mathbf{H}})=1,\hspace{0.17em}\forall p\in [q]$ as in (40). We provide one example of this claim in Online Appendix D.

Thus, (61) is bounded if $[\begin{array}{c}\text{vec}{(S)}^{\top }\hspace{0.17em}{\mathbf{1}}^{\top }\end{array}]\in \text{row}(D)$, in which case, the value equals zero. Hence, Program (60) is equivalent to (40).

9. Conclusions and Future Work

In this paper, we consider SOS optimization for solving MAX-SAT and weighted partial MAX-SAT. We design an SOS-SDP–based exact MAX-SAT solver called SOS-MS. Our solver is competitive with the best known solvers on solving various (weighted partial) MAX-SAT instances. We are also first to compute SDP bounds for weighted partial MAX-SAT.

In Section 3, we propose a family of semidefinite feasibility problems $R_{\mathcal{F}}(\varphi )$ and show that one member of this family provides the rank-two guarantee; see Theorem 1. That is, the existence of a feasible rank-two matrix implies satisfiability of the corresponding SAT instance. In Section 4, we outline the SOS approach to MAX-SAT from van Maaren et al. (2008) and propose new bases. We introduce the $SO{S}_s^{\theta }$ and $SO{S}_p^{\mathbf{Q}}$ bases (see (23)) and provide several theoretical results related to these bases; see Lemmas 1 and 2. Clearly, the strength of the SOS-SDP–based relaxations and the required time to compute them depend on the chosen monomial basis. The SOS-SDP relaxation for MAX-SAT is denoted by ${\mathtt{P}}_{\varphi }$. We consider MAX-SAT resolution in Section 5 and show that resolution might not be beneficial for the SOS approach applied to MAX-SAT.

In Section 6, we elegantly show a connection between the SOS approach to MAX-SAT and the family of semidefinite feasibility problems $R_{\mathcal{F}}(\varphi )$. This is done by deriving the dual problem to ${\mathtt{P}}_{\varphi }$; see Theorem 2. In Section 7, we propose the PRSM for solving ${\mathtt{P}}_{\varphi }$. We show that PRSM is well-suited for exploiting the structure of ${\mathtt{P}}_{\varphi }$, in particular, the unit constraints; see (27). We, thus, provide an affirmative answer to the key question posed by van Maaren et al. (2008) regarding whether SDP software can be developed dealing with unit constraints efficiently.

We extend the SOS approach for MAX-SAT to weighted partial MAX-SAT in Section 8. Here, the variables are restricted to satisfy a set of hard clauses. We show that such hard clauses can be incorporated in the SOS program ${\mathtt{P}}_{\varphi }$ by adding scalar variables. We show in Section 8.1 that the resulting Program (55) is also well-suited for the PRSM.

In Online Appendix E, we provide implementation details of our SOS-SDP–based MAX-SAT solver, whose pseudocode is given in Online Algorithm 1. SOS-MS is a B&B algorithm and has two crucial components. The first one is the use of warm starts to program ${\mathtt{P}}_{\varphi }$, in order to quickly obtain strong bounds. The second one is its ability to quickly parse ${\mathtt{P}}_{\varphi }$ as outlined in Online Appendix E.1. Our algorithm parses a basis that contains 4,439,449 monomials in (approximately) one second (!).

In Online Appendix F, we provide extensive numerical results that verify efficiency of our exact solver SOS-MS and quality of SOS upper bounds. We show that SOS-MS can solve a variety of MAX-SAT instances in reasonable time, solving some instances faster than the best solvers in the MSE-2016. We show that the $SO{S}_p^{\mathbf{Q}}$ bases (22) are able to prove optimality of some MAX-SAT instances and the parameter Q provides the option to adjust the trade-off between quality of the bounds and computation time. We also test our B&B algorithm for (weighted) partial MAX-SAT instances in Online Appendices F.2 and F.4. Our solver is able to solve many (weighted) partial MAX-SAT instances in a reasonable time.

This paper demonstrates the strong performance of SOS-MS on (weighted partial) MAX-SAT instances from the MSE random track. In the future, we hope to also solve instances with SOS-MS from the so-called industrial and crafted tracks. These tracks currently impose two challenges on SOS-MS. First, these instances induce prohibitively large SOS_p bases, which hinders the computation of strong bounds. To solve this, we require a more sophisticated method for choosing a smaller, manageable, basis, such as $SO{S}_s^{\theta }$. Second, these instances can possess clauses of length k, where $k\ge 4$. This is problematic in the current settings because $F_{\varphi }$ (see (13)) is a kth degree polynomial, which requires a large basis to be represented. One possible way to overcome these challenges is through exploiting the structure present in these instances. For example, function $F_{\varphi }$ might have few nonzero coefficients, which allows for finding SOS decompositions with small monomial bases, using methods proposed in Wang et al. (2021); see also Ahmadi et al. (2017).