Anzeige
Erschienen in:
2005 | OriginalPaper | Buchkapitel
SAT-Based Decision Procedures for Automated Reasoning: A Unifying Perspective
verfasst von : Alessandro Armando, Claudio Castellini, Enrico Giunchiglia, Fausto Giunchiglia, Armando Tacchella
Erschienen in: Mechanizing Mathematical Reasoning
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
Propositional reasoning (SAT) is an essential part of many reasoning tasks. Many problems in computer science can be compiled to SAT and then effectively decided using state-of-the-art solvers. Alternatively, if reduction to SAT is not feasible, the ideas and technology of state-of-the-art SAT solvers can be useful in deciding the propositional component of the reasoning task being considered. This last approach has been used in different contexts by different authors, many times by authors of this paper. Because of the essential role played by the SAT solver, these decision procedures have been called “SAT-based”. SAT-based decision procedures have been proposed for various logics, but also in other areas such as planning. In this paper we present a unifying perspective on the various SAT-based approaches to these different reasoning tasks.