2002 | OriginalPaper | Buchkapitel
Bridging the Gap between SAT and CSP
verfasst von : Carlos Ansótegui, Felip Manyà
Erschienen in: Principles and Practice of Constraint Programming - CP 2002
Verlag: Springer Berlin Heidelberg
Enthalten in: Professional Book Archive
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
Our research program is aimed at bridging the gap between propositional satisfiability encodings and constraint satisfaction formalisms. The challenge is to combine the inherent efficiencies of SAT solvers operating on uniform satisfiability encodings with the much more compact and natural representations, and more sophisticated propagation techniques of CSP formalisms. Our research objective is to define a new language —MV-SAT— that incorporates the best characteristics of the existing many-valued languages [1,2], as well as to develop fast MV-SAT solvers. MV-SAT is formally defined as the problem of deciding the satisfiability of MV-formulas. An MV-formula is a classical propositional conjunctive clause form based on a generalized notion of literal, called MV-literal. Given a domain T (|T| ≥ 2) equipped with a total ordering ≤, an MV-literal is an expression of the form S: p, where p is a propositional variable and S is a subset of T which is of the form {i}, ↑ i = {j ∈ T | j ≥ i}, or ↓ i = {j ∈ T | j ≤ i} for some i ∈ T. The informal meaning of S: p is “p is constrained to the values in S”.