Monadic Constraint Programming

by Tom Schrijvers, Peter Stuckey and Philip Wadler

Edit: The slides of my invited talk at WLP 2009 on Monadic Constraint Programming are now available.

Abstract:

A constraint programming system combines two essential components: a constraint solver and a search engine. The constraint solver reasons about satisfiability of conjunctions of constraints, and the search engine controls the search for solutions by iteratively exploring a disjunctive search tree defined by the constraint program. In this paper we give a monadic definition of constraint programming where the solver is defined as a monad threaded through the monadic search tree. We are then able to define search and search strategies as first class objects that can themselves be built or extended by composable search transformers. Search transformers give a powerful and unifying approach to viewing search in constraint programming, and the resulting constraint programming system is first class and extremely flexible.

Let's briefly look at the n queens example from the paper. First, there is the nqueens model:

nqueens n = exist n $ \queens -> model queens n /\
                                 enumerate queens

model queens n = queens ‘allin‘ (1,n) /\ 
                 alldifferent queens /\ 
                 diagonals queens
 
allin queens range = conj [q ‘in_domain‘ range | q <- queens ]     alldifferent queens = conj [ qi @\= qj | qi:qjs <- tails queens,                                          qj <- qjs ]  diagonals queens = conj [ qi @\== (qj @+ d) /\ qj @\== (qi @+ d)                         | qi:qjs <- tails queens, (qj,d) <- zip qjs [1..]]  conj = foldl (/\) true  

The enumeration of possible values can be quite sophisticated, e.g.

enumerate = Lazy . (label firstfail middleout)

where firstfail selects the queen with the smallest
domain first, and middleout selects the middle values
in the domain first. You can easily write custom variable and
value selection strategies, or alternative enumeration functions.

To actually compute solutions, we have to solve the model:

> solve dfs it $ nqueens 4
[[2,4,1,3],[3,1,4,2]]

i.e. we yields these two solutions of 4 queens:

The search strategy used above is depth-first search (dfs) without
any additional search transformers (i.e. identity transformer it).
Here are three variations, using alternative search strategies:

> solve dfs (nb 100 :- db 25 :- bb newBound) $ nqueens 4
> solve bfs (db 25 :- nb 100 :- bb newBound) $ nqueens 4
> solve bfs (ld 10 :- nb 100 :- bb newBound) $ nqueens 4

where

• bfs is the breadth-first queueing strategy,


• nb n stops search after visiting n nodes in the search tree,


• dbn does not visit nodes below depth n in the search tree,


• ld n does not visit nodes that are more than n right branches from the root of the search tree (limited discrepancy), and


• bb newBound is branch-and-bound optimization (in this example the value of the last queen is minimized; makes more sense for other problems).

The :- operator combines the various (composable) search transformers. The purpose of these search transformers is of course to find (all, one, the best) solutions more quickly.

More

• Draft paper
• Prototype code (requires GHC >= 6.10)
  

Your feedback is appreciated.