Conflict-driven answer set solving 论文

摘要

We introduce a new approach to computing answer sets of logic programs, based on concepts from constraint processing (CSP) and satisfiability checking (SAT). The idea is to view inferences in answer set programming (ASP) as unit propagation on nogoods. This provides us with a uniform constraintbased framework for the different kinds of inferences in ASP. It also allows us to apply advanced techniques from the areas of CSP and SAT. We have implemented our approach in the new ASP solver clasp. Our experiments show that the approach is competitive with state-of-the-art ASP solvers. 1