[Back]

T. Eiter, M. Hecher, R. Kiesel:
"Treewidth-Aware Cycle Breaking for Algebraic Answer Set Counting.";
Talk: KR 2021 - 18th International Conference on Principles of Knowledge Representation and Reasoning, virtual event; 2021-11-03 - 2021-11-12; in: "Proceedings of the 18th International Conference on Principles of Knowledge Representation and Reasoning, KR 2021, Online event, November 3-12, 2021", (2021), 269 - 279.

Probabilistic reasoning, parameter learning, and most probable explanation inference for answer set programming have recently received growing attention. They are only some of the problems that can be formulated as Algebraic Answer Set Counting (AASC) problems. The latter are however hard to solve, and efficient evaluation techniques are needed. Inspired by Vlasser et al.'s Tp-compilation (JAR, 2016), we introduce Tp-unfolding, which employs forward reasoning to break the cycles in the positive dependency graph of a program by unfolding them. Tp-unfolding is defined for any normal answer set program and unfolds programs with respect to unfolding sequences, which are akin to elimination orders in SAT-solving. Using "good" unfolding sequences, we can ensure that the increase of the treewidth of the unfolded program is small. Treewidth is a measure adhering to a program's tree-likeness, which gives performance guarantees for AASC. We give sufficient conditions for the existence of good unfolding sequences based on the novel notion of component-boosted backdoor size, which measures the cyclicity of the positive dependencies in a program. The experimental evaluation of a prototype implementation, the AASC solver aspmc, shows promising results.

Probabilistisches Schließen, Parameterlernen und Inferenz der wahrscheinlichsten Erklärung für die Programmierung von Antwortmengen haben in letzter Zeit immer mehr Aufmerksamkeit erhalten. Dies sind nur einige der Probleme, die als Algebraic Answer Set Counting (AASC) Probleme formuliert werden können. Letztere sind jedoch schwer zu lösen, und es werden effiziente Auswertungstechniken benötigt. Inspiriert von der Tp-Kompilierung von Vlasser et al. (JAR, 2016), führen wir die Tp-Entfaltung ein, die Forward Reasoning einsetzt, um die Zyklen im positiven Abhängigkeitsgraphen eines Programms zu brechen, indem sie entfaltet werden. Die Tp-Entfaltung ist für jedes Programm mit normaler Antwortmenge definiert und entfaltet Programme unter Berücksichtigung von Entfaltungssequenzen, die mit Eliminationsreihenfolgen beim SAT-Lösen vergleichbar sind. Mit "guten" Entfaltungssequenzen können wir sicherstellen, dass die Zunahme der Baumbreite des entfalteten Programms klein ist. Treewidth ist ein Maß für die Baumähnlichkeit eines Programms, das Leistungsgarantien für AASC bietet. Wir geben hinreichende Bedingungen für die Existenz guter Entfaltungssequenzen an, die auf dem neuartigen Begriff der komponentenverstärkten Backdoor-Größe basieren, die die Zyklizität der positiven Abhängigkeiten in einem Programm misst. Die experimentelle Auswertung einer Prototyp-Implementierung, des AASC-Lösers aspmc, zeigt vielversprechende Ergebnisse.

ASP, Model Counting, Treewidth, Semiring

https://publik.tuwien.ac.at/files/publik_302170.pdf

Project Head Stefan Szeider:
DK - Logic

Project Head Stefan Woltran:
HYPAR

Project Head Stefan Woltran:
START