Umfang

Dieses Thema kann je nach Umfang als Bachelorarbeit, Teil einer Projektarbeit oder Masterarbeit bearbeitet werden.

Empfohlene Vorkenntnisse

  • logische Programmierung
  • Constraint Solving (CLP(FD))
  • C/C++
  • SMT-LIB

Problemstellung

Im Rahmen dieser Arbeit soll die Möglichkeit geschaffen werden arithmetische Constraints der CLP(FD) (https://www.swi-prolog.org/man/clpfd.html ; https://sicstus.sics.se/sicstus/docs/latest/html/sicstus/lib_002dclpfd.html) Bibliothek von Prolog (SWI- und/oder SICStus Prolog) mit modernen SMT Solvern zu lösen. Um dies zu erreichen, sollen CLP(FD) Constraints von Prolog nach SMT-LIB übersetzt und anschließend an einen entsprechenden SMT Solver gesendet werden. Gefundene Lösungen sollen dann wieder nach Prolog übersetzt werden. Als SMT Solver bieten sich z.B. Z3 (https://rise4fun.com/z3/tutorial) oder CVC4 (https://cvc4.github.io/) an. Diesbezüglich muss eine Schnittstelle zwischen Prolog und einem SMT Solver geschaffen werden. Hierfür bietet sich eine Entwicklung in C oder C++ an. Die eigentliche Übersetzung kann wahlweise in Prolog oder C/C++ erfolgen.

Die Motivation dieser Arbeit ist darin begründet, dass die CLP(FD) Solver von SWI- und SICStus Prolog auf klassische Domänenreduktion setzen wohingegen SMT Solver arithmetische Constraints zum Beispiel als Bitvektoren darstellen und anschließend SAT Solver für die Lösungsfindung verwenden (Bit-Blasting). Die Vermutung ist, dass SMT Solver im Allgemeinen eine bessere Performance aufweisen als Konsistenzalgorithmen.

Minimalanforderungen

  • Übersetzung von (einer Teilmenge an) CLP(FD) Constraints nach SMT-LIB
  • Schnittstelle zwischen Prolog und mindestens einem SMT Solver
  • Backtracking zwischen Prolog und dem SMT Solver
  • Einbettung von gefundenen Lösungen in Prolog
  • Evaluation der Performance im Vergleich zu CLP(FD) Solver

Erweiterungen

  • Integration von Labeling Optionen in die Übersetzung nach SMT-LIB
  • Integration von sogenannten Globalen Constraints (z.B. all_different/1)
  • Integration von Reification Predicates
  • Evaluation verschiedener SMT Solver

Kontakt

Joshua Schmidt
Raum 25.12.02.52 · joshua.schmidt@hhu.de