Zahlreiche schwere algorithmische Probleme, die im Bereich der formalen Verifikation von Hard- und Software oder bei der automatischen Lösung von Planungsaufgaben auftreten, können effizient in das Erfüllbarkeitsproblem Quantifizierter Boolscher Formeln (QBF) übersetzt werden. Dieses Projekt erforscht neue Methoden zur Nutzung von Unabhängigkeit zwischen Variablen für QBF. Durch die Verschachtelung von Existenz- und Allquantoren in quantifizerten Boolschen Formeln können Abhängigkeiten zwischen Variablen entstehen, die das Übertragen erfolgreicher Techniken zur Lösung des Erfüllbarkeitsproblems aussagenlogischer Formeln (SAT) auf QBF erschweren. In manchen Fällen kann sich eine vermeintliche Abhängigkeit als rein syntaktisch entpuppen und festgestellt werden, dass die entsprechenden Variablen in Wirklichkeit voneinander unabhängig sind. Diese Information kann wiederum dazu genutzt werden, Entscheidungsprozeduren für QBF zu beschleunigen. Im Allgemeinen kann allerdings nicht effizient entschieden werden, ob Variablen einer quantifizierten Boolschen Formel voneinander unabhängig sind oder nicht.

Dieses Forschungsprojekt verfolgt drei Ziele: (A) die Weiterentwicklung existierender Techniken zur Ermittlung von Unabhängigkeit zwischen Variablen durch das Erforschen deren theoretischer Grundlagen sowie durch die Entwicklung verbesserter Algorithmen; (B) die Entdeckung neuer Verfahren zur Ermittlung und Nutzung von Unabhängigkeit zwischen Variablen; (C) die Verallgemeinerung dieser Methoden auf Probleme jenseits von QBF.