Answer set programming (ASP) uses declarative programming to target difficult (primarily nondeterministic polynomial time (NP)-complete) search problems, for which stable models are computed. Beside its theoretical importance, ASP and satisfiability (SAT) checking have been successfully applied to problems in electronic circuit design, software verification, molecular biology, constraint solving in artificial intelligence, and operations research, among others.
The title of the paper reflects in a precise and modest way the main theme: the proposal of an efficient method and its implementation for ASP.
The authors are well-known experts in the field. They selected the existing conflict-driven clause learning (CDCL) method (known to be successful in SAT checking), and refined it for efficient ASP evaluation. As is usually done in ASP and SAT checking, the authors focus mainly on normal propositional conjunctive normal form (CNF) formulas and, in particular, on solving the decision problem of answer set existence. They present their conflict-driven algorithm for ASP solving in terms of nogoods. Beyond this aim, their implemented system, called clasp, supports extended rules, solution enumeration, and optimization. Formal properties of their method are shown, and its soundness and completeness are proven.
Clasp has been implemented in a direct, native way, so the method is very efficient, ranking among the most successful systems in contests such as the Coalition for Academic Scientific Computation (CASC), the Mancoosi International Solver Competition (MISC), and the Pseudo Boolean Competition (PB), as well as other ASP and SAT solver contests, since 2007. Clasp is a “central component of the Potassco tool suite and has already been used in various applications [in] diverse areas.”
I recommend this paper both for researchers and for programmers looking to apply ASP and SAT solvers.