Uni-Logo
English       Login
Rechnerarchitektur
        Startseite         |         Institut für Informatik         |         Technische Fakultät
 

Projekte

Lösen von abhängigkeitsquantifizierten Booleschen Formeln

Projektbeschreibung

Algorithmen für Boolesche Erfüllbarkeitsprobleme (SAT) werden heutzutage in zahlreichen Anwendungsgebieten der Informatik und der elektronischen Entwurfsautomatisierung mit großem Erfolg eingesetzt. Sie sind, um nur einige wenige zu erwähnen, von höchster Relevanz in der formalen Verifikation und im Test von Hard- und Software, z. B. beim Bounded Model Checking (BMC) und bei der automatischen Testmustergenerierung (ATPG). Sie werden jedoch auch im Bereich der künstlichen Intelligenz, z. B. im Planen, eingesetzt. Obwohl das Problem NP-vollständig ist, können moderne Algorithmen mit Formeln umgehen, die aus Hunderttausenden von Variablen und Millionen von Klauseln bestehen. Aus diesem Grund haben SAT-Verfahren große industrielle Relevanz erlangt; so verwenden die meisten bedeutenden Chiphersteller SAT-basierte Techniken, um Fehler in ihren Hardwareentwürfen zu finden. Neben Arbeiten zur weiteren Verbesserung der SAT-Verfahren konzentriert sich die aktuelle Forschung auf eine Erweiterung des SAT-Problems, sogenannte quantifizierte Boolesche Formeln (QBF). Die Lösung von QBF ist noch komplexer (das Problem ist PSPACE-vollständig); trotzdem haben moderne Lösungsverfahren enorme Fortschritte bei der Lösung praktisch relevanter Probleme gemacht, und hierdurch eine ernsthafte Möglichkeit geschaffen, um viele schwierige Probleme zu lösen. Eine Reihe von Problemen kann jedoch nicht auf natürliche Art und Weise als QBF codiert werden, sondern benötigt eine Verallgemeinerung davon. Beispiele sind die Realisierbarkeit von unvollständigen digitalen Schaltungen, die Analyse von nicht-kooperativen Spielen mit unvollständiger Information, bestimmte Bitvektor-Logiken und die Synthese sicherer Controller. Für eine natürliche und kompakte Formulierung benötigen sie sogenannte Henkin-Quantoren, die zu abhängigkeitsquantifizierten Booleschen Formeln (DQBF) führen. Mit DQBFs lassen sich beliebige Abhängigkeiten der existentiellen Variablen im Quantorenpräfix ausdrücken, während QBF auf lineare Abhängigkeiten beschränkt ist. Momentan schränkt der Mangel an effizienten DQBF-Verfahren deren Anwendbarkeit auf praktische Probleme stark ein. In diesem Projekt entwickeln und verbessern wir Lösungstechniken für DQBF. Eine zentrale Aufgabe ist es, deren Effizienz bzgl. Berechnungsaufwand und Speicherbedarf zu verbessern. Darüber hinaus ist es von besonderer Bedeutung, die Lösungsverfahren so zu erweitern, dass sie nicht nur die Erfüllbarkeit einer Formel entscheiden, sondern auch Zertifikate für die Erfüllbarkeit in Form von sogenannten Skolem-Funktionen berechnen. Skolem-Funktionen spielen eine bedeutende Rolle z. B. als Implementierung fehlender Schaltkreisteile in unvollständigen Schaltungen oder als Gewinnstrategien in Spielen. Um die Machbarkeit der entwickelten Techniken zu demonstrieren, wenden wir sie auf Probleminstanzen aus verschiedenen Anwendungsdomänen an.

Laufzeit

01.01.2016 bis 31.12.2017

Projektleitung

Bernd Becker

Ansprechpartner/in

Dr. Ralf Wimmer
Telefon:0761 - 203 8179

Finanzierung

Deutsche Forschungsgemeinschaft

Publikationen


Jahre: 2016

    2016

    Icon: top nach oben zur Jahresübersicht
    • Ralf Wimmer, Christoph Scholl, Karina Wimmer, Bernd Becker
      Dependency Schemes for DQBF
      2016 Proceedings of the 19th International Conference on Theory and Applications of Satisfiability Testing (SAT), Springer, Band: 9710, Seiten: 473 - 489
    • Karina Wimmer, Ralf Wimmer, Christoph Scholl, Bernd Becker
      Skolem Functions for DQBF
      2016 Int'l Symposium on Automated Technology for Verification and Analysis (ATVA) Proceedings of the 14th International Symposium on Automated Technology for Verification and Analysis (ATVA), Springer, Band: 9938, Seiten: 395 - 411
    • Karina Wimmer, Ralf Wimmer, Christoph Scholl, Bernd Becker
      Skolem Functions for DQBF (Extended Version)
      , 2016