On Solving MAX-SAT Using Sum of Squares
Lennart Sinjorgo (l.m.sinjorgo@tilburguniversity.edu) and
Renata Sotirov (r.sotirov@tilburguniversity.edu)
Additional contact information
Lennart Sinjorgo: CentER, Department of Econometrics and Operations Research, Tilburg University, 5037 AB Tilburg, Netherlands
Renata Sotirov: CentER, Department of Econometrics and Operations Research, Tilburg University, 5037 AB Tilburg, Netherlands
INFORMS Journal on Computing, 2024, vol. 36, issue 2, 417-433
Abstract:
We consider semidefinite programming (SDP) approaches for solving the maximum satisfiability (MAX-SAT) problem and weighted partial MAX-SAT. It is widely known that SDP is well-suited to approximate (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-and-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 MAX-SAT and derive several properties of monomial bases used in the SOS approach. We connect two well-known SDP approaches for (MAX)-SAT in an elegant way. Moreover, we relate our SOS-SDP relaxations for partial MAX-SAT to the known SAT relaxations.
Keywords: SAT; MAX-SAT; weighted partial MAX-SAT; semidefinite programming; sum of squares; Peaceman–Rachford splitting method (search for similar items in EconPapers)
Date: 2024
References: Add references at CitEc
Citations:
Downloads: (external link)
http://dx.doi.org/10.1287/ijoc.2023.0036 (application/pdf)
Related works:
This item may be available elsewhere in EconPapers: Search for items with the same title.
Export reference: BibTeX
RIS (EndNote, ProCite, RefMan)
HTML/Text
Persistent link: https://EconPapers.repec.org/RePEc:inm:orijoc:v:36:y:2024:i:2:p:417-433
Access Statistics for this article
More articles in INFORMS Journal on Computing from INFORMS Contact information at EDIRC.
Bibliographic data for series maintained by Chris Asher (casher@informs.org).