Erfüllbarkeitsproblem der Aussagenlogik: : SAT-Solver können helfen

Von Dr. Anastasia-Maria Leventi-Peetz und Oliver Zendel, BSI, sowie Kai Weber und Werner Lennartz, inducto GmbH

Sicherheitskritische Software, die beispielsweise in der Luftfahrt, in kerntechnischen Anlagen, der Automobilindustrie und der Medizintechnik zum Einsatz kommt und nach strengsten Normen geprüft werden muss (z. B. DO-178B), wird automatisch mittels spezieller Software-Werkzeuge auf Basis von SAT-Solvern getestet. Diese Werkzeuge können Millionen Zeilen von Programmcode in Computersprachen in wenigen Stunden auf Fehler und Sicherheitslücken zuverlässig überprüfen. Heutige SAT-Solver können Probleme mit vielen Millionen Klauseln und mehreren hunderttausend Variablen in überschaubarer Zeit auf Multicore-Workstation-Computern lösen.

SAT-Solver im Einsatz

SAT-Solver sind vielseitige Werkzeuge und werden für die Lösung eines ganzen Spektrums von industriellen Anwendungen eingesetzt. Ihr Einsatzgebiet reicht von der routinemäßigen Verifikation der Richtigkeit von komplexen Eigenschaften, auch dynamisch während des Prozesses der automatisierten Hardware-Planung und -Produktion rekonfigurierbarer Schaltkreise, bis zur Schwachstellen- und Fehlersuche bei der automatisierten Quellcode-Analyse von komplexen und sicherheitsrelevanten Softwareprodukten (Model-Checkers, SMT-Tools, Theorem-Provers). Die Lösungseffizienz der SAT-Solver-Methoden bei der Bewältigung von komplizierten Problemen hat sich in den letzten zwei Jahrzehnten exponentiell entwickelt.

Dazu trägt auch die Tatsache bei, dass die effizientesten SAT-Solver als Open-Source-Werkzeuge entwickelt werden beziehungsweise als Sourcecode offen verfügbar sind. Algorithmische Verbesserungen werden über Veröffentlichungen in Fachzeitschriften anderen Entwicklern und Anwendern zur Diskussion gestellt. Auf diese Weise werden diverse Anregungen dafür ausgetauscht, wie die SAT-Solver auf Basis von umfangreichen intensiven praktischen Erfahrungen eines großen heterogenen Benutzerkreises, der unter unterschiedlichen Perspektiven die Nützlichkeit des Solvers testet, weiterentwickelt und erweitert werden können.

SAT-Solver im Wettbewerb

Viele dieser so entwickelten SAT-Solver nehmen regelmäßig am inzwischen renommierten internationalen SAT-Solver-Wettbewerb teil. Dabei handelt es sich um eine Veranstaltung, die von der jährlich stattfi ndenden „Internationalen Konferenz zur Theorie und Anwendung der Erfüllbarkeitsprüfung“ ausgerichtet wird. Dort werden zahlreiche Anwendungsfälle aus Industrie, Entwicklung und Forschung sowie seit Anfang 2000 aus der Kryptografie zusammengestellt, analysiert und kritisiert.

Die am Wettbewerb teilnehmenden SAT-Solver müssen in der Lage sein, anwendungsnahe Probleme aus den Bereichen Hardware-Verifikation, Software-Verifikation, Kryptoanalyse, Bioinformatik et cetera innerhalb einer begrenzten Rechenzeit lösen zu können, um sich für den Wettbewerb zu qualifizieren. Dort werden dann die Solver danach bewertet, wie zuverlässig und schnell sie die Zusammenstellung von Anwendungsfällen lösen können. Diese Wettbewerbsveranstaltungen mit Diskussionen unter Experten und Anwendern stärken den Austausch von Ideen weiter, motivieren neue Entwicklungen und untermauern das Vertrauen der Anwender in die Solver, deren Transparenz von Code und Leistung wie eine Art Qualitätssicherung am Ende jedem Interessierten offenliegen.

SAT-Solver und NP-Probleme

In der Informatik bezeichnet man ein Problem als NP-vollständig (vollständig für die Klasse der Probleme, die sich nichtdeterministisch in Polynomialzeit lösen lassen), wenn es zu den schwierigsten Problemen in der Klasse NP gehört, also sowohl in NP liegt als auch NP-schwer ist. Das Erfüllbarkeitsproblem als zuerst anerkanntes NP-vollständiges Problem ist auch der Kern einer großen Klasse von NP-vollständigen Problemen und spielt eine wichtige Rolle bei der Untersuchung von Systemen der künstlichen Intelligenz (KI). Die Mehrheit der Entscheidungs- und Optimierungsprobleme in der KI, der Wissensrepräsentation und der Entscheidungsbegründung sind notorisch schwer zu lösen und ihre Komplexität geht über NP hinaus. Trotz ihrer Widerspenstigkeit im klassischen Sinne lassen sich solche Probleme aus der Praxis einer Vielzahl von Bereichen überraschend effektiv mit Methoden lösen, die auf SAT- und Integer-Programming-Solvern basieren.

Schwierige Probleme aus der Mathematik, wie das 3700 Jahre alte Zahlenrätsel des „Pythagoreischen Tripels“, konnten von zwei Informatikern, Marjin Heule und Oliver Kullmann, mittels eines SAT-Solvers und eines Supercomputers im Jahr 2016 gelöst werden. Die Fragestellung lautete: Kann man die natürlichen Zahlen von 1 bis n in zwei Gruppen aufteilen, sodass keine von beiden ein pythagoreisches Tripel enthält? Es dürfen also nicht alle drei Zahlen eines solchen Tripels zu derselben Gruppe gehören. Mit wachsendem n wird die Anzahl der Möglichkeiten der Aufteilung schnell unübersichtlich, weil es 2n Möglichkeiten gibt, sodass es schon bei n = 100 mehr als 1030 Möglichkeiten zu prüfen gäbe. Die zwei Forscher konnten beweisen, dass nur bis n = 7824 eine Lösung möglich ist. Hätten alle Möglichkeiten blind durchprobiert werden müssen, so sollten 27825, also etwa 4 × 102355 Kombinationen getestet werden und das ist eine Aufgabe, die kein heutiger Supercomputer innerhalb seiner Lebensdauer bewältigen kann.

Zur Lösung mit einem SAT-Solver muss die zur Prüfung stehende Fragestellung erst in ein Erfüllbarkeitsproblem transformiert werden. Diese Umsetzung ist keineswegs trivial, und ihr Ergebnis kann unterschiedlich parametrisiert werden. So kann ein und dieselbe Fragestellung in mehrere logische Formeln übersetzt werden, die sich in der Anzahl der binären Variablen und der Länge und Anzahl der Klauseln unterscheiden. Dabei spielt das Format der logischen Formel der Solver-Eingabe eine wesentliche Rolle für die Effizienz des Solvers – in Abhängigkeit von den Solver-Einstellungen.

SAT-Solver CryptoMiniSat

Im Rahmen eines Projekts, das vom BSI zusammen mit der inducto GmbH durchgeführt wurde, ist der Sourcecode des Open-Source-SAT-Solvers CryptoMiniSat (CMS) analysiert worden. Durch eine statistische Analyse der Laufzeitergebnisse des Solvers bei wiederholten Lösungsversuchen von Instanzen, die einen kryptografischen Known-Plaintext-Angriff (KPA) auf die „Small AES-64 Modell-Cipher SR (3, 4, 4, 4)“ implementieren, wurden Kombinationen der Einstellungsparameter von CMS gefunden, mit denen dieses im Allgemeinen als unlösbar betrachtete Problem mit realistischem Aufwand lösbar wurde. Die empirisch ermittelten Solver-Parametereinstellungen wurden dabei mithilfe des Open-Source-Software-Tools SMAC zur automatisierten Algorithmen-Konfiguration weiter verfeinert, das sich einer sogenannten sequenziellen modellbasierten Optimierung, einer Reinforcement-Learning-Methode der KI, bedient. Die in diesem Projekt erzielten sehr guten Ergebnisse wurden auf der FLoC (Federated Logic Conference) in Oxford im Juli 2018 präsentiert (siehe auch https://easychair.org/publications/paper/5g6S).

Die statistische Laufzeitanalyse des SAT-Solver (CMS) für Instanzen verschiedener Größen wurde mit Boxplots visualisiert, da Median und Quartile ein stabileres Maß für die Streuung der wegen längerer Laufzeiten begrenzten Anzahl von Ergebnissen als Mittelwert und Varianz darstellen. Hier ist anzumerken, dass CMS parallelisiert mit mehreren Threads indeterministisch zu einer Lösung findet und bei gleichen Eingaben und identischen Solver-Einstellungen unterschiedliche Laufzeiten liefert.

Die Code-Analyse und eine anschließende Machbarkeitsstudie motivieren zur Steigerung der Effizienz von CMS bei der Lösung von harten CNF-Instanzen mithilfe von KI-Methoden. Es mag wie ein Zirkelschluss klingen, wenn SAT-Solver-Methoden einerseits für das maschinelle Lernen eingesetzt werden und anderseits die SAT-Solver mittels KI verbessert werden – jedoch wird diese Richtung schon in der Informatik verfolgt und hat bereits einige gute Ergebnisse hervorgebracht.

Aussagenlogisches Erfüllbarkeitsproblem

In der Mathematik ist die boolesche Erfüllbarkeit (nach George Boole, einem britischen Mathematiker) ein
Entscheidungsproblem, das sich durch eine aussagenlogische Formel darstellen lässt, die ausschließlich UND-, ODER- und NICHT-Verknüpfungen binärer Variablen enthält. Die Formel wird in kleinere logische Aussagen, die sogenannten Klauseln, unterteilt, die ihrerseits alle mit UND zur Gesamtformel verknüpft sind.

Das Erfüllbarkeitsproblem ist es, zu entscheiden, ob eine gegebene quantifizierte boolesche Formel ohne freie Variablen wahr oder falsch ist. Gesucht wird daher eine Belegung der Variablen mit WAHR oder FALSCH, die alle Klauseln des Problems erfüllt, oder aber der Nachweis, dass keine solche Belegung möglich, also mindestens eine Klausel nicht erfüllbar ist.