Performance-Evaluation von SAT-Solving-Verfahren

Bachelorarbeit (abgeschlossen 2023)

Erstbetreuer: Prof. Dr. Malte Lochau

Zweitbetreuer: M. Sc. Robert Müller

Beschreibung

In dieser Abschlussarbeit beschäftigen wir uns mit der Verwendung von SAT-Solver im Rahmen vorlesungsbegleitenden Kapazitäten. Hierzu betrachten wir zuerst worum es sich bei dem SAT-Problem, auch bekannt als Erfüllbarkeitsproblem der Aussagenlogik, genau handelt und warum es relevant ist. Nach dieser Einführung in die Thematik des SAT-Solving werfen wir dann einen Blick auf die Ursprünge der SAT-Solver und grundlegende Funktionsweise moderner SAT-Solver.

Anschließend an diese Einführung in den Themenbereich der SAT-Solver präsentieren wir noch die Anforderungen die an die SAT-Solver in vorlesungsbegleitender Verwendung gestellt werden. Bei den betrachteten SAT-Solvern handelt es sich um Z3, Sat4j und PySAT welche wir im Zuge dieser Abschlussarbeit noch genauer vorstellen werden. Den Anforderungen und Präsentationen der SAT-Solver folgend werden die betrachteten SAT-Solver über den Kriterien der Kompatibilität, Benutzerfreundlichkeit und Transparenz verglichen. Diesem Vergleich folgend werden die SAT-Solver noch über ihrer Performance verglichen. Abschließend geben wir noch ein Fazit darüber wie sehr sich die betrachteten SAT-Solver für eine vorlesungsbegleitende Verwendung eignen.

⇐ Zurück zur Übersicht der Abschlussarbeiten