[Back]

G. Charwat, S. Woltran:
"BDD-based Dynamic Programming on Tree Decompositions";
Report No. DBAI-TR-2016-95, DBAI, 2016; 47 pages.

Dynamic programming on tree decompositions is a well-studied approach for solving computationally hard problems efficiently - given that the input exhibits small treewidth. Usually, implementations rely on tables for storing information, and algorithms specify how tuples are manipulated during traversal of the decomposition. However, a bottleneck of such table-based algorithms is relatively high memory consumption. Binary Decision Diagrams (BDDs) and related concepts have been shown to be very well suited to store information efficiently. In this report we illustrate BDD-based dynamic programming on tree decompositions. We first show algorithms for several well-known NP-complete problems that are fixed-parameter tractable w.r.t treewidth. These algorithms are specified on a logical level in form of set-based formula manipulation operations that are executed directly 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. The data structure is extended to nestings of BDDs, which account for quantifier alternations of the QBF instance. Additionally, several algorithm optimizations, including heuristic data structure compression, delayed variable removal and intermediate unsatisfiability checks, are introduced. We develop the prototypical QBF solver dynQBF, that shows to be useful in practice for instances with few quantifier alternations and where the treewidth of the propositional formula does not exceed 50. Compared to state-of-the-art solvers, our system performs well on 2-QBF instances, and we even identify classes of instances that are uniquely solved by dynQBF.

Project Head Stefan Woltran:
START