Umfang

Dieses Thema kann als Bachelorarbeit bearbeitet werden.

Empfohlene Vorkenntnisse

  • logische Programmierung (Prolog)

Problemstellung

Das Ziel des Constraint Solving ist es eine logische Formel mit gewissen Theorien (z.B. Mengentheorie, ganze Zahlen, reelle Zahlen, ..) zu beweisen oder zu widerlegen. Für die Erfüllbarkeit einer Formel wird vereinfacht gesagt eine Belegung aller vorkommenden Variablen gesucht welche die Formel wahr machen. Wenn eine Lösung existiert, wird die gefundene Belegung der Variablen zurück gegeben. Mittels Backtracking sollen weitere/alle Lösungen enumeriert werden können.

Constraint Solving ist eine komplexe Aufgabe und erfordert oftmals einen hohen Rechenaufwand. Für reelle Zahlen ist die Komplexität um ein vielfaches höher, da unter anderem auch auf Genauigkeiten bei dem Rechnen mit rellen Zahlen geachtet werden muss. Integer Difference Logic ist eine Teilmenge der Integer Arithmetik bei welcher Constraints der Form x - y <= c akzeptiert werden, wobei x und y Integer Variablen sind und c eine Integer Konstante. Viele Integer Constraints können in diese Form überführt werden. Dies gilt ebenso für Constraints über reelle Zahlen. Wang et al. haben eine graphbasierten Solver für Integer und Real Difference Logic präsentiert. Christopher David Lösbrock hat im Rahmen seiner Bachelorarbeit graphbasierte Solver für Integer und Real Difference Logic implementiert und evaluiert.

Im Rahmen dieser Arbeit soll ein graphbasierter Constraint Solver für Real Difference Logic in Prolog implementiert und evaluiert werden. Es ist geplant, dass dieser Constraint Solver Anwendung in dem bei uns am Lehrstuhl entwickelten Werkzeug ProB findet. Der Constraint Solver könnte z.B. als Theory Solver in unser SMT Framework und zugleich als alleinstehender Constraint Solver in ProB integriert werden. Dies ist aber kein verpflichtender Teil dieser Arbeit sondern eine Erweiterung.

Minimalanforderungen

  • ein graphbasierter Constraint Solver für Real Difference Logic
  • Backtracking für (vollständige) Enumeration von Lösungen
  • eine empirische Auswertung der Leistung, z.B. im Vergleich zu Prolog’s CLP(R) Bibliothek

Erweiterungen

  • Performanceoptimierung
  • Einbindung in SMT Framework (Satisfiability Modulo Theories)

Kontakt

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