Variablenabha¿ngigkeiten Quantifizierter Boolscher Formeln

01.06.2015 - 31.05.2018
Forschungsförderungsprojekt

 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.

Personen

Projektleiter_in

Institut

Förderungsmittel

  • Fonds zur Förderung der wissenschaftlichen Forschung (FWF) (Nationale Förderung) Förderschiene Einzelprojekt Förderprogramm Fonds zur Förderung der wissenschaftlichen Forschung (FWF) Fördergeber Forschungsförderungsgesellschaft Reichweite Nationale Förderung Projekttyp Forschungsförderungsprojekt Ausschreibungskennung P 27721-N25

Forschungsschwerpunkte

  • Information and Communication Technology

Schlagwörter

DeutschEnglisch
Boole'sche FormelnQuantified Boolean Formulas
QBF certificationQBF certification
QBF resolutionQBF resolution
DQBFDQBF