csp-1.4.0: Discrete constraint satisfaction problem (CSP) solver.

Safe HaskellNone
LanguageHaskell2010

Control.Monad.CSP

Contents

Synopsis

Overview

This constructs a discrete constraint satisfaction problem (CSP) and then solves it. A discrete CSP consists of a number of variables each having a discrete domain along with a number of constraints between those variables. Solving a CSP searches for assignments to the variables which satisfy those constraints. At the moment the only constraint propagation technique available is arc consistency.

Here is a simple example which solves Sudoku puzzles, project Euler problem 96.

import Data.List
import Control.Monad.CSP

solveSudoku :: (Enum a, Eq a, Num a) => [[a]] -> [[a]]
solveSudoku puzzle = oneCSPSolution $ do
  dvs <- mapM (mapM (\a -> mkDV $ if a == 0 then [1 .. 9] else [a])) puzzle
  mapM_ assertRowConstraints dvs
  mapM_ assertRowConstraints $ transpose dvs
  sequence_ [assertSquareConstraints dvs x y | x <- [0,3,6], y <- [0,3,6]]
  return dvs
      where assertRowConstraints =  mapAllPairsM_ (constraint2 (/=))
            assertSquareConstraints dvs i j = 
                mapAllPairsM_ (constraint2 (/=)) [(dvs !! x) !! y | x <- [i..i+2], y <- [j..j+2]]

 mapAllPairsM_ :: Monad m => (a -> a -> m b) -> [a] -> m ()
 mapAllPairsM_ f []     = return ()
 mapAllPairsM_ f (_:[]) = return ()
 mapAllPairsM_ f (a:l) = mapM_ (f a) l >> mapAllPairsM_ f l

sudoku3 = [[0,0,0,0,0,0,9,0,7],
           [0,0,0,4,2,0,1,8,0],
           [0,0,0,7,0,5,0,2,6],
           [1,0,0,9,0,4,0,0,0],
           [0,5,0,0,0,0,0,4,0],
           [0,0,0,5,0,7,0,0,9],
           [9,2,0,1,0,8,0,0,0],
           [0,3,4,0,5,9,0,0,0],
           [5,0,7,0,0,0,0,0,0]]
 
>>> solveSudoku sudoku3
[[4,6,2,8,3,1,9,5,7],[7,9,5,4,2,6,1,8,3],[3,8,1,7,9,5,4,2,6],[1,7,3,9,8,4,2,6,5],[6,5,9,3,1,2,7,4,8],[2,4,8,5,6,7,3,1,9],[9,2,6,1,7,8,5,3,4],[8,3,4,2,5,9,6,7,1],[5,1,7,6,4,3,8,9,2]]

Building CSPs

mkDV :: [a] -> CSP r (DV r a) Source #

Create a variable with the given domain

constraint1 :: (a -> Bool) -> DV r1 a -> CSP r () Source #

Assert a unary constraint.

constraint2 :: (a -> t1 -> Bool) -> DV t a -> DV t t1 -> CSP r () Source #

Assert a binary constraint with arc consistency.

constraint3 :: (a -> t1 -> t2 -> Bool) -> DV t a -> DV t t1 -> DV t t2 -> CSP r () Source #

Assert a trinary constraint with arc consistency.

constraint :: ([a] -> Bool) -> [DV r1 a] -> CSP r () Source #

Assert an n-ary constraint with arc consistency. One day this will allow for a heterogeneous list of variables, but at the moment they must all be of the same type.

Solving CSPs

oneCSPSolution :: CSPResult a1 => CSP (Result a1) a1 -> Result a1 Source #

Return a single solution to the CSP. solveCSP running with oneValueT

allCSPSolutions :: CSPResult a1 => CSP (Result a1) a1 -> [Result a1] Source #

Return all solutions to the CSP. solveCSP running with allValuesT

solveCSP :: CSPResult a1 => (AmbT r IO (Result a1) -> IO a) -> CSP r a1 -> a Source #

Solve the given CSP. The CSP solver is a nondeterministic function in IO and this is the generic interface which specifies how the nondeterministic computation should be carried out.

class CSPResult a where Source #

This extracts results from a CSP.

Minimal complete definition

result

Associated Types

type Result a Source #

Methods

result :: a -> IO (Result a) Source #

Instances

CSPResult a => CSPResult [a] Source # 

Associated Types

type Result [a] :: * Source #

Methods

result :: [a] -> IO (Result [a]) Source #

(CSPResult a, CSPResult b) => CSPResult (a, b) Source # 

Associated Types

type Result (a, b) :: * Source #

Methods

result :: (a, b) -> IO (Result (a, b)) Source #

CSPResult (DV r a) Source # 

Associated Types

type Result (DV r a) :: * Source #

Methods

result :: DV r a -> IO (Result (DV r a)) Source #

(CSPResult a, CSPResult b, CSPResult c) => CSPResult (a, b, c) Source # 

Associated Types

type Result (a, b, c) :: * Source #

Methods

result :: (a, b, c) -> IO (Result (a, b, c)) Source #

(CSPResult a, CSPResult b, CSPResult c, CSPResult d) => CSPResult (a, b, c, d) Source # 

Associated Types

type Result (a, b, c, d) :: * Source #

Methods

result :: (a, b, c, d) -> IO (Result (a, b, c, d)) Source #

(CSPResult a, CSPResult b, CSPResult c, CSPResult d, CSPResult e) => CSPResult (a, b, c, d, e) Source # 

Associated Types

type Result (a, b, c, d, e) :: * Source #

Methods

result :: (a, b, c, d, e) -> IO (Result (a, b, c, d, e)) Source #

(CSPResult a, CSPResult b, CSPResult c, CSPResult d, CSPResult e, CSPResult f) => CSPResult (a, b, c, d, e, f) Source # 

Associated Types

type Result (a, b, c, d, e, f) :: * Source #

Methods

result :: (a, b, c, d, e, f) -> IO (Result (a, b, c, d, e, f)) Source #

Low-level internal

csp :: IO x -> CSP r x Source #

Lift an IO computation into the CSP monad. CSPs are only in IO temporarily.

domain :: DV t t1 -> IO [t1] Source #

Extract the current domain of a variable.

demons :: DV r a -> IO [Constraint r] Source #

Extract the current constraints of a variable.

isBound :: DV t t1 -> IO Bool Source #

Is the variable currently bound?

domainSize :: DV t t1 -> IO Int Source #

Compute the size of the current domain of variable.

localWriteIORef :: IORef a -> a -> AmbT r IO () Source #

This performs a side-effect, writing to the given IORef but records this in the nondeterministic computation so that it can be undone when backtracking.

binding :: DV t b -> IO b Source #

Retrieve the current binding of a variable.

addConstraint :: DV r1 a -> Constraint r1 -> CSP r () Source #

Add a constraint to the given variable.

restrictDomain :: DV r a -> ([a] -> IO [a]) -> AmbT r IO () Source #

The low-level function out of which constraints are constructed. It modifies the domain of a variable.

Types

data DV r a Source #

Constructors

DV 

Instances

CSPResult (DV r a) Source # 

Associated Types

type Result (DV r a) :: * Source #

Methods

result :: DV r a -> IO (Result (DV r a)) Source #

type Result (DV r a) Source # 
type Result (DV r a) = a

data DVContainer r Source #

Constructors

DVContainer 

Fields

type Constraint r = AmbT r IO () Source #

data CSP r x Source #

Constructors

CSP 

Fields

Instances

Monad (CSP r) Source # 

Methods

(>>=) :: CSP r a -> (a -> CSP r b) -> CSP r b #

(>>) :: CSP r a -> CSP r b -> CSP r b #

return :: a -> CSP r a #

fail :: String -> CSP r a #

Functor (CSP r) Source # 

Methods

fmap :: (a -> b) -> CSP r a -> CSP r b #

(<$) :: a -> CSP r b -> CSP r a #

Applicative (CSP r) Source # 

Methods

pure :: a -> CSP r a #

(<*>) :: CSP r (a -> b) -> CSP r a -> CSP r b #

liftA2 :: (a -> b -> c) -> CSP r a -> CSP r b -> CSP r c #

(*>) :: CSP r a -> CSP r b -> CSP r b #

(<*) :: CSP r a -> CSP r b -> CSP r a #