Home > Uncategorized > A monadic constraint solver in F#

A monadic constraint solver in F#

Monads, a.k.a. computation expressions, permits the programmer to define a custom domain specific language (dsl) within the host language. When thinking about this I got the, in my opinion, great idea to build a dsl for constraint programming in F# using monads. However, as is common with great ideas, someone else has already though of it before. In this case I found out that David Overton was the man. He uses a specialized monad that allows constraint programming within Haskell. I definitely recommend reading his excellent blog post on this and also how he uses his library to solve Sudoku puzzles. Still, I thought it would be interesting to see how this worked out in F#.

Using the state transformer from an earlier post, with a few minor modifications, provided the core framework that I needed. David also uses a few monad control functions that made his code short and readable. Mostly due to the fact that they cannot be implemented generically, I think no F# equivalent exists in any library. However, non-generic versions are easy to implement – and that is what I did. Here is the entire monadic framework:

// ref: http://www.randomhacks.net/articles/2007/03/12/monads-in-15-minutes

type ListMonad() =

   // Semantics

   member o.Return(x) = [x]

   member o.Bind(m, f) = List.concat( List.map f m )

   member o.Zero() = []

   // Helpers

   member o.Guard(c) = if c then o.Return(()) else o.Zero()

 

// ref: http://matthewmanela.com/blog/parameterized-state-transformer-monad-in-f-2/

// ref: http://monads.haskell.cz/html/xformeranatomy.html

// ref: http://cs.hubfs.net/forums/thread/7472.aspx (combine, delay)

// ref: http://tomasp.net/articles/imperative-i-return.aspx (combine, delay)

type StateMonadT(listM : ListMonad) =

    // Semantics

    member o.Return(v) = fun st -> listM.Return(v, st)

    member o.ReturnFrom(x) = x

    member o.Bind(m, f) = fun st -> listM.Bind(m st, fun (v, st’) -> f v st’)

    member o.Zero() = fun st -> listM.Return((), st)

    member o.Combine(p1,dp2) = o.Bind(p1, fun _ -> dp2)

    member b.Delay(f) = f()

    // Helpers

    member o.Update(f) = fun st -> listM.Return((), f st)       

    member o.Get() = fun st -> listM.Return(st, st)

    member o.Set(st) = fun _ -> listM.Return((), st)

    member o.Execute(m, s0) = m s0 |> List.map fst

    member o.Lift(c) = fun st -> listM.Bind(c, fun x -> listM.Return(x,st))

    member o.Guard(c) = o.Lift(listM.Guard(c))

 

let listM = ListMonad()

let stateMT = StateMonadT(listM)

 

let rec mapM m xs = stateMT {

        match xs with

        | x::rest ->

            let! value = m x

            let! values = mapM m rest

            return value :: values

        | _ -> return []       

    }

 

let rec mapM_ m xs = stateMT {

        match xs with

        | x::rest ->

            do! m x

            do! mapM_ m rest

        | _ -> return ()

    }

 

let rec replicateM n m = stateMT {

        match n with

        | 0 -> return []

        | _ ->

            let! x = m

            let! rest = replicateM (n-1) m

            return x::rest   

    }

 

let rec zipWithM_ f xs ys = stateMT {

        match xs, ys with

        | x::rxs, y::rys ->

            let m = f x y

            do! m

            do! zipWithM_ f rxs rys

        | _ -> return ()

    }

 

Having this in place the constraint solver can be constructed. First of all the types needed:

type FDVar = { id : int }

and VarInfo = { values : Set<int>; delayedConstraints : FDState -> List<unit*FDState> }

and FDState = { varMap : Map<FDVar, VarInfo>; nextId : int }

 

I kept it a little less verbose then the original but the semantics is the same. The function for executing a constraint program was short:

let runFD fd = stateMT.Execute(fd, { varMap = Map.empty; nextId = 0 })

 

The next step was to add functions for declarations of variables:

let newVar domain =

    let nextVar = stateMT {

        let! s = stateMT.Get()

        let vid = s.nextId

        do! stateMT.Set({ s with nextId = vid + 1})

        return { id = vid }

    }

    let isOneOf x domain = stateMT {

        return! stateMT.Update(fun s ->

            let vm = s.varMap

            let vi = { values = Set.ofList domain; delayedConstraints = stateMT.Return(()) }

            { s with varMap = Map.add x vi vm }

        )

    }   

    stateMT {

        let! v = nextVar

        do! isOneOf v domain

        return v

    }

 

let rec newVars n domain = replicateM n (newVar domain)

 

A few helper methods (following the same path as David):

let lookup x = stateMT {

        let! s = stateMT.Get()

        return s.varMap.[x].values

    }

 

let update x i = stateMT {

        let! s = stateMT.Get()

        let vm = s.varMap

        let vi = vm.[x]

        do! stateMT.Set({ s with varMap = Map.add x { vi with values = i } vm })

        do! vi.delayedConstraints

    }

 

let addConstraint x constr = stateMT {

        let! s = stateMT.Get()

        let vm = s.varMap

        let vi = vm.[x]

        let delayedConstraints’ = stateMT {

            do! constr

            do! vi.delayedConstraints

        }

        do! stateMT.Set({ s with varMap = Map.add x { vi with delayedConstraints = delayedConstraints’ } vm })

    }

 

let addBinaryConstraint f x y = stateMT {

        let constr = f x y

        do! constr

        do! addConstraint x constr

        do! addConstraint y constr

    }

 

Now, using the helper methods, we start defining constraints:

let hasValue var value = stateMT {

        let! vals = lookup var

        do! stateMT.Guard(Set.contains value vals)

        let i = Set.singleton value       

        if i <> vals then

            do! update var i

    }

 

let same =

    let sameConstraint x y = stateMT {

        let! xv = lookup x

        let! yv = lookup y

        let i = Set.intersect xv yv

        do! stateMT.Guard(Set.isEmpty i |> not)        

        if i <> xv then

            do! update x i

        if i <> yv then

            do! update y i

    }

    addBinaryConstraint sameConstraint

 

let different =

    let differentConstraint x y = stateMT {

        let! xv = lookup x

        let! yv = lookup y

        do! stateMT.Guard(Set.count xv > 1 || Set.count yv > 1 || xv <> yv)

        if Set.count xv = 1 && Set.isProperSubset xv yv then

            do! update y (Set.difference yv xv)

        if Set.count yv = 1 && Set.isProperSubset yv xv then

            do! update x (Set.difference xv yv)

    }

    addBinaryConstraint differentConstraint

 

let rec allDifferent xs =

    stateMT {

        match xs with

        | x::rest ->

            do! mapM_ (different x) rest

            do! allDifferent rest

        | _ -> return ()

    }   

 

I use the optimized different constraint that David suggests in his later post. The only thing that remains now is the labelling function for backtrack search.

let rec labelling vars =

    let label var = stateMT {

        let! vals = lookup var

        let! value = stateMT.Lift(Set.toList vals)

        do! hasValue var value

        return value

    }

    mapM label vars

 

That’s all we need. A couple of samples may be in place:

let sample1 = stateMT {

        let! a = newVar [1..4]

        let! b = newVar [1..4]

        do! different a b

        return! labelling [a; b]

    }

 

runFD sample1 |> printf “sample1: %A\n”

 

let sample2 = stateMT {

        let! vars = newVars 3 [1..4]

        do! allDifferent vars

        return! labelling vars

    }

 

runFD sample2 |> printf “sample2: %A\n”

 

let sample3 = stateMT {

        let! a = newVar [1..9]

        let! b = newVar [1..3]

        let! c = newVar [1..2]

        do! hasValue a 7

        return! labelling [a;b;c]

    }

 

runFD sample3 |> printf “sample3: %A\n”

 

let sample4 = stateMT {

        let! a = newVar [1..9]

        let! b = newVar [2..7]

        do! same a b

        return! labelling [a;b]

    }

 

runFD sample4 |> printf “sample4: %A\n” 

 

And of course also a Sudoku solver:

type Puzzle = int list

 

let test : Puzzle = [

    0; 0; 0; 0; 8; 0; 0; 0; 0;

    0; 0; 0; 1; 0; 6; 5; 0; 7;

    4; 0; 2; 7; 0; 0; 0; 0; 0;

    0; 8; 0; 3; 0; 0; 1; 0; 0;

    0; 0; 3; 0; 0; 0; 8; 0; 0;

    0; 0; 5; 0; 0; 9; 0; 7; 0;

    0; 5; 0; 0; 0; 8; 0; 0; 6;

    3; 0; 1; 2; 0; 4; 0; 0; 0;

    0; 0; 6; 0; 1; 0; 0; 0; 0 ];

 

// ref: http://fsharpcode.blogspot.com/2010/03/splitevery-chunk.html

let rec chunk n xs =

    let splitAt n (xs:#seq<‘a>) = (Seq.take n xs |> Seq.toList, Seq.skip n xs |> Seq.toList)

    match xs with

    | [] -> []

    | _ ->

        let ys, zs = splitAt n xs

        ys :: chunk n zs

 

let rows xs = chunk 9 xs

 

let columns xs =

    // ref: http://stackoverflow.com/questions/3016139/help-me-to-explain-the-f-matrix-transpose-function

    let rec transpose = function

        | (_::_)::_ as M -> List.map List.head M :: transpose (List.map List.tail M)

        | _ -> []   

    xs |> rows |> transpose

 

let boxes xs =    

    let box (xa : array<‘a>) bi bj : list<‘a> =

        [       

            for j in 0..2 do

              let r = bj*3 + j

              for i in 0..2 do

                 let c = bi*3 + i

                 yield xa.[r*9+c]

        ]

    [

        let xa = Array.ofList xs

        for bj in 0..2 do

          for bi in 0..2 do

            yield box xa bi bj                           

    ]

 

let sudoku (puzzle : Puzzle) = stateMT {

        let! vars = newVars 81 [1..9]

        do! zipWithM_ (fun x n -> stateMT { if n > 0 then do! hasValue x n }) vars puzzle

        do! mapM_ allDifferent (rows vars)

        do! mapM_ allDifferent (columns vars)

        do! mapM_ allDifferent (boxes vars)

        return! labelling vars

    }

 

let result = runFD (sudoku test)

for r in result do

    r |> rows |> List.map (fun row -> printf “%A\n” row) |> ignore

    printf “———–\n”

 

Advertisements
Categories: Uncategorized
  1. No comments yet.
  1. No trackbacks yet.

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

%d bloggers like this: