New Inference Rules for Max-SAT

Visualitza/ Obre
Data de publicació
2007Citació recomanada
Li, Chu-Min;
Manyà Serres, Felip;
Planes Cid, Jordi;
.
(2007)
.
New Inference Rules for Max-SAT.
Journal of Artificial Intelligence Research, 2007, vol. 30, p. 321-359.
https://doi.org/10.1613/jair.2215.
Metadades
Mostra el registre d'unitat completResum
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 but, unfortunately, solving the Max-SAT
problem for the simplified formula is not equivalent to solving it for the original formula.
In this paper, we define a number of original inference rules that, besides being applied
efficiently, transform Max-SAT instances into equivalent Max-SAT instances which are
easier to solve. The soundness of the rules, that can be seen as refinements of unit resolution
adapted to Max-SAT, are proved in a novel and simple way via an integer programming
transformation. With the aim of finding out how powerful the inference rules are in practice,
we have developed a new Max-SAT solver, called MaxSatz, which incorporates those rules,
and performed an experimental investigation. The results provide empirical evidence that
MaxSatz is very competitive, at least, on random Max-2SAT, random Max-3SAT, MaxCut,
and Graph 3-coloring instances, as well as on the benchmarks from the Max-SAT
Evaluation 2006.
És part de
Journal of Artificial Intelligence Research, 2007, vol. 30, p. 321-359Projectes de recerca europeus
Publicacions relacionades
Mostrant elements relacionats per títol, autor i matèria.
-
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, ... -
Exploiting Unit Propagation to Compute Lower Bounds in Branch and Bound Max-SAT Solvers
Li, Chu-Min; Manyà Serres, Felip; Planes Cid, Jordi (Springer Verlag, 2005)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, ...