Detecting Disjoint Inconsistent Subformulas for Computing Lower Bounds for Max-SAT

Abstract

Many lower bound computation methods for branch and bound Max-SAT solvers can be explained as procedures that search for disjoint inconsistent subformulas in the Max-SAT instance under consideration. The difference among them is the technique used to detect inconsistencies. In this paper, we define five new lower bound computation methods: two of them are based on detecting inconsistencies via a unit propagation procedure that propagates unit clauses using an original ordering; the other three add an additional level of forward look-ahead based on detecting failed literals. Finally, we provide empirical evidence that the new lower bounds are of better quality than the existing lower bounds, as well as that a solver with our new lower bounds greatly outperforms some of the best performing state-of-the-art Max-SAT solvers on Max-2SAT, Max-3SAT, and Max-Cut instances.