LP2PB: Translating Answer Set Programs into Pseudo-Boolean Theories

Wolf De Wulf; Bart Bogaerts

doi:10.4204/EPTCS.325.25

LP2PB: Translating Answer Set Programs into Pseudo-Boolean Theories

Research output: Chapter in Book/Report/Conference proceeding › Conference paper › Research

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 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 language	English
Title of host publication	Proceedings 36th International Conference on Logic Programming
Subtitle of host publication	(Technical Communications)
Publisher	Open Publishing Association
Pages	206-219
DOIs	https://doi.org/10.4204/EPTCS.325.25
Publication status	Published - 2020
Event	The 36th International Conference on Logic Programming - Rende, Italy Duration: 18 Sep 2020 → 25 Sep 2020 Conference number: 36 https://iclp2020.unical.it/

Publication series

Name	Electronic Proceedings in Theoretical Computer Science
Publisher	Open Publishing Association
Volume	325
ISSN (Print)	2075-2180
ISSN (Electronic)	2075-2180

Conference

Conference	The 36th International Conference on Logic Programming
Abbreviated title	ICLP2020
Country	Italy
City	Rende
Period	18/09/20 → 25/09/20
Internet address	https://iclp2020.unical.it/

Access to Document

10.4204/EPTCS.325.25

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

Cite this

@inproceedings{9f3ad09e16eb4226a8019a8967d8e448,

title = "LP2PB: Translating Answer Set Programs into Pseudo-Boolean Theories",

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 succe{\ss}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.",

author = "{De Wulf}, Wolf and Bart Bogaerts",

year = "2020",

doi = "10.4204/EPTCS.325.25",

language = "English",

series = "Electronic Proceedings in Theoretical Computer Science",

publisher = "Open Publishing Association",

pages = "206--219",

booktitle = "Proceedings 36th International Conference on Logic Programming",

}

De Wulf, W & Bogaerts, B 2020, LP2PB: Translating Answer Set Programs into Pseudo-Boolean Theories. in Proceedings 36th International Conference on Logic Programming: (Technical Communications). Electronic Proceedings in Theoretical Computer Science, vol. 325, Open Publishing Association, pp. 206-219, The 36th International Conference on Logic Programming
, Rende, Italy, 18/09/20. https://doi.org/10.4204/EPTCS.325.25

LP2PB: Translating Answer Set Programs into Pseudo-Boolean Theories. / De Wulf, Wolf; Bogaerts, Bart.

Proceedings 36th International Conference on Logic Programming: (Technical Communications). Open Publishing Association, 2020. p. 206-219 (Electronic Proceedings in Theoretical Computer Science; Vol. 325).

Research output: Chapter in Book/Report/Conference proceeding › Conference paper › Research

TY - GEN

T1 - LP2PB: Translating Answer Set Programs into Pseudo-Boolean Theories

AU - De Wulf, Wolf

AU - Bogaerts, Bart

PY - 2020

Y1 - 2020

N2 - 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.

AB - 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.

U2 - 10.4204/EPTCS.325.25

DO - 10.4204/EPTCS.325.25

M3 - Conference paper

T3 - Electronic Proceedings in Theoretical Computer Science

SP - 206

EP - 219

BT - Proceedings 36th International Conference on Logic Programming

PB - Open Publishing Association

ER -