In order to experiment with constraint monads I have implemented a simple SAT solver based on the Davis-Putnam-Logemann-Loveland (DPLL) algorithm. The marked-up code is meant for human consumption — if you want to execute it, you should fetch the latest version from my git repository.
In a previous post I have explained how to extend arbitrary instances of MonadPlus with constraint solving capabilities. Now, I’ll focus on how to use this functionality to implement lazy non-deterministic computations on top of a MonadPlus.
Recently, I thought about two seemingly different topics which turn out to form a fruitful combination.
One thing I have been thinking about a lot is how to model functional-logic programming in Haskell without using impure features to ensure call-time choice semantics of lazy computations. The other thing is how to integrate constraint solving in a purely functional setting, to improve the performance of test-case generation.
It turns out that a framework for constrained monadic computations is enough to express call-time choice in non-deterministic lazy computations. We can add constraint solving to any instance of the MonadPlus type class and, hence, reuse existing instances of this class to model lazy functional-logic programming in pure Haskell.
Die Vorlesung Informatik für Nebenfächler findet Montags und Dienstags von 16-18 Uhr im CAP3(III) statt. Am Dienstag dem 21. Oktober ist die erste Vorlesung, in der auch die Anmeldung in der Studierenden-Datenbank erfolgt. Falls Sie nicht an der Anmeldung teilgenommen haben, können Sie sich auch online in der StudiDB anmelden.
Sie sollten am Tag nach der Anmeldung eine Bestätigung per Email bekommen, nach der sie sich in der StudiDB zur Übung anmelden können — und sollen! Falls Sie Probleme mit der Anmeldung haben, besuchen Sie bitte die unten genannten Rechnerzeiten.
Übungszettel 1, Übungszettel 2
Alle weiteren Übungszettel sind über das iLearn-System verfügbar.