Conflict-driven answer set solving: From theory to practice

作者: Martin Gebser , Benjamin Kaufmann , Torsten Schaub

DOI: 10.1016/J.ARTINT.2012.04.001

关键词:

摘要: We introduce an approach to computing answer sets of logic programs, based on concepts successfully applied in Satisfiability (SAT) checking. The idea is view inferences Answer Set Programming (ASP) as unit propagation nogoods. This provides us with a uniform constraint-based framework capturing diverse encountered ASP solving. Moreover, our allows apply advanced solving techniques from the area SAT. As result, we present first full-fledged algorithmic for native conflict-driven Our implemented solver clasp that has demonstrated its competitiveness and versatility by winning places at various contests.

参考文章(109)
Martin Gebser, Christian Anger, Torsten Schaub, Approaching the core of unfounded sets ,(2006)
Martin Gebser, Roland Kaminski, Benjamin Kaufmann, Torsten Schaub, Bettina Schnor, Cluster-based ASP solving with claspar international conference on logic programming. pp. 364- 369 ,(2011) , 10.1007/978-3-642-20895-9_42
Martin Gebser, Benjamin Kaufmann, Torsten Schaub, André Neumann, Advanced Preprocessing for Answer Set Solving european conference on artificial intelligence. ,vol. 178, pp. 15- 19 ,(2008) , 10.3233/978-1-58603-891-5-15
Olivier Roussel, Vasco Manquinho, None, Pseudo-Boolean and Cardinality Constraints Handbook of Satisfiability. pp. 695- 733 ,(2009) , 10.3233/978-1-58603-929-5-695
Gilles Audemard, Laurent Simon, Predicting learnt clauses quality in modern SAT solvers international joint conference on artificial intelligence. pp. 399- 404 ,(2009)
Tomi Janhunen, Ilkka Niemelä, Compact translations of non-disjunctive answer set programs to propositional clauses Logic programming, knowledge representation, and nonmonotonic reasoning. pp. 111- 130 ,(2011) , 10.1007/978-3-642-20832-4_8
Martin Gebser, Benjamin Kaufmann, Torsten Schaub, André Neumann, Conflict-driven answer set solving international joint conference on artificial intelligence. pp. 386- 392 ,(2007)
Joohyung Lee, A model-theoretic counterpart of loop formulas international joint conference on artificial intelligence. pp. 503- 508 ,(2005)
Ravi Palla, Tae-Won Kim, Joohyung Lee, Circumscriptive event calculus as answer set programming international joint conference on artificial intelligence. pp. 823- 829 ,(2009)
Joao Marques-Silva, Ines Lynce, Sharad Malik, Conflict-driven clause learning SAT solvers Handbook of Satisfiability. pp. 131- 153 ,(2009) , 10.3233/978-1-58603-929-5-131