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 prop- agation procedure that propagates unit clauses using an orig- inal ordering; the other three add an additional level of for- ward 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.

• Tagged
• XML
• BibTex