Conflict-driven answer set solving: From theory to practice
- We introduce an approach to computing answer sets of logic programs, based on concepts successfully applied in Satisfiability (SAT) checking. The idea is to view inferences in Answer Set Programming (ASP) as unit propagation on nogoods. This provides us with a uniform constraint-based framework capturing diverse inferences encountered in ASP solving. Moreover, our approach allows us to apply advanced solving techniques from the area of SAT. As a result, we present the first full-fledged algorithmic framework for native conflict-driven ASP solving. Our approach is implemented in the ASP solver clasp that has demonstrated its competitiveness and versatility by winning first places at various solver contests.
Verfasserangaben: | Martin GebserORCiD, Benjamin KaufmannGND, Torsten SchaubORCiDGND |
---|---|
DOI: | https://doi.org/10.1016/j.artint.2012.04.001 |
ISSN: | 0004-3702 |
Titel des übergeordneten Werks (Englisch): | Artificial intelligence |
Verlag: | Elsevier |
Verlagsort: | Amsterdam |
Publikationstyp: | Wissenschaftlicher Artikel |
Sprache: | Englisch |
Jahr der Erstveröffentlichung: | 2012 |
Erscheinungsjahr: | 2012 |
Datum der Freischaltung: | 26.03.2017 |
Freies Schlagwort / Tag: | Answer set programming; Logic programming; Nonmonotonic reasoning |
Band: | 187 |
Ausgabe: | 8 |
Seitenanzahl: | 38 |
Erste Seite: | 52 |
Letzte Seite: | 89 |
Fördernde Institution: | German Science Foundation (DFG) [SCHA 550/8-1, SCHA 550/8-2] |
Organisationseinheiten: | Mathematisch-Naturwissenschaftliche Fakultät / Institut für Informatik und Computational Science |
Peer Review: | Referiert |
Name der Einrichtung zum Zeitpunkt der Publikation: | Mathematisch-Naturwissenschaftliche Fakultät / Institut für Informatik |