Development of High-Performance Systems for Model-based Problem Solving via Answer Set Programming
Final Report Abstract
Answer Set Programming has become a popular declarative problem solving paradigm, in which a problem is expressed as a logic program so that the program’s models, called stable models, provide solutions to the original problem. The combination of a rich yet simple modeling language with flexible reasoning modes, such as solution enumeration and optimization, has led to a growing use of ASP in various domains. The overall project has contributed to this success by the development of high-performance solving technology that supports the full expressiveness of ASP and renders it attractive for real-world applications. The project has initiated and coined the theory and resulting technology of conflict-driven ASP solving. To this end, and based on a constraint-based characterization of stable models, it introduced a computational approach to ASP solving that associates fundamental inferences in ASP with Boolean constraints that can be analyzed upon conflicts. This led to the design and implementation of different parallel ASP solving strategies and diverse forms of complex reasoning that are indispensable for addressing demanding applications. The key publications are very well cited and the project, also dubbed Potassco, has become an international renowned icon for cutting edge ASP solving technology, as reflected by a world-wide community in science as well as industry. The six most cited publication of our project unite more than 1500 citations, the projects software was downloaded at sourceforge more than 160,000 times, not counting packages directly distributed for Macintosh, Linux, and Windows computers. The systems, in particular, the multi-threaded ASP solver clasp, have won international solving competitions in several areas, notably in Satisfiability Testing. They have also attracted the interest of several companies. Perhaps the most prestigious application of clasp was its usage by the US department FCC to control the US wide auction of radio and mobile frequencies that is estimated to save the US government 20-40 Billion US dollars. This increasing industrial interest also motives our license change from GPL to MIT that will be issued with the next release.
Publications
- Advanced Conflict-Driven Disjunctive Answer Set Solving. Proceedings of the Twenty-third International Joint Conference on Artificial Intelligence (IJCAI’13)
M. Gebser, B. Kaufmann, and T. Schaub
- Domain-specific Heuristics in Answer Set Programming. Proceedings of the Twenty-Seventh National Conference on Artificial Intelligence (AAAI’13)
M. Gebser, B. Kaufmann, R. Otero, J. Romero, T. Schaub, and P. Wanko
- claspfolio 2: Advances in Algorithm Selection for Answer Set Programming. Theory and Practice of Logic Programming, 2014
H. Hoos, M. Lindauer (born Schneider), and T. Schaub
- aspeed: Solver Scheduling via Answer Set Programming. Theory and Practice of Logic Programming, 2015
H. Hoos, R. Kaminski, M. Lindauer, and T. Schaub
- Progress in clasp Series 3. Proceedings of the Thirteenth International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR’15)
M. Gebser, R. Kaminski, B. Kaufmann, J. Romero, and T. Schaub
(See online at https://doi.org/10.1007/978-3-319-23264-5_31) - Answer Set Programming Modulo Acyclicity. Fundamenta Informaticae, 2016
J. Bomanson, M. Gebser, T. Janhunen, B. Kaufmann, and T. Schaub
(See online at https://doi.org/10.3233/FI-2016-1398)
