LP2PB: Translating Answer Set Programs into Pseudo-Boolean Theories
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.
Code (1)
Similar Papers 제목 키워드 기반
Translating LPOD and CR-Prolog2 into Standard Answer Set Programs
Logic Programs with Ordered Disjunction (LPOD) is an extension of standard answer set programs to handle preference using the construct of ordered disjunction, and CR-Prolog2 is an extension of standard answer set progra…
Pseudo-Boolean d-DNNF Compilation for Expressive Feature Modeling Constructs
Configurable systems typically consist of reusable assets that have dependencies between each other. To specify such dependencies, feature models are commonly used. As feature models in practice are often complex, automa…
Inconsistency Proofs for ASP: The ASP-DRUPE Format
Answer Set Programming (ASP) solvers are highly-tuned and complex procedures that implicitly solve the consistency problem, i.e., deciding whether a logic program admits an answer set. Verifying whether a claimed answer …
Leveraging Large Language Models to Generate Answer Set Programs
Large language models (LLMs), such as GPT-3 and GPT-4, have demonstrated exceptional performance in various natural language processing tasks and have shown the ability to solve certain reasoning problems. However, their…
Formal LogicIn-Context LearningNeural logic programs and neural nets
Neural-symbolic integration aims to combine the connectionist subsymbolic with the logical symbolic approach to artificial intelligence. In this paper, we first define the answer set semantics of (boolean) neural nets an…