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.