[Back]

F. Slivovsky:
"Structure in #SAT and QBF";
Supervisor, Reviewer: S. Szeider, H. Chen; Institut für Computergraphik und Algorithmen, 2015; oral examination: 2015-05-05.

Computational problems that are intractable in general can often be efficiently resolved in practice due to latent structure in real-world instances. This thesis considers structural properties that can be used in the design of more efficient algorithms for two highly intractable problems: the satisfiability problem of quantified Boolean formulas (QSAT) and propositional model counting (#SAT). QSAT. The nesting of existential and universal quantifiers in quantified Boolean formulas (QBFs) generates dependencies among variables that have to be respected by QSAT solvers. In standard decision algorithms, it is assumed that all possible variable dependencies exist. But often, only a fraction of these dependencies is realized, while the remaining, "spurious" dependencies lead to unnecessary restrictions that inhibit solver performance. We study dependency schemes as a means to identifying spurious dependencies and establish the following results. * Among dependency schemes considered in the literature, the resolution-path dependency scheme identifies a maximal set of spurious dependencies. We prove that the resolution-path dependency scheme can be computed in polynomial time. * We state sufficient conditions for the sound deployment of dependency schemes in search-based QSAT solvers and prove that these conditions are met by several dependency schemes, including those implemented in the solver DepQBF and a variant of the resolution-path dependency scheme. * We show that known dependency schemes support a reordering operation that is more powerful than quantifier shifting, and present an application to the reduction of quantifier alternations of a QBF. #SAT. The model counting problem (#SAT) asks for the number of satisfying assignments of a propositional formula in conjunctive normal form. This problem is hard even for classes that admit satisfiability testing in polynomial time, such as Horn or 2CNF formulas. We prove the following results on the complexity of #SAT with respect to structural parameters based on graph width measures, identifying new classes of formulas amenable to efficient model counting. * Contraction of modules in a graph is a commonly used preprocessing step in combinatorial optimization. We define the modular treewidth of a graph as its treewidth after contraction of modules, and prove that #SAT is polynomial-time tractable for classes of formulas with incidence graphs of bounded modular treewidth. * Symmetric clique-width is a graph parameter that generalizes treewidth as well as modular treewidth. We show that #SAT is polynomial-time tractable for classes of formulas with incidence graphs of bounded symmetric clique-width.

In der Komplexitätstheorie geht man davon aus, dass für zahlreiche zentrale Probleme keine effizienten Algorithmen existieren. Einige dieser Probleme lassen sich in der Praxis dennoch lösen, was üblicherweise damit begründet wird, dass praxisrelevante Instanzen "Struktur" aufweisen, die von Lösungsverfahren ausgenutzt werden kann. Die vorliegende Arbeit untersucht konkrete Ausprägungen dieses Strukturbegriffs für zwei äußerst schwierige Probleme: das Erfüllbarkeitsproblem quantifizierter boolescher Formeln (QSAT) und das Abzählproblem von Modellen aussagenlogischer Formeln (#SAT). QSAT. Die Alternierung von Existenz- und Allquantoren im Präfix quantifizierter boolescher Formeln erzeugt Abhängigkeiten unter Variablen, die von Lösungsverfahren für QSAT berücksichtigt werden müssen. Gängige Verfahren gehen davon aus, dass alle prinzipiell möglichen Abhängigkeiten tatsächlich bestehen. Oft ist jedoch nur ein Bruchteil dieser Abhängigkeiten triftig, während die übrigen, "falschen" Abhängigkeiten lediglich zu unnötigen Einschränkungen führen. Wir untersuchen Dependency Schemes als Mittel zur Identifikation solcher falscher Abhängigkeiten, mit folgenden Resultaten. * Wir zeigen, dass das Resolution-Path Dependency Scheme in Polynomialzeit berechnet werden kann. Unter den derzeit bekannten Dependency Schemes erkennt das Resolution-Path Dependency Scheme eine maximale Menge falscher Abhängigkeiten. * Wir definieren notwendige und hinreichende Bedingungen für den Einsatz von Dependency Schemes in suchbasierten Algorithmen für QSAT und zeigen, dass diese Bedingungen von den in DepQBF implementierten Dependency Schemes sowie einer Variante des Resolution-Path Dependency Schemes erfüllt werden. * Dependency Schemes waren ursprünglich zum Verschieben von Quantoren im Präfix quantifizierter boolescher Formeln gedacht. Wir zeigen, dass gängige Dependency Schemes eine allgemeinere Operation zur Manipulation des Präfixes erlauben, und demonstrieren, wie diese Operation zur Minimierung der Alternierungstiefe von Formeln verwendet werden kann. #SAT. Das Zählen von Modellen aussagenlogischer Formeln ist nicht nur im Allgemeinen schwer, sondern selbst für Formelklassen, für die das zugehörige Entscheidungsproblem in Polynomialzeit gelöst werden kann, beispielsweise für Horn- oder 2CNF-Formeln. Wir untersuchen den Effekt von strukturellen (über Graphenparameter definierten) Einschränkungen auf die Komplexität von #SAT und bestimmen neue Formelklassen, die das Zählen von Modellen in Polynomialzeit erlauben. * Das Kontrahieren von Modulen in Graphen ist eine gängige Technik zur Vereinfachung kombinatorischer Optimierungsprobleme. Wir definieren die modulare Baumweite eines Graphen als seine Baumweite nach dem Kontrahieren von Modulen und zeigen, dass #SAT für Formeln, deren Inzidenzgraphen beschränkte modulare Baumweite haben, in Polynomialzeit gelöst werden kann. * Die symmetrische Cliquenweite ist ein Parameter, der sowohl Baumweite als auch modulare Baumweite verallgemeinert. Wir zeigen, dass #SAT für Formelklassen, deren Inzidenzgraphen beschränkte symmetrische Cliquenweite aufweisen, in Polynomialzeit lösbar ist.

http://publik.tuwien.ac.at/files/PubDat_247771.pdf