Solving Over-Constrained Problems with SAT Technology

View/ Open
Issue date
2005Suggested citation
Argelich Romà, Josep;
Manyà Serres, Felip;
.
(2005)
.
Solving Over-Constrained Problems with SAT Technology.
Lecture Notes in Computer Science, 2005, vol. 3569, p. 1-15.
https://doi.org/10.1007/11499107_1.
Metadata
Show full item recordAbstract
We present a new generic problem solving approach for overconstrained
problems based on Max-SAT. We first define a clausal form
formalism 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; the first one incorporates
static variable selection heuristics while the second one incorporates dynamic
variable selection heuristics. Finally, we present an experimental
investigation to assess the performance of our approach on a representative
sample of instances (random 2-SAT, Max-CSP, and graph coloring).
Is part of
Lecture Notes in Computer Science, 2005, vol. 3569, p. 1-15European research projects
Related items
Showing items related by title, author, creator and subject.
-
Modelling Max-CSP as Partial Max-SAT
Argelich Romà, Josep; Cabiscol i Teixidó, Alba; Lynce, Inês; Manyà Serres, Felip (Springer Verlag, 2008)We define a number of original encodings that map MaxCSP instances into partial Max-SAT instances. Our encodings rely on the well-known direct and support encodings from CSP into SAT. Then, we report on an experimental ... -
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, ...