Anzeige
Erschienen in:
2005 | OriginalPaper | Buchkapitel
Solving Over-Constrained Problems with SAT
verfasst von : Josep Argelich, Felip Manyà
Erschienen in: Principles and Practice of Constraint Programming - CP 2005
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
We have defined a new formalism, based on Max-SAT, for encoding and solving over-constrained problems. Our formalism is an extension of Boolean CNF formulas in which we deal with blocks of Boolean clauses instead of dealing with individual clauses. Every block, formed by a set of clauses, is declared either as a hard block (i.e., must be satisfied by any solution) or as a soft block (i.e., can be violated by some solution). The idea behind the notion of block is that it encodes a problem constraint (for example, adjacent vertices have different colors); in general, it is not enough a single clause to encode a problem constraint. We call
soft CNF formulas
to this new kind of formulas.