Direkt zum InhaltDirekt zur Navigation

Navigation

Kompilation von Constraint-Programmen: Erfolgreicher Abschluß eines kooperativen Promotionsverfahrens

Publiziert: 22.02.2017
Diagramm aus dem Korrektheitsbeweis der Constraint-Kompilation

Constraint-Kompilation

Herr Diplom-Informatiker (FH) Alexander Bau, Absolvent unserer Fakultät, verteidigte am 7. Februar 2017 seine Dissertation "SAT Compilation for Constraints over Structured Finite Domains". Damit konnte Herr Bau das kooperative Promotionsverfahren mit der Fakultät Informatik der Technischen Universität Dresden erfolgreich abschließen. Seine Arbeit wurde betreut von Herrn Prof. Dr.‑Ing. habil. Dr. h.c. Heiko Vogler (TUD) und Herrn Prof. Dr. Johannes Waldmann (HTWK) und gefördert durch ein Stipendium des Europäischen Sozialfonds.

Kompilation von Constraint-Programmen

Ausführbare Spezifikationen sind das Ideal der Programmierung: Wir spezifizieren die gewünschte Beziehung zwischen Ein- und Ausgabe durch eine logische Formel (ein sogenanntes Constraint) - und alles weitere geschieht automatisch - ein Constraint-Solver bestimmt zu jeder Eingabe eine passende Ausgabe.

Als Assemblersprache der Constraint-Programmierung benutzt man  aussagenlogische Constraints in konjunktiver Normalform (SAT). Dafür gibt es erstaunlich effiziente Solver. Diese benutzen Baumsuche mit Propagationen (DPLL-Verfahren, ca. 1960) sowie Lernverfahren (CDCL, ca. 1996) und können SAT-Constraints mit Millionen von Klauseln oft in wenigen Minuten lösen, was bei jährlichen Wettbewerben nachgewiesen wird.

Solche SAT-Constraints möchten wir aber nicht von Hand schreiben, sondern die Anwendungsaufgabe in einer ausdrucksstärkeren und besser strukturierten Constraint-Sprache formulieren. In seiner Dissertation hat Herr Bau einen Compiler von einer Teilmenge der funktionalen Programmiersprache Haskell nach SAT entwickelt. Damit können baumartige Daten (algebraische Datentypen und pattern matching) sowie Funktionen (auch polymorph und von höherer Ordnung) zur Constraint-Programmierung benutzt werden.

Herr Bau hat den Compiler entworfen und realisiert sowie dessen Korrektheit bewiesen und zwei Anwendungsfälle ausführlich untersucht - die automatische Terminationsanalyse durch rekursive Pfadordnung auf sematische gelabelten Systemen sowie das RNA-Design-Problem. Resultate dieser Forschungsarbeiten wurden in mehreren Workshop-Beiträgen publiziert. Das Programm zur Terminationsanalyse nahm an der Termination Competition 2014 teil und war dort für einige Benchmarks das einzige Programm, das eine Lösung fand.

Herrn Baus Arbeit wurde an unserer Fakultät IMN durch Herrn Prof. Dr. J. Waldmann betreut, der Compilerbau und Constraint-Programmierung erforscht und lehrt. Der Betreuer der kooperierenden Fakultät Informatik der TU Dresden war Herr Prof. Dr.‑Ing. habil. Dr. h.c. Heiko Vogler, Lehrstuhl für Grundlagen der Programmierung.

 

http://www.imn.htwk-leipzig.de/~abau/  http://abau.org/co4.html

Nachrichten RSS
Termine
JUG Saxony Camp 2017 an der HTWK 31.03.2017 09:00 - 18:00 — NIEPER-Bau der HTWK Leipzig
Masterseminar am 12.04.2017 12.04.2017 14:00 - 17:30 — Z 417
SKILL 2017 / Call for Papers 30.04.2017 - 30.09.2017