Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
Conflict-driven answer set solving: from theory to practice
Gebser M., Kaufmann B., Schaub T. Artificial Intelligence187-188 52-89,2012.Type:Article
Date Reviewed: Nov 29 2012

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.

Reviewer:  K. Balogh Review #: CR140701 (1303-0246)
Bookmark and Share
Models Of Computation (F.1.1 )
Complexity Measures And Classes (F.1.3 )
Model Development (I.6.5 )
Simulation And Modeling (I.6 )
Would you recommend this review?
Other reviews under "Models Of Computation": Date
Brains, machines, and mathematics (2nd ed.)
Arbib M., Springer-Verlag New York, Inc., New York, NY, 1987. Type: Book (9789780387965390)
Sep 1 1988
Communication and concurrency
Milner R., Prentice-Hall, Inc., Upper Saddle River, NJ, 1989. Type: Book (9780131150072)
Jan 1 1990
The social metaphor for distributed processing
Stark W., Kotin L. Journal of Parallel and Distributed Computing 7(1): 125-147, 1989. Type: Article
Dec 1 1990

E-Mail This Printer-Friendly
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright 1999-2024 ThinkLoud®
Terms of Use
| Privacy Policy