BDD-based dynamic programming on tree decompositions : towards an alternative approach for efficient QBF solving

Abstract

Ein wesentliches Forschungsgebiet der Informatik beschäftigt sich mit der Entwicklung effizienter Algorithmen zum Lösen von schwer berechenbaren Problemen. Vielversprechend in diesem Bereich ist die Analyse der Struktur der gegebenen Daten. Viele Probleme sind leichter zu lösen, wenn gewisse Parameter der Daten als konstant angenommen werden. In dieser Arbeit beschäftigen wir uns mit dem Parameter Baumweite, der beschreibt, wie sehr ein Graph einem Baum ähnelt: Viele Probleme sind leichter auf Bäumen zu lösen, als sie es auf allgemeinen Graphen wären. Algorithmen, die Baumweite ausnutzen, basieren meist auf Dynamischer Programmierung über Baumzerlegungen. Aktuelle Implementierungen verwenden für gewöhnlich Tabellen um Zwischenergebnisse abzuspeichern. Eine Schwachstelle stellt allerdings der meinst hohe Speicherbedarf dar. Binäre Entscheidungsdiagramme (BEDs) bieten eine Möglichkeit, den Speicherbedarf zu reduzieren. Während die Zwischenergebnisse in Tabellen normalerweise explizit repräsentiert werden, können diese in BEDs implizit dargestellt werden. Im ersten Teil dieser Arbeit betrachten wir einige klassische NP-vollständige Probleme, welche, parametrisiert mit Baumweite, effizient lösbar sind (sie sind fixed-parameter tractable). Wir kodieren die vorgestellten Algorithmen in Propositionaler Logik, womit diese direkt auf den BEDs ausgeführt werden können. Im Verlauf der Arbeit entwickeln wir einen neuen Lösungsansatz für Quantifizierte Boolesche Formeln (QBFs). Nachdem das entsprechende Entscheidungsproblem (QSAT) PSPACE-vollständig ist, sind hier BEDs alleine nicht mehr ausreichend. Wir erweitern die verwendete Datenstruktur zu verschachtelten Mengen von BEDs. Die Verschachtelungen dienen dazu, Quantorenalternierungen abzubilden. Unser Algorithmus basiert auf Expansion von Variablen. Wir betrachten Instanzen in PKNF, die aus einem Quantorenpräfix (P) sowie einem quantorenfreien Teil in konjunktiver Normalform (KNF) bestehen. Struktur in der KNF Formel wird durch die verwendete Baumzerlegung gehandhabt, während Struktur im Präfix mittels Integration von Abhängigkeitsschemata (dependency schemes) beachtet wird. In der Praxis sind allerdings weitere Optimierungen notwendig: Dies inkludiert Zerlegung von Klauseln, Auswahl der verwendeten Baumzerlegung auf Basis von Eigenschaften, welche über Baumweite hinausgehen, Caching von Variablen, sowie Redundanzvermeidung in unserer Datenstruktur. Diese Optimierungen könnten auch in zukünftigen praktischen Realisierungen von Dynamischer Programmierung auf Baumzerlegungen Anwendung finden. Die vorgestellten Ansätze wurden im System dynQBF implementiert. In einer umfangreichen experimentellen Analyse zeigen wir, wie sich unsere Optimierungen auf die Laufzeit auswirken. Weiters vergleichen wir dynQBF mit aktuellen Systemen zum Lösen von QBFs. Unsere Experimente belegen, dass sich dynQBF auf Instanzen mit einer Quantorenalternierung kompetitiv verhält. Außerdem beobachten wir, dass eine größere Anzahl der Instanzen von dynQBF als einziges System gelöst werden kann. Dies unterstreicht, dass unser Ansatz tatsächlich eine neuartige Möglichkeit bietet, um QBFs zu lösen.

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.