LP2PB: Translating Answer Set Programs into Pseudo-Boolean Theories

Wolf De Wulf, Bart Bogaerts

Research output: Chapter in Book/Report/Conference proceedingConference paperResearch


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 succeßful 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.

Original languageEnglish
Title of host publicationProceedings 36th International Conference on Logic Programming
Subtitle of host publication(Technical Communications)
PublisherOpen Publishing Association
Publication statusPublished - 2020
EventThe 36th International Conference on Logic Programming
- Rende, Italy
Duration: 18 Sep 202025 Sep 2020
Conference number: 36

Publication series

NameElectronic Proceedings in Theoretical Computer Science
PublisherOpen Publishing Association
ISSN (Print)2075-2180
ISSN (Electronic)2075-2180


ConferenceThe 36th International Conference on Logic Programming
Abbreviated titleICLP2020
Internet address

Fingerprint Dive into the research topics of 'LP2PB: Translating Answer Set Programs into Pseudo-Boolean Theories'. Together they form a unique fingerprint.

Cite this