Enabling SMT Solvers for Prolog by Translating to SMT-LIB
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 SchmidtRaum 25.12.02.52 · joshua.schmidt@hhu.de