作者: 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.