csp (empty) → 1.0
raw patch · 5 files changed
+479/−0 lines, 5 filesdep +basedep +containersdep +mtlsetup-changed
Dependencies added: base, containers, mtl, nondeterminism
Files
- Control/Monad/CSP.hs +246/−0
- LICENSE +165/−0
- README.md +41/−0
- Setup.lhs +4/−0
- csp.cabal +23/−0
+ Control/Monad/CSP.hs view
@@ -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
+ LICENSE view
@@ -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.
+ README.md view
@@ -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
+ Setup.lhs view
@@ -0,0 +1,4 @@+#! /usr/bin/env runhaskell++> import Distribution.Simple+> main = defaultMain
+ csp.cabal view
@@ -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