Exploiting Unit Propagation to Compute Lower Bounds in Branch and Bound Max-SAT Solvers
MetadataShow full item record
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 ofLecture Notes in Computer Science, 2005, vol. 3709, p. 403-414
European research projects
Showing items related by title, author, creator and subject.
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 ...
Argelich Romà, Josep; Li, Chu-Min; Manyà Serres, Felip; Planes Cid, Jordi (Springer Verlag, 2011)The MaxSAT Evaluation  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, ...
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 ...