|Títol||Detecting Disjoint Inconsistent Subformulas for Computing Lower Bounds for Max-SAT|
|Publication Type||Conference Paper|
|Year of Publication||2006|
|Authors||Li CMin, Manyà F, Planes J.|
|Conference Name||Proceedings of the 21st National Conference on Artificial Intelligence, AAAI-2006, Boston/MA, USA|
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.
- Quant a IIIA