summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorAndreiBarbu <>2013-08-14 08:53:46 (GMT)
committerhdiff <hdiff@hdiff.luite.com>2013-08-14 08:53:46 (GMT)
commita6267d1b1b823fb571614323cd160991e29af86d (patch)
treec227aa2810b629b9c9ff8a7897e8d788810c6a9f
version 1.01.0
-rw-r--r--Control/Monad/CSP.hs246
-rw-r--r--LICENSE165
-rw-r--r--README.md41
-rw-r--r--Setup.lhs4
-rw-r--r--csp.cabal23
5 files changed, 479 insertions, 0 deletions
diff --git a/Control/Monad/CSP.hs b/Control/Monad/CSP.hs
new file mode 100644
index 0000000..e611287
--- /dev/null
+++ b/Control/Monad/CSP.hs
@@ -0,0 +1,246 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module Control.Monad.CSP
+ (
+ -- * Overview
+ -- $overview
+
+ -- * Building CSPs
+ mkDV,
+ constraint1,
+ constraint2,
+ constraint,
+ -- * Solving CSPs
+ oneCSPSolution,
+ allCSPSolutions,
+ solveCSP,
+ CSPResult(..),
+ -- * Low-level internal
+ csp,
+ domain,
+ demons,
+ isBound,
+ domainSize,
+ localWriteIORef,
+ binding,
+ addConstraint,
+ restrictDomain,
+ -- * Types
+ DV(..),
+ DVContainer(..),
+ Constraint,
+ CSP(..),
+ ) where
+import Control.Monad.Amb
+import Control.Monad
+import Control.Monad.State.Strict
+import Data.IORef
+import System.IO.Unsafe
+
+-- $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]]
+
+
+data DV r a = DV { dvDomain :: IORef [a], dvConstraints :: IORef [Constraint r] }
+type Constraint r = AmbT r IO ()
+
+data DVContainer r = DVContainer { dvcIsBound :: AmbT r IO Bool,
+ dvcConstraints :: AmbT r IO (),
+ dvcABinding :: AmbT r IO () }
+
+data CSP r x = CSP { unCSP :: IORef [DVContainer r] -> IO x }
+
+-- | Lift an IO computation into the CSP monad. CSPs are only in IO
+-- temporarily.
+csp :: IO x -> CSP r x
+csp x = CSP (\_ -> x)
+
+instance Monad (CSP r) where
+ CSP x >>= y = CSP (\s -> x s >>= (\(CSP z) -> z s) . y)
+ return a = CSP (\_ -> return a)
+
+-- | Extract the current domain of a variable.
+domain :: DV t t1 -> IO [t1]
+domain (DV d _) = readIORef d
+
+-- | Extract the current constraints of a variable.
+demons :: DV r a -> IO [Constraint r]
+demons dv = readIORef (dvConstraints dv)
+
+-- | Is the variable currently bound?
+isBound :: DV t t1 -> IO Bool
+isBound dv = domain dv >>= return . (== 1) . length
+
+-- | Compute the size of the current domain of variable.
+domainSize :: DV t t1 -> IO Int
+domainSize dv = domain dv >>= return . length
+
+-- | Create a variable with the given domain
+mkDV :: [a] -> CSP r (DV r a)
+mkDV xs = do
+ d <- csp $ newIORef xs
+ c <- csp $ newIORef []
+ let dv = DV d c
+ CSP (\x -> modifyIORef x $ ((DVContainer (lift $ isBound dv)
+ (lift (demons dv) >>= sequence_)
+ (do
+ d' <- lift $ readIORef d
+ e <- aMemberOf d'
+ restrictDomain dv (\_ -> return [e])))
+ :))
+ return dv
+
+-- | 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.
+localWriteIORef :: IORef a -> a -> AmbT r IO ()
+localWriteIORef ref new = do
+ previous <- lift $ readIORef ref
+ uponFailure (lift $ writeIORef ref previous)
+ lift $ writeIORef ref new
+
+-- | The low-level function out of which constraints are
+-- constructed. It modifies the domain of a variable.
+restrictDomain :: DV r a -> ([a] -> IO [a]) -> AmbT r IO ()
+restrictDomain dv f = do
+ l' <- lift (domain dv >>= f)
+ when (null l') fail'
+ size <- lift $ domainSize dv
+ when (length l' < size) $ do
+ localWriteIORef (dvDomain dv) l'
+ constraints <- lift $ demons dv
+ sequence_ constraints
+
+-- | Add a constraint to the given variable.
+addConstraint :: DV r1 a -> Constraint r1 -> CSP r ()
+addConstraint dv c = csp $ modifyIORef (dvConstraints dv) (c :)
+
+-- | Assert a unary constraint.
+constraint1 :: (a -> Bool) -> DV r1 a -> CSP r ()
+constraint1 f dv = addConstraint dv $ restrictDomain dv $ (return . filter f)
+
+-- | Assert a binary constraint with arc consistency.
+constraint2 :: (a -> t1 -> Bool) -> DV t a -> DV t t1 -> CSP r ()
+constraint2 f x y = do
+ addConstraint x $
+ restrictDomain y
+ (\yd -> do
+ xd <- (domain x)
+ return $ filter (\ye -> any (\xe -> f xe ye) xd) yd)
+ addConstraint y $
+ restrictDomain x
+ (\xd -> do
+ yd <- (domain y)
+ return $ filter (\xe -> any (\ye -> f xe ye) yd) xd)
+
+-- | 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.
+constraint :: ([a] -> Bool) -> [DV r1 a] -> CSP r ()
+constraint f dvl =
+ mapM_ (\(dv1, k) ->
+ addConstraint dv1 $
+ (mapM_ (\(dv2, i) -> do
+ unless (i == k) $
+ restrictDomain dv2
+ (\d2 -> do
+ ddvl <- mapM domain dvl
+ return $ filter (\d2e ->
+ let loop [] es _ = f (reverse es)
+ loop (d:ds) es j | i == j = loop ds (d2e:es) (j + 1)
+ | otherwise = any (\e -> loop ds (e : es) (j + 1)) d
+ in loop ddvl [] 0) d2))
+ $ zip dvl ([1..] :: [Int])))
+ $ zip dvl ([1..] :: [Int])
+
+-- | Retrieve the current binding of a variable.
+binding :: DV t b -> IO b
+binding d = domain d >>= return . head
+
+-- | This extracts results from a CSP.
+class CSPResult a where
+ type Result a
+ result :: a -> IO (Result a)
+instance CSPResult (DV r a) where
+ type Result (DV r a) = a
+ result = binding
+instance (CSPResult a, CSPResult b) => CSPResult (a,b) where
+ type Result (a,b) = (Result a, Result b)
+ result (a,b) = do
+ a' <- result a
+ b' <- result b
+ return (a', b')
+instance (CSPResult a) => CSPResult [a] where
+ type Result [a] = [Result a]
+ result = mapM result
+
+-- | 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.
+solveCSP :: CSPResult a1 => (AmbT r IO (Result a1) -> IO a) -> CSP r a1 -> a
+solveCSP runAmb (CSP f) =
+ (unsafePerformIO $ runAmb $ do
+ dvcs <- lift $ newIORef []
+ r <- lift $ f dvcs
+ dvcs' <- lift $ readIORef dvcs
+ -- One round of applying all constraints
+ mapM_ dvcConstraints dvcs'
+ let loop [] = return ()
+ loop (d:ds) = do
+ dvcABinding d
+ filterM (liftM not . dvcIsBound) ds >>= loop
+ in filterM (liftM not . dvcIsBound) dvcs' >>= loop
+ lift $ result r >>= return)
+
+-- | Return a single solution to the CSP. 'solveCSP' running with 'oneValueT'
+oneCSPSolution :: CSPResult a1 => CSP (Result a1) a1 -> Result a1
+oneCSPSolution = solveCSP oneValueT
+
+-- | Return all solutions to the CSP. 'solveCSP' running with
+-- 'allValuesT'
+allCSPSolutions :: CSPResult a1 => CSP (Result a1) a1 -> [Result a1]
+allCSPSolutions = solveCSP allValuesT
diff --git a/LICENSE b/LICENSE
new file mode 100644
index 0000000..fc8a5de
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,165 @@
+ GNU LESSER GENERAL PUBLIC LICENSE
+ Version 3, 29 June 2007
+
+ Copyright (C) 2007 Free Software Foundation, Inc. <http://fsf.org/>
+ Everyone is permitted to copy and distribute verbatim copies
+ of this license document, but changing it is not allowed.
+
+
+ This version of the GNU Lesser General Public License incorporates
+the terms and conditions of version 3 of the GNU General Public
+License, supplemented by the additional permissions listed below.
+
+ 0. Additional Definitions.
+
+ As used herein, "this License" refers to version 3 of the GNU Lesser
+General Public License, and the "GNU GPL" refers to version 3 of the GNU
+General Public License.
+
+ "The Library" refers to a covered work governed by this License,
+other than an Application or a Combined Work as defined below.
+
+ An "Application" is any work that makes use of an interface provided
+by the Library, but which is not otherwise based on the Library.
+Defining a subclass of a class defined by the Library is deemed a mode
+of using an interface provided by the Library.
+
+ A "Combined Work" is a work produced by combining or linking an
+Application with the Library. The particular version of the Library
+with which the Combined Work was made is also called the "Linked
+Version".
+
+ The "Minimal Corresponding Source" for a Combined Work means the
+Corresponding Source for the Combined Work, excluding any source code
+for portions of the Combined Work that, considered in isolation, are
+based on the Application, and not on the Linked Version.
+
+ The "Corresponding Application Code" for a Combined Work means the
+object code and/or source code for the Application, including any data
+and utility programs needed for reproducing the Combined Work from the
+Application, but excluding the System Libraries of the Combined Work.
+
+ 1. Exception to Section 3 of the GNU GPL.
+
+ You may convey a covered work under sections 3 and 4 of this License
+without being bound by section 3 of the GNU GPL.
+
+ 2. Conveying Modified Versions.
+
+ If you modify a copy of the Library, and, in your modifications, a
+facility refers to a function or data to be supplied by an Application
+that uses the facility (other than as an argument passed when the
+facility is invoked), then you may convey a copy of the modified
+version:
+
+ a) under this License, provided that you make a good faith effort to
+ ensure that, in the event an Application does not supply the
+ function or data, the facility still operates, and performs
+ whatever part of its purpose remains meaningful, or
+
+ b) under the GNU GPL, with none of the additional permissions of
+ this License applicable to that copy.
+
+ 3. Object Code Incorporating Material from Library Header Files.
+
+ The object code form of an Application may incorporate material from
+a header file that is part of the Library. You may convey such object
+code under terms of your choice, provided that, if the incorporated
+material is not limited to numerical parameters, data structure
+layouts and accessors, or small macros, inline functions and templates
+(ten or fewer lines in length), you do both of the following:
+
+ a) Give prominent notice with each copy of the object code that the
+ Library is used in it and that the Library and its use are
+ covered by this License.
+
+ b) Accompany the object code with a copy of the GNU GPL and this license
+ document.
+
+ 4. Combined Works.
+
+ You may convey a Combined Work under terms of your choice that,
+taken together, effectively do not restrict modification of the
+portions of the Library contained in the Combined Work and reverse
+engineering for debugging such modifications, if you also do each of
+the following:
+
+ a) Give prominent notice with each copy of the Combined Work that
+ the Library is used in it and that the Library and its use are
+ covered by this License.
+
+ b) Accompany the Combined Work with a copy of the GNU GPL and this license
+ document.
+
+ c) For a Combined Work that displays copyright notices during
+ execution, include the copyright notice for the Library among
+ these notices, as well as a reference directing the user to the
+ copies of the GNU GPL and this license document.
+
+ d) Do one of the following:
+
+ 0) Convey the Minimal Corresponding Source under the terms of this
+ License, and the Corresponding Application Code in a form
+ suitable for, and under terms that permit, the user to
+ recombine or relink the Application with a modified version of
+ the Linked Version to produce a modified Combined Work, in the
+ manner specified by section 6 of the GNU GPL for conveying
+ Corresponding Source.
+
+ 1) Use a suitable shared library mechanism for linking with the
+ Library. A suitable mechanism is one that (a) uses at run time
+ a copy of the Library already present on the user's computer
+ system, and (b) will operate properly with a modified version
+ of the Library that is interface-compatible with the Linked
+ Version.
+
+ e) Provide Installation Information, but only if you would otherwise
+ be required to provide such information under section 6 of the
+ GNU GPL, and only to the extent that such information is
+ necessary to install and execute a modified version of the
+ Combined Work produced by recombining or relinking the
+ Application with a modified version of the Linked Version. (If
+ you use option 4d0, the Installation Information must accompany
+ the Minimal Corresponding Source and Corresponding Application
+ Code. If you use option 4d1, you must provide the Installation
+ Information in the manner specified by section 6 of the GNU GPL
+ for conveying Corresponding Source.)
+
+ 5. Combined Libraries.
+
+ You may place library facilities that are a work based on the
+Library side by side in a single library together with other library
+facilities that are not Applications and are not covered by this
+License, and convey such a combined library under terms of your
+choice, if you do both of the following:
+
+ a) Accompany the combined library with a copy of the same work based
+ on the Library, uncombined with any other library facilities,
+ conveyed under the terms of this License.
+
+ b) Give prominent notice with the combined library that part of it
+ is a work based on the Library, and explaining where to find the
+ accompanying uncombined form of the same work.
+
+ 6. Revised Versions of the GNU Lesser General Public License.
+
+ The Free Software Foundation may publish revised and/or new versions
+of the GNU Lesser General Public License from time to time. Such new
+versions will be similar in spirit to the present version, but may
+differ in detail to address new problems or concerns.
+
+ Each version is given a distinguishing version number. If the
+Library as you received it specifies that a certain numbered version
+of the GNU Lesser General Public License "or any later version"
+applies to it, you have the option of following the terms and
+conditions either of that published version or of any later version
+published by the Free Software Foundation. If the Library as you
+received it does not specify a version number of the GNU Lesser
+General Public License, you may choose any version of the GNU Lesser
+General Public License ever published by the Free Software Foundation.
+
+ If the Library as you received it specifies that a proxy can decide
+whether future versions of the GNU Lesser General Public License shall
+apply, that proxy's public statement of acceptance of any version is
+permanent authorization for you to choose that version for the
+Library.
diff --git a/README.md b/README.md
new file mode 100644
index 0000000..6866268
--- /dev/null
+++ b/README.md
@@ -0,0 +1,41 @@
+# CSP
+
+A simple example which solves Sudoku puzzles, project Euler problem 96.
+
+ 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]]
+
+ 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]]
+
+ 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
+
+ solveSudoku sudoku3
+
+## Future
+
+ - Docs!
+ - Allow a randomized execution order for CSPs
+ - CSPs don't need use IO internally. ST is enough.
+ - Constraint synthesis. Already facilitated by the fact that
+ constraints are internally nondeterministic
+ - Other constraint types for CSPs, right now only AC is implemented
+ - n-ary heterogeneous constraints
diff --git a/Setup.lhs b/Setup.lhs
new file mode 100644
index 0000000..6b32049
--- /dev/null
+++ b/Setup.lhs
@@ -0,0 +1,4 @@
+#! /usr/bin/env runhaskell
+
+> import Distribution.Simple
+> main = defaultMain
diff --git a/csp.cabal b/csp.cabal
new file mode 100644
index 0000000..97592d5
--- /dev/null
+++ b/csp.cabal
@@ -0,0 +1,23 @@
+Name: csp
+Version: 1.0
+Description: Constraint satisfaction problem (CSP) solvers
+License: LGPL
+License-file: LICENSE
+Author: Andrei Barbu <andrei@0xab.com>
+Maintainer: Andrei Barbu <andrei@0xab.com>
+Category: Control, AI, Constraints, Failure, Monads
+Build-Type: Simple
+cabal-version: >= 1.6
+synopsis:
+ Discrete constraint satisfaction problem (CSP) solvers.
+extra-source-files: README.md
+
+source-repository head
+ type: git
+ location: git://github.com/abarbu/csp-haskell.git
+
+Library
+ Build-Depends: base >= 3 && < 5, mtl >= 2, containers, nondeterminism
+ Exposed-modules:
+ Control.Monad.CSP
+ ghc-options: -Wall