Bachelor/Master Thesis
SAT-Löser (SAT-solver) sind Programme, die erfüllende Belegungen für aussagenlogische Formeln berechnen. Obwohl das Problem NP-vollständig ist, sind in den letzten 10 Jahren entscheidende Implementierungsfortschritte gemacht worden, die es erlauben, erfüllende Belegungen für Formeln mit mehr als 100000 Variablen zu finden. Die Anwendungsgebiete sind vielfältig und reichen von der Schaltungsverifikation bis zur Lösung von Sudokus. Alle 1-2 Jahre findet ein Wettlauf der besten SAT-Löser der Welt statt.
Die meisten SAT-Löser sind in C geschrieben. Ziel der Arbeit ist es, einen SAT Löser in (Standard) ML zu entwerfen und programmieren. (OCaml ist ein Dialekt von ML.) Dabei ist zu untersuchen, wie Implementierungstechniken von C sich auf ML übertragen lassen, wobei ML auch Arrays und Zeiger hat. Ausgangspunkt ist der in C geschriebene open source SAT-Löser MiniSat.
Arbeitsumgebung:
Standard ML
Notwendige Vorkenntnisse:
Vertrautheit mit OCaml, ML oder Haskell; Englisch
Aufgabensteller und Betreuer:
Tobias Nipkow, Raum FMI 01.11.058, email {nipkow} AT [in.tum.de]