Exploiting Unit Propagation to Compute Lower Bounds in Branch and Bound Max-SAT Solvers
Issue date
2005Suggested 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.
Metadata
Show full item recordAbstract
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.