Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
Search
Conflict-driven answer set solving: from theory to practice
Gebser M., Kaufmann B., Schaub T.  Artificial Intelligence 187-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?
yes
no
Other reviews under "Models Of Computation": Date
Turing’s revolution: the impact of his ideas about computability
Sommaruga G., Strahm T.,  Birkhäuser Basel, New York, NY, 2016. 329 pp. Type: Book (978-3-319221-55-7)
Aug 23 2016
  Jul 15 2016
Uncertainty quantification: theory, implementation, and applications
Smith R.,  SIAM, Philadelphia, PA, 2013. 401 pp. Type: Book (978-1-611973-21-1)
May 20 2016
more...

E-Mail This Printer-Friendly
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright © 2000-2017 ThinkLoud, Inc.
Terms of Use
| Privacy Policy