Solving Over-Constrained Problems with SAT Technology

Argelich Romà, Josep; Manyà Serres, Felip

doi:https://doi.org/10.1007/11499107_1

View/Open

Postprint (182.8Kb)

Issue date

2005

Author

Argelich Romà, Josep

Manyà Serres, Felip

Suggested 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.

Abstract

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).

URI

http://hdl.handle.net/10459.1/57269

DOI

https://doi.org/10.1007/11499107_1

Is part of

Lecture Notes in Computer Science, 2005, vol. 3569, p. 1-15