LP2PB: Translating Answer Set Programs into Pseudo-Boolean Theories
arXiv:2009.10248 · doi:10.4204/EPTCS.325.25
Abstract
Answer set programming (ASP) is a well-established knowledge representation formalism. Most ASP solvers are based on (extensions of) technology from Boolean satisfiability solving. While these solvers have shown to be very successful in many practical applications, their strength is limited by their underlying proof system, resolution. In this paper, we present a new tool LP2PB that translates ASP programs into pseudo-Boolean theories, for which solvers based on the (stronger) cutting plane proof system exist. We evaluate our tool, and the potential of cutting-plane-based solving for ASP on traditional ASP benchmarks as well as benchmarks from pseudo-Boolean solving. Our results are mixed: overall, traditional ASP solvers still outperform our translational approach, but several benchmark families are identified where the balance shifts the other way, thereby suggesting that further investigation into a stronger proof system for ASP is valuable.
In Proceedings ICLP 2020, arXiv:2009.09158
References in corpus (7)
- The DLV System for Knowledge Representation and Reasoning
- ASP-Core-2 Input Language Format
- Predicate Logic as a Modeling Language: Modeling and Solving some Machine Learning and Data Mining Problems with IDP3
- The Seventh Answer Set Programming Competition: Design and Results
- Vicious Circle Principle and Logic Programs with Aggregates
- Properties and Applications of Programs with Monotone and Convex Constraints
- Optimizing Phylogenetic Supertrees Using Answer Set Programming