2023/02/14 by Sinjorgo, Lennart, Sotirov, Renata · 1 citation
#90C09 #90C22 #90C23 #FOS: Mathematics #Optimization and Control (math.OC)
paper · doi:10.48550/arxiv.2302.06931
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.