Doctor's Theses (authored and supervised):
"BDD-based Dynamic Programming on Tree Decompositions - Towards an Alternative Approach for Efficient (QBF) Solving";
Supervisor, Reviewer: L. Pulina, M. Seidl, S. Woltran;
Institut fuer Informationssysteme,
oral examination: 2017-09-22.
Solving computationally hard problems efficiently is a challenging task in computer science. One approach to tackle such problems is to consider structural properties of the input. Many problems become tractable in case certain parameters of the input are assumed to be fixed. In this work we consider treewidth that, roughly speaking, captures the ``tree-likeness" of a graph. It is motivated by the observation that many problems are easier to be solved on trees than they are on arbitrary graphs. Treewidth as a parameter is oftentimes exploited by dynamic programming on a tree decomposition of the original input. Usually, dynamic programming relies on tables for storing intermediate results obtained during the tree decomposition traversal. However, a bottleneck of such table-based algorithms is relatively high memory consumption. In this work we study Binary Decision Diagrams (BDDs) as a suitable data structure for storing intermediate results. Instead of tables where the information is explicitly enumerated, BDDs allow for an implicit storage of this information. In the first part of this thesis we consider several well-known NP-complete problems that are fixed-parameter tractable with respect to treewidth. The presented dynamic programming algorithms are specified on a logical level and can be directly executed on the underlying BDD data structure. We then extend our approach to Quantified Boolean Formula (QBF) solving. Since the corresponding decision problem (QSAT) is PSPACE-complete, we require additional machinery. Our data structure is extended to nestings of BDDs, which account for quantifier alternations in the QBF instance. This yields an alternative technique for expansion-based QBF solving that explicitly takes the structure of QBF instances in prenex conjunctive normal form (PCNF) into account. While structure in the CNF is considered by the tree decomposition, structure in the quantifier prefix is handled by integrating dependency schemes. Towards efficiency in practice, we present optimizations such as clause splitting, feature-based tree decomposition selection, variable caching and (extended) subsumption checking. The considered optimizations may also be suitable for future developments in the area of dynamic programming on tree decompositions. The presented algorithms are implemented in the QBF solver dynQBF. We provide an exhaustive experimental evaluation of dynQBF that shows the impact of the developed optimizations. Furthermore, we compare the performance of dynQBF to state-of-the-art solvers. The evaluation reveals that our system is competitive on instances with one quantifier alternation. Additionally, we show that our approach appears to be orthogonal to existing techniques, with a large number of uniquely solved instances.
BDD-based; Dynamic; Programming;Tree; Decompositions; Towards; Alternative; Approach;Efficient; QBF; Solving;
Created from the Publication Database of the Vienna University of Technology.