Seminar 28 Sept 12:00, 2012 in the seminar room of I7
Preprocessing für das Lösen Nicht-Linearer Reell-Arithmetischer Formeln (Preprocessing for Solving Non-linear Real Arithmetic Formulas)
Das Lösen nicht-linearer reell-arithmetischer (NRA) Formeln, d.h. beliebige aussagenlogische
Formeln über boolesche Variablen sowie NRA Constraints, ist im Allgemeinen sehr aufwendig.
Da es sehr häufig Verwendung findet, wie zum Beispiel in der Verifikation und Analyse von
Programmen und Modellierungen, beschäftigt man sich heutzutage vor allem im Bereich des
SAT Modulo Theorie(SMT)-Solvings ausgiebig mit diesem Thema. SMT Solver verwenden eine
Kombination aus einem SAT-Solver, der zum Lösen der booleschen Abstraktion der
Ursprungsformel verwendet wird, und einem Theorie Solver, der verschiedene
mathematische Lösungsprozeduren bereitstellt um die Konsistenz einer Menge von NRA
Constraints zu überprüfen. Optimierungsmöglichkeiten des SMT-Solvings beschäftigen sich
vor allem mit der Kommunikation zwischen dem SAT-Solver und dem Theorie Solver. Für die
reelle Arithmetic liegt der Fokus der Optimierung auch auf dem Kombinieren der vielen hierfür
existierenden mathematischen Lösungsprozeduren.
Diese Bachelorarbeit befasst sich dagegen mit dem Preprocessing der Eingabeformel bevor
sie an den SAT-Solver übergeben wird und lässt sich in die folgenden vier Ideen
unterteilen. Variablen welche linear in Gleichungen auftreten können zur Vereinfachung
von Constraints genutzt werden, indem sie darin entsprechend der Gleichung substituiert
werden. Konjunkte und Klauseln einer Formel in konjunktiver Normalform können durch
bestimmte Zusammenhänge zwischen Constraints vereinfacht werden um die Komplexität der
booleschen Struktur zu verringern. Lernklauseln, Klauseln welche dem SAT-Solver
gewisse Verhältnisse zwischen Constraints aufzuzeigen, helfen die Anzahl und den
Schwierigkeitsgrad der Theorieaufrufe zu reduzieren. Eine Analyse und Bewertungen
der Constraints beeinflusst die Belegung ihrer booleschen Abstraktion im SAT-Solver,
um die in der Theorie einfacheren Constraints vorzuziehen. Die Ergebnisse einiger
Testläufe zeigen, dass die hier vorgestellten Methoden eine zum Teil deutliche
Beschleunigung des SMT-Solvings zur Folge haben.
Das Lösen nicht-linearer reell-arithmetischer (NRA) Formeln, d.h. beliebige aussagenlogische
Formeln über boolesche Variablen sowie NRA Constraints, ist im Allgemeinen sehr aufwendig.
Da es sehr häufig Verwendung findet, wie zum Beispiel in der Verifikation und Analyse von
Programmen und Modellierungen, beschäftigt man sich heutzutage vor allem im Bereich des
SAT Modulo Theorie(SMT)-Solvings ausgiebig mit diesem Thema. SMT Solver verwenden eine
Kombination aus einem SAT-Solver, der zum Lösen der booleschen Abstraktion der
Ursprungsformel verwendet wird, und einem Theorie Solver, der verschiedene
mathematische Lösungsprozeduren bereitstellt um die Konsistenz einer Menge von NRA
Constraints zu überprüfen. Optimierungsmöglichkeiten des SMT-Solvings beschäftigen sich
vor allem mit der Kommunikation zwischen dem SAT-Solver und dem Theorie Solver. Für die
reelle Arithmetic liegt der Fokus der Optimierung auch auf dem Kombinieren der vielen hierfür
existierenden mathematischen Lösungsprozeduren.
Diese Bachelorarbeit befasst sich dagegen mit dem Preprocessing der Eingabeformel bevor
sie an den SAT-Solver übergeben wird und lässt sich in die folgenden vier Ideen
unterteilen. Variablen welche linear in Gleichungen auftreten können zur Vereinfachung
von Constraints genutzt werden, indem sie darin entsprechend der Gleichung substituiert
werden. Konjunkte und Klauseln einer Formel in konjunktiver Normalform können durch
bestimmte Zusammenhänge zwischen Constraints vereinfacht werden um die Komplexität der
booleschen Struktur zu verringern. Lernklauseln, Klauseln welche dem SAT-Solver
gewisse Verhältnisse zwischen Constraints aufzuzeigen, helfen die Anzahl und den
Schwierigkeitsgrad der Theorieaufrufe zu reduzieren. Eine Analyse und Bewertungen
der Constraints beeinflusst die Belegung ihrer booleschen Abstraktion im SAT-Solver,
um die in der Theorie einfacheren Constraints vorzuziehen. Die Ergebnisse einiger
Testläufe zeigen, dass die hier vorgestellten Methoden eine zum Teil deutliche
Beschleunigung des SMT-Solvings zur Folge haben.
