Answer Set Solving exploiting Treewidth and its Limits
Markus Hecher

TL;DR
This paper explores the use of treewidth-based parameterized algorithms to solve Answer Set Programming problems efficiently, introduces a framework for projected model counting, and establishes lower bounds on algorithm improvements.
Contribution
It presents novel algorithms exploiting treewidth for ASP, extends to projected model counting, and introduces a methodology for proving lower bounds on runtime improvements.
Findings
Algorithms for ASP leveraging treewidth are competitive in counting answer sets.
Framework for projected model counting applies to ASP, argumentation, and higher polynomial hierarchy problems.
Most worst-case runtimes of the proposed algorithms cannot be significantly improved under standard complexity assumptions.
Abstract
Parameterized algorithms have been subject to extensive research of recent years and allow to solve hard problems by exploiting a parameter of the corresponding problem instances. There, one goal is to devise algorithms, where the runtime is exponential exclusively in this parameter. One particular well-studied structural parameter is treewidth. Typically, a parameterized algorithm utilizing treewidth takes or computes a tree decomposition, which is an arrangement of a graph into a tree, and evaluates the problem in parts by dynamic programming on the tree decomposition. In our research, we want to exploit treewidth in the context of Answer Set Programming (ASP), a declarative modeling and solving framework, which has been successfully applied in several application domains and industries for years. So far, we presented algorithms for ASP for the full ASP-Core-2 syntax, which is…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, Reasoning, and Knowledge · Multi-Agent Systems and Negotiation · Formal Methods in Verification
Answer Set Solving exploiting Treewidth and its Limits††thanks: This work has been supported by Austrian Science Fund (FWF): Y698.
The author is also affiliated with the University of Potsdam, Germany.
Markus Hecher
TU Wien, Austria, [email protected]
Abstract
Parameterized algorithms have been subject to extensive research of recent years and allow to solve hard problems by exploiting a parameter of the corresponding problem instances. There, one goal is to devise algorithms, where the runtime is exponential exclusively in this parameter. One particular well-studied structural parameter is treewidth. Typically, a parameterized algorithm utilizing treewidth takes or computes a tree decomposition, which is an arrangement of a graph into a tree, and evaluates the problem in parts by dynamic programming on the tree decomposition. In our research, we want to exploit treewidth in the context of Answer Set Programming (ASP), a declarative modeling and solving framework, which has been successfully applied in several application domains and industries for years. So far, we presented algorithms for ASP for the full ASP-Core-2 syntax, which is competitive especially when it comes to counting answer sets. Since dynamic programming on tree decomposition lands itself well to counting, we designed a framework for projected model counting, which applies to ASP, abstract argumentation and even to problems higher in the polynomial hierarchy. Given standard assumptions in computational complexity, we established a novel methodology for showing lower bounds, and we showed that most worst-case runtimes of our algorithms cannot be significantly improved.
1 Introduction
Parameterized algorithms [6] have attracted considerable interest in recent years and allow to solve hard combinatorial problems by utilizing a certain parameter of the problem instance. Of particular interest is to devise algorithms, where the runtime is polynomial and additionally depends on some computable function in the parameter. One structural and extensively studied parameter is treewidth [2, 22]. Intuitively, treewidth measures the closeness of a graph to a tree based on the observation that problems on trees are often easier than on arbitrary graphs. A (parameterized) algorithm utilizing treewidth typically solves problem instances by dynamic programming (DP). Thereby it takes a tree decomposition, which is an arrangement of a graph (representation) of the given problem instance into a tree, and then evaluates the problem in parts. Such dynamic programming algorithms are then sensitive to treewidth, which provides an upper bound on the worst-case runtime needed for each tree decomposition node of an (optimal) tree decomposition. However, in practice, solvers based on this idea can produce results for certain problems [5, 20] up to treewidth 80. Further, there are observations that instances relevant for certain applications and different problems sometimes have small treewidth. One particular problem, for which dynamic programming algorithms on tree decompositions were investigated [18] is Answer Set Programming. Answer Set Programming (ASP) [3] is a logic-based declarative modeling language and problem solving framework where selected models, the answer sets, of a given ASP program directly represent the solutions to the modeled problem. ASP has been applied in several application domains, which accelerates the search for alternative solving methods. This raises then the question whether exploiting structural parameters, e.g., treewidth, improves the performance of evaluation of ASP programs, which forms the topic of the thesis. Jakl et al. [18] established a DP algorithm for disjunctive ASP that is linear in the size of the (ground) ASP program, but double exponential in the treewidth of a certain graph representing of the program. There is an implementation called DynASP solver [21] that adheres to this idea. In our work [10, 11], we presented an evaluation of extended ASP programs based on the full ASP-Core-2 [4] syntax. Further, we also showed that the double exponential runtime in the treewidth can not be avoided for ASP in general, unless the widely believed exponential time hypothesis (ETH) fails. This result is based on our novel methodology [14] for showing such lower bounds for problems even higher in the polynomial hierarchy. Currently, we are investigating hybrid parameterized solving techniques for ASP, where we aim to improve solving by a combination of both monolithic and parameterized solvers.
2 Background
Tree Decompositions. Tree decompositions are built for a given graph and are a tree-like representation of the graph. These tree decompositions are trees consisting of nodes, where each node contains certain vertices of the given graph. The so-called width of a given tree decomposition corresponds to the largest number of vertices that is contained in one node (minus one). The parameter treewidth captures the “tree-likeness” of the given graph and corresponds to the smallest width among all tree decompositions for the graph. The treewidth intuitively reveals, how hard the given graph is when solving a certain problem. The smaller the treewidth of a given graph, the more “tree-like” the graph and thus typically easier to solve problems on the graph. In particular, the treewidth of a graph that is a tree corresponds to one.
Dynamic Programming. Tree decompositions allow to tackle hard problems by evaluating a certain problem-dependent graph representation of a problem instance in parts, thereby being sensitive to the treewidth of the instance. This evaluation is done by means of dynamic programming (on the tree decomposition), where the tree decomposition is traversed in post-order, and each tree decomposition node reflects a certain part of the problem instance. During the traversal, one stores intermediate results in a table for each node. Thereby, each node uses and transforms intermediate results of its child nodes and computes solutions to the corresponding problem part for the node. The dynamic programming algorithm relies on properties of the tree decomposition in order to ensure that a non-empty table for the root node guarantees that a problem solution was found. Using this exact idea, one can also define algorithms to enumerate and count solutions. The runtime of these dynamic programming algorithms is polynomial in the instance size, but additionally depends on a function for some computable function , where is the parameter treewidth. If the parameter is reasonably small, such an algorithm could outperform classical ASP solvers, which require exponential runtime in the instance size in the worst-case. Since might be exponential, we aim at classification of problems according to the function that is required to solve the problem using parameter treewidth. These lower bounds are typically dependent on the widely believed exponential time hypothesis (ETH), which implies that there is no algorithm for Boolean satisfiability (SAT) such that satisfiability of a given formula with variables can be decided in time .
Answer Set Programming (ASP). ASP is a rule-based modeling and problem solving framework, where rules can contain (first-order) variables, which are instantiated by the grounder. The grounder is responsible for producing a (ground) ASP program, which is a set of rules obtained by eliminating variables of a given non-ground program. Modern grounders parse non-ground programs that adhere to the ASP-Core-2 [4] syntax and output (among others) ground programs in SModels intermediate format [4, 17]. The main interest of this research proposal concerns the solving, i.e., how to efficiently evaluate an ASP program.
3 Research
First, we discuss the goals of the thesis. Then, we provide a detailed description of achievements and the lessons learned so far. Finally, we give an outlook about ongoing and future work.
3.1 Goals
The thesis shall address and achieve the following main goals.
- •
Design ASP solving algorithms and techniques that utilize the structural parameter treewidth in order to efficiently solve ASP-Core-2 programs. These algorithms shall be extended to problem variants and extensions later.
- •
Implement these ideas in a solver and compete against other ASP solvers and the related DynASP system.
- •
Investigate the theoretical limitations that any of these solvers can not evade given reasonable assumptions in computational complexity. The thereby obtained results might depend on certain fragments of ASP and could be crucial to further improve the solver.
- •
Generalize and apply these findings in a broader, general context. Especially applications in artificial intelligence might benefit from the outcome of this research. In this regard also other structural parameters could be considered.
3.2 Achieved Results
First of all, we established dynamic programming algorithms [10] for decision and counting problems related to ASP111These algorithms were later also generalized to the formalism of default logic [15]. using the full ASP-Core-2 syntax. Thereby we adapted the existing DynASP solver [21] resulting in the DynASP2 system. This covers interoperation with state-of-the-art grounders, and handling of the SModels intermediate format including also optimization statements. The new system DynASP2 conceptually follows the approach of the original implementation, where tree decomposition(s) of a certain graph representation of a given ground program are prepared222Later we also investigated the more general approach of fractional hypertree decompositions [8], which could be relevant for ASP as well.. The resulting tree decomposition is then traversed in a bottom-up manner (using post-order traversals) to evaluate the program. We implemented several variants of such algorithms, based on the input program’s graph representation. One such graph representation is the primal graph representation, where atoms are vertices, and atoms appearing together in a rule have an edge between them. Further, we also investigated algorithms based on the incidence graph representation, where atoms and rules are vertices, and when an atom appears in a rule there is an edge between them. Then, we improved the whole approach, where we presented dynamic programming algorithms that rely on multiple passes (where the tree decomposition is traversed multiple times). This new approach of traversing in multiple passes, which extends an existing work on two passes [1], allows then to improve existing data structures of DynASP2. In particular, one can benefit from early pruning of data after each traversal, which then allows for efficient solving in practice [11], given dedicated data structures that heavily rely on preventing redundancy using pointers. Given ASP programs of small treewidth, DynASP2 proved to be competitive in the setting of model counting, a central problem in areas like machine learning, statistics, probabilistic reasoning and combinatorics. When counting answer sets, our approach conceptually has a big advantage: it does not require to materialize the full answer sets in order to count them. This ensures huge speed-ups against classical ASP systems like clasp [17]. However, our implementation was also able to beat existing SAT model counters. Benchmarks indicate that the performance of model counting using a popular fragment of quantified boolean formulas with quantifier depth two (2-QBFs) is competitive as well.
Model counting proved to be a rather successful application of dynamic programming on tree decompositions, since it lands itself well to parallelization. Indeed, using a novel approach on modern graphics computing units (GPUs), we were able to compete existing model counters in a comprehensive benchmark evaluation using all known state-of-the-art systems for model counting of SAT formulas and weighted variants. We recently improved the resulting system gpusat [16] by a new architecture involving data compression, dedicated data structures, optimized counters and customized tree decompositions.
Later, we generalized our algorithms to projected model counting, where models that are identical with respect to a given set of projection variables, i.e., when “projected” to these projection variables, count as one (projected) model. To this end, we designed an algorithm [12] that works in multiple passes for SAT. The idea was to propose one dynamic programming algorithm that relies on previous passes that solve the base (decision) problem according to certain conditions. Then, this algorithm takes the results of the previous passes and performs projected counting on top of it. Unfortunately, the algorithm might exponentially increase (in the treewidth) the results of the previous passes in the worst case. As an example, although SAT can be solved in single-exponential runtime in the treewidth (while still being polynomial in the instance size), projected model counting on SAT requires double-exponential runtime in the treewidth using our algorithm. However, we also considered the exponential time hypothesis (ETH), a standard assumption in computational complexity. Our results reveal that if one assumes ETH, one cannot significantly improve the worst-case runtime of this problem. We also generalized our results of projected model counting to abstract argumentation [9] and ASP [7, 13], where we provided algorithms and lower bounds based on ETH for fragments of ASP (for decision, counting and projected model counting problems). Some of these lower bounds were achieved by relying on our recent generalization of a result for 2-QBFs to arbitrary QBFs, which provides a novel methodology for lower bounds of problems located higher in the polynomial hierarchy [14].
3.3 Current and Future Work
Given our recent dynamic programming algorithms [13] that utilize treewidth for certain fragments of ASP, we consider an implementation, which will be added to DynASP. Especially in the context of hybrid parameterized solving, which aims at the interplay between existing monolithic solvers (e.g., clasp) and approaches based on exploiting (structural) parameters, there is still room for improvement. There are already existing systems of this kind, e.g., dynqbf [5], which is capable of deciding validity of QBFs up to treewidth 80 with this idea. Since DynASP can be used up to treewidth 14, and existing reductions from ASP to QBF seem to fail for dynqbf, one might consider a new implementation DynASP3, which provides the best of monolithic solving (e.g., clasp) and parameterized solving (e.g., DynASP2).
At the moment I am focusing on an efficient implementation of our algorithm for projected model counting, since it seems that the mentioned worst-case result does not reflect the average case. In particular, I am evaluating the prospect of a potential implementation targeted on alternative hardware, e.g., GPUs, and potential strategies towards projected model counting solvers for ASP. This new type of hardware raises interesting questions concerning alternative data structures and methods to exploit parallelism efficiently.
Further, we are permanently improving on our methodology [14] for lower bounds, and the idea is to provide a catalog of simple, alternative proofs based on our methodology for existing lower bounds for treewidth under ETH. It is for example still open, whether our methodology can be applied to easily show lower bounds that are called slightly superexponential [19] (in the treewidth), which is between single- and double-exponential.
- [1]
B. Bliem, G. Charwat, M. Hecher, and S. Woltran.
D-FLAT: Subset Minimization in Dynamic Programming on Tree Decompositions Made Easy.
Fundam. Inform., 147(1):27–61, 2016.
- [2]
H. L. Bodlaender and A. M. Koster.
Combinatorial optimization on graphs of bounded treewidth.
Comput. J., 51(3):255–269, 2008.
- [3]
G. Brewka, T. Eiter, and M. Truszczyński.
Answer set programming at a glance.
Commun. ACM, 54(12):92–103, 2011.
- [4]
F. Calimeri, W. Faber, M. Gebser, G. Ianni, R. Kaminski, T. Krennwallner, N. Leone, F. Ricca, and T. Schaub.
ASP-core-2 input language format, 2013.
- [5]
G. Charwat and S. Woltran.
Expansion-based QBF solving on tree decompositions.
Accepted for publication in Fundamenta Informaticae. To appear, 2019.
- [6]
M. Cygan, F. V. Fomin, Ł. Kowalik, D. Lokshtanov, D. Marx, M. Pilipczuk, M. Pilipczuk, and S. Saurabh.
Parameterized Algorithms.
Springer, 2015.
- [7]
J. K. Fichte and M. Hecher.
Exploiting treewidth for counting projected answer sets.
In KR’18, pages 643–644. The AAAI Press, 2018.
Extended abstract.
- [8]
J. K. Fichte, M. Hecher, N. Lodha, and S. Szeider.
An SMT approach to fractional hypertree width.
In CP’18, volume 11008 of LNCS, pages 109–127. Springer, 2018.
- [9]
J. K. Fichte, M. Hecher, and A. Meier.
Counting complexity for reasoning in abstract argumentation.
Accepted for publication at AAAI’19. The paper is available at https://tinyurl.com/ybr6upbd.
- [10]
J. K. Fichte, M. Hecher, M. Morak, and S. Woltran.
Answer set solving with bounded treewidth revisited.
In LPNMR’17, volume 10377 of LNCS, pages 132–145. Springer, 2017.
- [11]
J. K. Fichte, M. Hecher, M. Morak, and S. Woltran.
DynASP2.5: Dynamic programming on tree decompositions in action.
In IPEC’17, volume 89 of LIPIcs, pages 17:1–17:13. Dagstuhl Publishing, 2017.
- [12]
J. K. Fichte, M. Hecher, M. Morak, and S. Woltran.
Exploiting treewidth for projected model counting and its limits.
In SAT’18, volume 10929 of LNCS, pages 165–184. Springer, 2018.
- [13]
J. K. Fichte, M. Hecher, M. Morak, and S. Woltran.
Answer set solving with bounded treewidth revisited.
Accepted for publication at LPNMR’19. The paper is available at https://tinyurl.com/y6gkrblc.
- [14]
J. K. Fichte, M. Hecher, and A. Pfandler.
TE-ETH: Lower Bounds for QBFs of Bounded Treewidth.
Under review. Preliminary version available at https://tinyurl.com/y7wnvu6w.
- [15]
J. K. Fichte, M. Hecher, and I. Schindler.
Default Logic and Bounded Treewidth.
In LATA’18, volume 10792 of LNCS, pages 130–142. Springer, 2018.
- [16]
J. K. Fichte, M. Hecher, S. Woltran, and M. Zisser.
Weighted Model Counting on the GPU by Exploiting Small Treewidth.
In ESA’18, volume 112 of LIPIcs, pages 28:1–28:16. Dagstuhl Publishing, 2018.
- [17]
M. Gebser, R. Kaminski, B. Kaufmann, and T. Schaub.
Answer Set Solving in Practice.
Synthesis Lectures on Artificial Intelligence and Machine Learning. Morgan & Claypool Publishers, 2012.
- [18]
M. Jakl, R. Pichler, and S. Woltran.
Answer-set programming with bounded treewidth.
In IJCAI’09, volume 2, pages 816–822. The AAAI Press, 2009.
- [19]
D. Lokshtanov, D. Marx, and S. Saurabh.
Slightly superexponential parameterized problems.
In SODA’11, pages 760–776. SIAM, 2011.
- [20]
F. Lonsing and U. Egly.
Evaluating QBF solvers: Quantifier alternations matter.
In CP’18, volume 11008 of LNCS, pages 276–294. Springer, 2018.
- [21]
M. Morak, N. Musliu, R. Pichler, S. Rümmele, and S. Woltran.
A new tree-decomposition based algorithm for answer set programming.
In ICTAI’11, pages 916–918. IEEE Computer Society, 2011.
- [22]
N. Robertson and P. Seymour.
Graph minors. II. Algorithmic aspects of tree-width.
J. Algorithms, 7(3):309–322, 1986.
The reference list from the paper itself. Each links out to its DOI / PubMed record.
- 1[1] B. Bliem, G. Charwat, M. Hecher, and S. Woltran. D-FLAT 2 2 {}^{\mbox{2}} : Subset Minimization in Dynamic Programming on Tree Decompositions Made Easy. Fundam. Inform. , 147(1):27–61, 2016.
- 2[2] H. L. Bodlaender and A. M. Koster. Combinatorial optimization on graphs of bounded treewidth. Comput. J. , 51(3):255–269, 2008.
- 3[3] G. Brewka, T. Eiter, and M. Truszczyński. Answer set programming at a glance. Commun. ACM , 54(12):92–103, 2011.
- 4[4] F. Calimeri, W. Faber, M. Gebser, G. Ianni, R. Kaminski, T. Krennwallner, N. Leone, F. Ricca, and T. Schaub. ASP-core-2 input language format, 2013.
- 5[5] G. Charwat and S. Woltran. Expansion-based QBF solving on tree decompositions. Accepted for publication in Fundamenta Informaticae. To appear, 2019.
- 6[6] M. Cygan, F. V. Fomin, Ł. Kowalik, D. Lokshtanov, D. Marx, M. Pilipczuk, M. Pilipczuk, and S. Saurabh. Parameterized Algorithms . Springer, 2015.
- 7[7] J. K. Fichte and M. Hecher. Exploiting treewidth for counting projected answer sets. In KR’18 , pages 643–644. The AAAI Press, 2018. Extended abstract.
- 8[8] J. K. Fichte, M. Hecher, N. Lodha, and S. Szeider. An SMT approach to fractional hypertree width. In CP’18 , volume 11008 of LNCS , pages 109–127. Springer, 2018.
