SUPRA: Erfüllbarkeit von Verallgemeinerungen des SAT-Problems

• Antragsteller: Professor Dr.-Ing. Christoph Scholl
• Fachliche Zuordnung: Sicherheit und Verlässlichkeit, Betriebs-, Kommunikations- und verteilte Systeme ; Rechnerarchitektur, eingebettete und massiv parallele Systeme ; Theoretische Informatik
• Förderung: Förderung seit 2022
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 508508079

Das Projektziel ist die Weiterentwicklung von SAT-Solving zum Erfüllbarkeitstest aussagenlogischer Formeln über die Aussagenlogik hinaus. SAT-Solving ist mittlerweile eine ausgereifte Technologie mit hoher industrieller Relevanz und wird intensiv in den verschiedensten Anwendungsgebieten eingesetzt wie in der Künstlichen Intelligenz (KI), der elektronischen Entwurfsautomatisierung (EDA) und der (Hardware- und Software-)Verifikation.Motiviert durch Problemstellungen aus praktisch relevanten Anwendungen, deren natürliche und kompakte Formulierung erweiterte Formalismen erfordert, betrachten wir hier vier wesentliche Zusatzaspekte: Quantifizierung, partielle Information, Wahrscheinlichkeit und nicht-boolesche Wertebereiche.Wir untersuchen Quantifizierte Boolesche Formeln (QBFs) mit universellen und existentiellen Quantoren sowie Abhängigkeitsquantifizierte Boolesche Formeln (DQBFs), die eine existentielle Quantifizierung unter partieller Information erlauben.Hier befassen wir uns insbesondere mit offenen Fragestellungen bei der Zertifizierung, die durch zusätzliche Informationen (neben einer reinen Ja-/Nein-Antwort) eine Überprüfung der Solver-Antwort ermöglicht, ohne die Solverimplementierung zu betrachten.Da mehr und mehr Anwendungen probabilistisch geprägt sind, untersuchen wir darüber hinaus eine Erweiterung des SAT-Solving auf Stochastisches SAT (SSAT), das Erfüllbarkeits*wahrscheinlichkeiten* berechnet bzw. abschätzt.Unser Ziel in diesem Zusammenhang ist die Verbesserung der Effizienz bestehender prototypischer SSAT-Solver sowie die Integration von Zertifizierung. Die Kombination von Wahrscheinlichkeiten mit partieller Information führt zu einer darüber hinaus gehenden Erweiterung zu Dependency Stochastic SAT (DSSAT).Da viele Anwendungen (insbesondere bei der Analyse von Software und Hybriden Systemen) eine Erweiterung um verschiedene `Theorien' zur Behandlung nicht-Boolescher Wertebereiche erfordern, übertragen wir Ideen aus dem Entwurf moderner QBF- und DQBF-Solver in das Gebiet `SAT modulo Theories'.Zusammenfassend werden wir neue Konzepte, Algorithmen und Werkzeuge für verallgemeinerte Entscheidungsverfahren jenseits der Aussagenlogik entwickeln. Die folgenden realen Anwendungen in KI, EDA und Systemverifikation werden (unter anderem) von den entwickelten Werkzeugen profitieren:die Verifikation bestimmter Klassen unvollständiger digitaler Schaltungen, die Analyse von nicht-kooperativen Spielen mit unvollständiger Information, die Synthese von sicheren Controllern für diskrete und hybride Systeme, verschiedene KI-Planungsprobleme wie Multi-Agenten-Planung und probabilistische Planung,die formale Verifikation probabilistischer Designs (unter Berücksichtigung des zunehmend probabilistischen Verhaltens moderner Chiptechnologien bei fortschreitender Miniaturisierung), die Analyse von (dezentralen) teilweise beobachtbaren Markov-Entscheidungsprozessen (POMDPs und Dec-POMDPs) sowie die Analyse von Software-Security.

• DFG-Verfahren: Sachbeihilfen
• Internationaler Bezug: Taiwan
• Partnerorganisation: National Science and Technology Council (NSTC)
• Kooperationspartner: Professor Jie-Hong Roland Jiang, Ph.D.