Direkt zum InhaltDirekt zur Navigation

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

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

Termine
21. Fakultätsratssitzung IMN 27.09.2017 14:30 - 16:30 — Z417
World Usability Day 09.11.2017, HTWK-Veranstaltung 09.11.2017 09:00 - 17:00 — HTWK Leipzig, Gutenberg-Bau
Verteidigungen
Bachelorverteidigung Aruscha Kramm Raum: Z 417
Beginn: 26.09.17 - 09:00
Masterverteidigung Alexander Twrdik Raum: Z417
Beginn: 26.09.17 - 14:00
Masterverteidigung Sebastian Knabe Raum: ***Li 125***
Beginn: 27.09.17 - 09:00
Bachelorverteidigung Patrick Jeckel Raum: *** Li 125 ***
Beginn: 27.09.17 - 10:30
Bachelorverteidigung Martin Schmidt Raum: Z 417
Beginn: 27.09.17 - 12:30