|
|
Logic Programming Systems
The Conflict-Driven Answer Set Solver clasp
System Web Page: http://potassco.sourceforge.net PDF: Here The clasp system combines the high-level modeling capacities of Answer Set Programming (ASP; [1]) with state-of-the-art techniques from the area of Boolean constraint solving. clasp is designed and optimized for conflict-driven ASP solving [2,3]; it is freely available at http://potassco.sourceforge.net. Given the proximity of ASP to Satisfiability Checking (SAT), clasp can also deal with formulas in CNF via an additional DIMACS front-end. As such, it can be viewed as a chaff-type Boolean constraint solver [4], encompassing
For supporting the high-level modeling capacities of ASP, clasp offers special Boolean constraint techniques for dealing with
Special mention deserves the detection of unfounded sets [7], aiming at small and "loop-encompassing" rather than greatest unfounded sets, as done traditionally. Meanwhile, clasp has been extended in several ways.
References[1] Baral, C.: Knowledge Representation, Reasoning and Declarative Problem Solving. Cambridge University Press (2003)[2] Gebser, M., Kaufmann, B., Neumann, A., Schaub, T.: Conflict-driven answer set solving. In Veloso, M., ed.: Proceedings of the Twentieth International Joint Conference on Artificial Intelligence (IJCAI'07), AAAI Press/The MIT Press (2007) 386--392. [3] Gebser, M., Kaufmann, B., Neumann, A., Schaub, T.: clasp: A conflict-driven answer set solver. [11], 260--265 [4] Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.:Chaff: Engineering an efficient SAT solver. In: Proceedings of the Thirty-eighth Conference on Design Automation (DAC'01), ACM Press (2001) 530--535 [5] Gebser, M., Kaufmann, B., Neumann, A., Schaub, T.: Conflict-driven answer set enumeration. \newblock [11], 136--148 [6] Gebser, M., Kaufmann, B., Neumann, A., Schaub, T.: Advanced preprocessing for answer set solving. In Ghallab, M., Spyropoulos, C., Fakotakis, N., Avouris, N., eds.: Proceedings of the Eighteenth European Conference on Artificial Intelligence (ECAI'08), IOS Press (2008) 15--19 [7] Anger, C., Gebser, M., Schaub, T.: Approaching the core of unfounded sets.In Dix, J., Hunter, A., eds.: Proceedings of the Eleventh International Workshop on Nonmonotonic Reasoning (NMR'06). Number IFI-06-04 in Technical Report Series, Clausthal University of Technology, Institute for Informatics (2006) 58--66 [8] Drescher, C., Gebser, M., Grote, T., Kaufmann, B., König, A., Ostrowski, M., Schaub, T.: Conflict-driven disjunctive answer set solving.In Brewka, G., Lang, J., eds.: Proceedings of the Eleventh International Conference on Principles of Knowledge Representation and Reasoning (KR'08), AAAI Press (2008) 422--432 [9] Gebser, M., Schaub, T., Thiele, S.: GrinGo: A new grounder for answer set programming. [11], 266--271 [10] Gebser, M., Kaminski, R., Kaufmann, B., Ostrowski, M., Schaub, T., Thiele, S.: Engineering an incremental ASP solver. In Garcia de la Banda, M., Pontelli, E., eds.: Proceedings of the Twenty-fourth International Conference on Logic Programming (ICLP'08). Volume 5366 of Lecture Notes in Computer Science., Springer-Verlag (2008) To appear. [11] Baral, C., Brewka, G., Schlipf, J., eds.:Proceedings of the Ninth International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR'07). Volume 4483 of Lecture Notes in Artificial Intelligence., Springer-Verlag (2007). * Affiliated with Simon Fraser University, Canada, and Griffith University, Australia. |