|
Notas:
|
We present a new generic problem solving approach for over-constrained problems
based on Max-SAT. We first define a Boolean clausal form formalism, called soft CNF
formulas, that deals with blocks of clauses instead of individual clauses, and that allows
one to declare each block either as hard (i.e., must be satisfied by any solution) or soft
(i.e., can be violated by some solution). We then present two Max-SAT solvers that find a
truth assignment that satisfies all the hard blocks of clauses and the maximum number of
soft blocks of clauses. Our solvers are branch and bound algorithms equipped with original
lazy data structures, powerful inference techniques, good quality lower bounds, and
original variable selection heuristics. Finally, we report an experimental investigation on a
representative sample of instances (random 2-SAT, Max-CSP, graph coloring, pigeon hole
and quasigroup completion) which provides experimental evidence that our approach is very
competitive compared with the state-of-the-art approaches developed in the CSP and SAT
communities.
Research partially supported by projects TIN2004-07933-C03-03 and TIC2003-00950 funded by the Ministerio de Educacion y Ciencia. The second author is supported by a grant Ramon y Cajal. |
