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.
Is part of
Lecture Notes in Computer Science, 2005, vol. 3709, p. 403-414European research projects
Related items
Showing items related by title, author, creator and subject.
-
The first and second Max-SAT evaluations
Argelich Romà, Josep; Li, Chu-Min; Manyà Serres, Felip; Planes Cid, Jordi (IOS Press, 2008)We describe the organization and report on the results of the First and Second Max-SAT Evaluations, which were organized as affiliated events of the 2006 and 2007 editions of the International Conference on Theory and ... -
Analyzing the instances of the MaxSAT evaluation
Argelich Romà, Josep; Li, Chu-Min; Manyà Serres, Felip; Planes Cid, Jordi (Springer Verlag, 2011)The MaxSAT Evaluation [1] is an affiliated event of the SAT Conference that is held every year since 2006, and is devoted to empirically evaluate exact MaxSAT algorithms solving any of the following problems: MaxSAT, ... -
New Inference Rules for Max-SAT
Li, Chu-Min; Manyà Serres, Felip; Planes Cid, Jordi (Association for the Advancement of Artificial Intelligence, 2007)Exact Max-SAT solvers, compared with SAT solvers, apply little inference at each node of the proof tree. Commonly used SAT inference rules like unit propagation produce a simplified formula that preserves satisfiability ...