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.
Unhappy with the conclusion of this article, I began to develop a framework for lazy functional-logic programming in Haskell that allows to compare different search strategies in an in other respects identical environment. Specifically, I aim at comparing complete strategies like breath-first search or FBackTrack (cf. aforementioned articel) w.r.t. their run-time and memory requirements. Unlike described earlier, the combination of laziness and nondeterminism should conform to Call-Time Choice semantics without prohibiting compiler optimizations due to side effects.