Exploiting Unit Propagation to Compute Lower Bounds in Branch and Bound Max-SAT Solvers

Li, Chu-Min; Manyà Serres, Felip; Planes Cid, Jordi

doi:https://doi.org/10.1007/11564751_31

View/Open

007814.pdf (219.8Kb)
Sol·licita una còpia

Issue date

2005

Author

Li, Chu-Min

Manyà Serres, Felip

Planes Cid, Jordi

Suggested citation

Li, Chu-Min; Manyà Serres, Felip; Planes Cid, Jordi; . (2005) . Exploiting Unit Propagation to Compute Lower Bounds in Branch and Bound Max-SAT Solvers. Lecture Notes in Computer Science, 2005, vol. 3709, p. 403-414. https://doi.org/10.1007/11564751_31.

Abstract

One of the main differences between complete SAT solvers and exact Max-SAT solvers is that the former make an intensive use of unit propagation at each node of the proof tree while the latter, in order to ensure optimality, can only apply unit propagation to a restricted number of nodes. In this

paper, we describe a branch and bound MaxSAT solver that applies unit propagation at each node of the proof tree to compute the lower bound instead of applying unit propagation to simplify the formula. The new lower bound captures the lower bound based on inconsistency counts that apply most of the state-of-the-art Max-SAT solvers as well as other improvements, like the start rule, that have been defined to get a lower bound of better quality. Moreover, our solver incorporates the Jeroslow-Wang variable selection heuristic, the pure literal and dominating unit clause rules, and novel preprocessing techniques. The experimental investigation we conducted to compare our solver with the most modern Max-SAT solvers provides experimental evidence that our solver is very competitive.

URI

http://hdl.handle.net/10459.1/57574

DOI

https://doi.org/10.1007/11564751_31

Is part of

Lecture Notes in Computer Science, 2005, vol. 3709, p. 403-414