Monad Transformers for Backtracking Search

TL;DR

This paper introduces the selection monad transformer in Haskell for expressing backtracking search algorithms, demonstrates its application in SAT solving, and explores its connection to game theory through nondeterministic backward induction.

Contribution

It extends the selection monad to a transformer, enabling modular backtracking algorithms and links selection functions to game theory concepts.

Findings

Implemented a DPLL-like SAT solver without explicit recursion

Connected selection monad transformer to backward induction in nondeterministic games

Demonstrated the utility of monad transformers for backtracking search algorithms

Abstract

This paper extends Escardo and Oliva's selection monad to the selection monad transformer, a general monadic framework for expressing backtracking search algorithms in Haskell. The use of the closely related continuation monad transformer for similar purposes is also discussed, including an implementation of a DPLL-like SAT solver with no explicit recursion. Continuing a line of work exploring connections between selection functions and game theory, we use the selection monad transformer with the nondeterminism monad to obtain an intuitive notion of backward induction for a certain class of nondeterministic games.