On solving the MAX-SAT using sum of squares

TL;DR

This paper explores semidefinite programming, especially sum of squares methods, for solving MAX-SAT problems, demonstrating competitive performance and theoretical guarantees beyond traditional 2-SAT applications.

Contribution

It introduces a novel SOS-based SDP approach for MAX-SAT, combining theoretical insights with practical solver implementation that competes in MAX-SAT competitions.

Findings

SDP approaches are competitive with top MAX-SAT solvers

A family of SDP relaxations provides rank two guarantees

Connections established between different SDP methods for MAX-SAT

Abstract

We consider semidefinite programming (SDP) approaches for solving the maximum satisfiability problem (MAX-SAT) and the weighted partial MAX-SAT. It is widely known that SDP is well-suited to approximate the (MAX-)2-SAT. Our work shows the potential of SDP also for other satisfiability problems, by being competitive with some of the best solvers in the yearly MAX-SAT competition. Our solver combines sum of squares (SOS) based SDP bounds and an efficient parser within a branch & bound scheme. On the theoretical side, we propose a family of semidefinite feasibility problems, and show that a member of this family provides the rank two guarantee. We also provide a parametric family of semidefinite relaxations for the MAX-SAT, and derive several properties of monomial bases used in the SOS approach. We connect two well-known SDP approaches for the (MAX)-SAT, in an elegant way. Moreover, we relate our SOS-SDP relaxations for the partial MAX-SAT to the known SAT relaxations.