satchmo 1.2 → 1.3
raw patch · 14 files changed
+194/−472 lines, 14 files
Files
- Satchmo/Relation.hs +14/−0
- Satchmo/Relation/Data.hs +58/−0
- Satchmo/Relation/Op.hs +57/−0
- Satchmo/Relation/Prop.hs +51/−0
- Satchmo/Solve.hs +6/−19
- TODO +0/−11
- satchmo.cabal +8/−7
- test/Binary.hs +0/−79
- test/Cage.hs +0/−58
- test/Factor.hs +0/−32
- test/HC.hs +0/−76
- test/Ramsey.hs +0/−83
- test/Schur.hs +0/−65
- test/VC.hs +0/−42
+ Satchmo/Relation.hs view
@@ -0,0 +1,14 @@+{-# language FlexibleInstances, MultiParamTypeClasses #-}++module Satchmo.Relation ++( module Satchmo.Relation.Data+, module Satchmo.Relation.Op+, module Satchmo.Relation.Prop+)++where++import Satchmo.Relation.Data+import Satchmo.Relation.Op+import Satchmo.Relation.Prop
+ Satchmo/Relation/Data.hs view
@@ -0,0 +1,58 @@+{-# language FlexibleInstances, MultiParamTypeClasses #-}++module Satchmo.Relation.Data++( Relation, relation, build+, bounds, (!), indices+, table+) ++where++import Satchmo.Code+import Satchmo.Boolean++import qualified Data.Array as A+import Data.Array hiding ( bounds, (!), indices )++import Control.Monad ( guard )++data Relation a b = Relation ( Array (a,b) Boolean ) ++relation :: ( Ix a, Ix b ) + => ((a,b),(a,b)) -> SAT ( Relation a b ) +relation bnd = do+ pairs <- sequence $ do + p <- range bnd+ return $ do+ x <- boolean+ return ( p, x )+ return $ build bnd pairs++build :: ( Ix a, Ix b ) + => ((a,b),(a,b)) + -> [ ((a,b), Boolean ) ]+ -> Relation a b +build bnd pairs = Relation $ array bnd pairs++bounds :: (Ix a, Ix b) => Relation a b -> ((a,b),(a,b))+bounds ( Relation r ) = A.bounds r++indices ( Relation r ) = A.indices r++Relation r ! p = r A.! p++instance (Ix a, Ix b) => Decode ( Relation a b ) ( Array (a,b) Bool ) where+ decode ( Relation r ) = do+ decode r++table :: (Enum a, Ix a, Enum b, Ix b) + => Array (a,b) Bool -> String+table r = unlines $ do+ let ((a,b),(c,d)) = A.bounds r+ x <- [ a .. c ]+ return $ unwords $ do+ y <- [ b .. d ]+ return $ if r A.! (x,y) then "*" else "."++
+ Satchmo/Relation/Op.hs view
@@ -0,0 +1,57 @@+{-# language FlexibleInstances, MultiParamTypeClasses #-}++module Satchmo.Relation.Op++( mirror+, union+, complement+, product+) ++where++import Prelude hiding ( and, or, not, product )+import qualified Prelude++import Satchmo.Code+import Satchmo.Boolean+import Satchmo.Counting+import Satchmo.Relation.Data++import Control.Monad ( guard )+import Data.Ix++mirror :: ( Ix a , Ix b ) => Relation a b -> Relation b a+mirror r = + let ((a,b),(c,d)) = bounds r+ in build ((b,a),(d,c)) $ do (x,y) <- indices r ; return ((y,x), r!(x,y))++complement :: ( Ix a , Ix b ) => Relation a b -> Relation a b+complement r = + build (bounds r) $ do i <- indices r ; return ( i, not $ r!i )++union :: ( Ix a , Ix b ) + => Relation a b -> Relation a b + -> SAT ( Relation a b )+union r s = do+ pairs <- sequence $ do+ i <- indices r+ return $ do o <- or [ r!i, s!i ] ; return ( i, o )+ return $ build ( bounds r ) pairs++product :: ( Ix a , Ix b, Enum b, Ix c ) + => Relation a b -> Relation b c -> SAT ( Relation a c )+product a b = do+ let ((ao,al),(au,ar)) = bounds a+ ((bo,bl),(bu,br)) = bounds b+ bnd = ((ao,bl),(au,br))+ pairs <- sequence $ do+ i @ (x,z) <- range bnd+ return $ do+ o <- monadic or $ do+ y <- [ al .. ar ]+ return $ and [ a!(x,y), b!(y,z) ]+ return ( i, o )+ return $ build bnd pairs++
+ Satchmo/Relation/Prop.hs view
@@ -0,0 +1,51 @@+module Satchmo.Relation.Prop++( implies+, symmetric +, transitive+, irreflexive+, regular+)++where++import Prelude hiding ( and, or, not, product )+import qualified Prelude++import Satchmo.Code+import Satchmo.Boolean+import Satchmo.Counting+import Satchmo.Relation.Data+import Satchmo.Relation.Op++import Control.Monad ( guard )+import Data.Ix++implies :: ( Ix a, Ix b ) => Relation a b -> Relation a b -> SAT Boolean+implies r s = monadic and $ do+ i <- indices r+ return $ or [ not $ r ! i, s ! i ]+++symmetric :: (Enum a, Ix a) => Relation a a -> SAT Boolean+symmetric r = implies r ( mirror r )++irreflexive :: (Enum a, Ix a) => Relation a a -> SAT Boolean+irreflexive r = and $ do+ let ((a,b),(c,d)) = bounds r+ x <- [a .. c]+ return $ Satchmo.Boolean.not $ r ! (x,x) ++regular :: (Enum a, Ix a) => Int -> Relation a a -> SAT Boolean+regular deg r = monadic and $ do+ let ((a,b),(c,d)) = bounds r+ x <- [ a .. c ]+ return $ exactly deg $ do + y <- [ b .. d ]+ return $ r !(x,y)++transitive :: ( Enum a, Ix a ) + => Relation a a -> SAT Boolean+transitive r = do+ r2 <- product r r+ implies r2 r
Satchmo/Solve.hs view
@@ -1,6 +1,7 @@ module Satchmo.Solve ( solve+, Implementation , Decoder ) @@ -15,14 +16,15 @@ import Control.Monad.State import Control.Monad.Reader-import System.Process +type Implementation = String -> IO ( Maybe ( Map Literal Bool ) ) -solve :: SAT ( Decoder a )+solve :: Implementation+ -> SAT ( Decoder a ) -> IO ( Maybe a )-solve build = do+solve implementation build = do let (s, a) = sat build- mfm <- run s+ mfm <- implementation s case mfm of Nothing -> do putStrLn "not satisfiable"@@ -32,18 +34,3 @@ -- print fm return $ Just $ runReader a fm -run :: String -> IO ( Maybe ( Map Literal Bool ) )-run cs = do- let debug = False- if debug - then putStrLn cs- else putStrLn $ head $ lines cs- ( code, stdout, stderr ) <- - readProcessWithExitCode "minisat" [ "/dev/stdin", "/dev/stdout" ] cs- when debug $ putStrLn stdout- case lines stdout of- "SAT" : xs : _ -> return $ Just $ M.fromList $ do- x <- takeWhile ( /= 0 ) $ map read $ words xs- let l = literal $ abs x- return ( l, x > 0 )- _ -> return $ Nothing
− TODO
@@ -1,11 +0,0 @@-* minisat needs to be in the $PATH (for execution),- this should be checked during installation.--* should provide several backends (separate package satchmo-minisat etc.,- similar as hsql with backends like hsql-mysql etc.)--* add timeout handler for calling the SAT solver.- --* implement fixed-width integer arithmetics-
satchmo.cabal view
@@ -1,5 +1,6 @@ Name: satchmo-Version: 1.2+Version: 1.3+ License: GPL License-file: gpl-2.0.txt Author: Johannes Waldmann@@ -8,9 +9,10 @@ Synopsis: SAT encoding monad description: Encoding for boolean and integral constraints into CNF-SAT. The encoder is provided as a State monad (hence the "mo" in "satchmo").- Requires SAT solver "minisat" installed.+ requires a backend (e.g. satchmo-minisat, satchmo-funsat) Build-depends: mtl, process, containers, base, array Exposed-modules:+ Satchmo.Data Satchmo.Solve Satchmo.Boolean Satchmo.Counting@@ -19,16 +21,15 @@ Satchmo.Binary.Op.Common Satchmo.Binary.Op.Fixed Satchmo.Binary.Op.Flexible+ Satchmo.Relation+ Satchmo.Relation.Data+ Satchmo.Relation.Op+ Satchmo.Relation.Prop Other-modules: Satchmo.Binary.Data Satchmo.Boolean.Op Satchmo.Boolean.Data Satchmo.Internal- Satchmo.Data hs-source-dirs: .-extra-source-files: test/Binary.hs test/HC.hs test/Schur.hs- test/Factor.hs- test/Cage.hs test/Ramsey.hs test/VC.hs- TODO extensions: build-type: Simple
− test/Binary.hs
@@ -1,79 +0,0 @@--- | run tests (in ghci) like this: "solve test2"--import Prelude hiding ( not )--import Satchmo.Boolean hiding ( constant )-import Satchmo.Code--import Satchmo.Binary.Op.Fixed--- import Satchmo.Binary.Op.Flexible--import Satchmo.Solve---assert_positive x = do - n <- constant 0 - e <- equals n x - assert [ not e ]--assert_equals x y = do - e <- equals x y - assert [ e ]--assert_lt x y = do - d <- number $ width y- assert_positive d- xd <- add x d- assert_equals xd y--test1 = do - x <- number 4 - y <- constant 12 - assert_equals x y- return $ decode (x,y)--test2 = do - x <- constant 3- y <- constant 9- z <- add x y- return $ decode [x,y,z]--test3 = do - x <- number 5 - xx <- add x x- xxx <- add xx x- y <- constant 15 - assert_equals xxx y - return $ decode [ x, y ]--test4 = do - x <- number 8- y <- number 8- xy <- times x y- z <- constant 63- assert_equals xy z- return $ decode [x, y, z]--test5 = do - x <- number 10- y <- number 10- xy <- times x y- z <- constant 1001- assert_equals xy z- return $ decode [x, y, z]--ramanujan = do- let bits = 11- a <- number bits- b <- number bits- c <- number bits- d <- number bits-- assert_lt a c ; assert_lt c d ; assert_lt d b-- let cube x = do x2 <- times x x ; times x2 x- a3 <- cube a; b3 <- cube b; ab <- add a3 b3- c3 <- cube c; d3 <- cube d; cd <- add c3 d3- assert_equals ab cd-- return $ decode [a,b,c,d]
− test/Cage.hs
@@ -1,58 +0,0 @@-import Prelude hiding ( not )--import Satchmo.Relation-import Satchmo.Code-import Satchmo.Boolean-import Satchmo.Counting-import Satchmo.Solve--import Data.List ( inits, tails )-import System.Environment---- | command line arguments: r g n--- program looks for a (r,g) cage:--- r-regular graph with girth g on n nodes--main :: IO ()-main = do- argv <- getArgs- let [ r, g, n ] = map read argv- Just a <- solve $ cage r g n- putStrLn $ table a--type Graph = Relation Int Int--cage r g n = do- a <- relation ((1,1),(n,n))- monadic assert [ symmetric a ]- monadic assert [ irreflexive a ]- monadic assert [ regular r a ]- girth_at_least g a- return $ decode a--girth_at_least :: Int -> Graph -> SAT ()-girth_at_least k g = sequence_ $ do- let ((lo,_),(hi,_)) = bounds g- c <- [ 3 .. k-1 ]- xs <- sublists c [lo .. hi]- return $ assert_no_circle xs g- -assert_no_circle xs g = - assert $ do - (x,y) <- zip xs $ rotate 1 xs- return $ not $ g ! (x,y)- -sublists :: Int -> [a] -> [[a]]-sublists 0 xs = return []-sublists k xs = do- ( pre, this : post ) <- splits xs- that <- sublists (k-1) $ pre ++ post- return $ this : that--splits :: [a] -> [ ([a],[a]) ]-splits xs = zip ( inits xs ) ( tails xs )--rotate :: Int -> [a] -> [a]-rotate k xs = - let ( pre, post ) = splitAt k xs- in post ++ pre
− test/Factor.hs
@@ -1,32 +0,0 @@--- | attempt factorization of integer.--- | run like this: ./test/Factor 1000000000001--- (takes 10 .. 20 seconds depending on your CPU)--import Prelude hiding ( not )--import Satchmo.Binary.Op.Fixed -import qualified Satchmo.Binary.Op.Flexible -import Satchmo.Solve-import Satchmo.Boolean -import Satchmo.Code--import System.Environment--main :: IO ()-main = do- [ n ] <- getArgs- res <- solve $ do- x <- Satchmo.Binary.Op.Flexible.constant $ read n- a <- number $ width x - notone a- b <- number $ width x - notone b- ab <- times a b- monadic assert [ equals ab x ]- return $ decode [ a, b ]- print res--notone f = do- one <- Satchmo.Binary.Op.Flexible.constant 1- e <- equals f one- assert [ not e ]
− test/HC.hs
@@ -1,76 +0,0 @@-{-# language ScopedTypeVariables #-}--import Prelude hiding ( not )-import qualified Prelude--import Satchmo.Relation-import Satchmo.Code-import Satchmo.Boolean-import Satchmo.Counting-import Satchmo.Solve--import Data.List (sort)-import qualified Data.Array as A-import Control.Monad ( guard, when )-import System.Environment---- | command line arguments: m n--- compute knight's tour on m x n chess board--main :: IO ()-main = do- argv <- getArgs- let [ m, n ] = map read argv- Just a <- solve $ tour m n- putStrLn $ unlines $ do- let ((u,l),(o,r)) = A.bounds a- x <- [u .. o]- return $ unwords $ do - y <- [ l ..r ]- return $ fill 4 $ show $ a A.! (x,y)--fill k cs = replicate (k - length cs) ' ' ++ cs--tour m n = do- let s = m * n- p :: Relation Int (Int,Int) <- bijection ((1,(1,1)), (s,(m,n)))- sequence_ $ do- (i,j) <- zip [1..s] $ rotate 1 [1..s]- a <- A.range ((1,1),(m,n))- return $ do- assert $ not ( p!(i,a)) : do- b <- A.range ((1,1),(m,n))- guard $ reaches a b- return $ p ! (j,b) - assert $ not ( p!(j,a)) : do- b <- A.range ((1,1),(m,n))- guard $ reaches a b- return $ p ! (i,b) - return $ do- a <- decode p- return $ A.array ((1,1),(m,n)) $ do- ((i,p),True) <- A.assocs a- return (p,i)--bijection :: (A.Ix a, A.Ix b) - => ((a,b),(a,b)) - -> SAT ( Relation a b )-bijection bnd = do- let ((u,l),(o,r)) = bnd- a <- relation bnd- sequence_ $ do- x <- A.range (u,o)- return $ monadic assert $ return $ exactly 1 $ do y <- A.range (l,r) ; return $ a!(x,y)- sequence_ $ do- y <- A.range (l,r)- return $ monadic assert $ return $ exactly 1 $ do x <- A.range (u,o) ; return $ a!(x,y)- return a --reaches (px,py) (qx,qy) = - 5 == (px - qx)^2 + (py - qy)^2--rotate :: Int -> [a] -> [a]-rotate k xs = - let ( pre, post ) = splitAt k xs- in post ++ pre-
− test/Ramsey.hs
@@ -1,83 +0,0 @@-import Prelude hiding ( not )-import qualified Prelude--import Satchmo.Relation-import Satchmo.Code-import Satchmo.Boolean-import Satchmo.Counting-import Satchmo.Solve--import Data.List ( inits, tails )-import Data.Ix-import qualified Data.Array as A-import Control.Monad ( forM, guard )-import System.Environment---- | command line arguments: c_1 .. c_k n--- program prints graph g that proves--- R(c_1, .., c_k) > n--main :: IO ()-main = do- argv <- fmap ( map read ) getArgs- let cs = init argv- n = last argv- Just a <- solve $ ramsey cs n- print a--type Graph = Relation Int Int--ramsey cs n = do- cols <- sequence $ replicate (length cs) $ do- r <- relation ((1,1),(n,n))- monadic assert [ symmetric r ]- monadic assert [ irreflexive r ]- return r- circular_colouring ( n `div` length cs ) cols- each_edge_is_coloured n cols- forM ( zip cs cols ) no_monochromatic_clique- return $ do- ds <- mapM decode cols- return $ do- i <- range ((1,1),(n,n))- let c = length $ takeWhile Prelude.not $ do d <- ds ; return $ d A.! i- return ( i, c )--circular_colouring period cols = sequence_ $ do- (col, col') <- zip cols $ rotate 1 cols- x @ (p,q) <- indices col- let y = (p+period,q+period)- guard $ inRange ( bounds col ) y- return $ do- assert [ not $ col ! x, col' ! y ]--rotate :: Int -> [a] -> [a]-rotate k xs = - let ( pre, post ) = splitAt k xs- in post ++ pre--each_edge_is_coloured n cols = sequence_ $ do- (p,q) <- range ((1,1),(n,n))- guard $ p < q- return $ assert $ do - col <- cols- return $ col ! (p,q)--no_monochromatic_clique (c, col) = sequence_ $ do- let ((lo,_),(hi,_)) = bounds col- xs <- ordered_sublists c [lo .. hi]- return $ assert $ do- x : ys <- tails xs- y <- ys- return $ not $ col!(x,y)--ordered_sublists :: Int -> [a] -> [[a]]-ordered_sublists 0 xs = return []-ordered_sublists k xs = do- ( pre, this : post ) <- splits xs- that <- ordered_sublists (k-1) $ post- return $ this : that--splits :: [a] -> [ ([a],[a]) ]-splits xs = zip ( inits xs ) ( tails xs )-
− test/Schur.hs
@@ -1,65 +0,0 @@-import Prelude hiding ( not, or, and )--import Satchmo.Relation-import Satchmo.Code-import Satchmo.Boolean-import Satchmo.Counting-import Satchmo.Solve--import Data.List ( inits, tails )-import qualified Data.Array as A-import System.Environment-import Control.Monad ( guard, forM_ )---- | command line arguments: c n--- program looks for sum-free c-colouring of [1 .. n]--main :: IO ()-main = do- argv <- getArgs- let [ c, n ] = map read argv- Just a <- solve $ schur c n- putStrLn $ table a- print $ do- o <- [ 1 .. c ]- return ( o, length $ do i <- [ 1 .. n ]; guard $ a A.! (i,o) )--schur c n = do- col <- relation ((1,1),(n,c))- each_number_coloured col- sum_free_colouring col- return $ decode col--periodic p col = sequence_ $ do- let ((1,1),(n,c)) = bounds col- x <- [ 1 .. n ]- let y = x + p- guard $ y <= n- o <- [ 1 .. c ]- let p = 1 + o `mod` c- return $ assert [ not $ col!(x,o), col!(y,p) ]--each_number_coloured col = sequence_ $ do- let ((1,1),(n,c)) = bounds col- x <- [ 1 .. n ]- return $ assert $ do o <- [1 .. c]; return $ col!(x,o)--sum_free_colouring col = sequence_ $ do- let ((1,1),(n,c)) = bounds col- x <- [ 1 .. n ]- y <- [ x .. n ]- let z = (x + y) `mod` (n+1)- guard $ z <= n- guard $ 1 <= z- o <- [1 .. c]- return $ assert $ do - p <- [ x, y, z ]- return $ not $ col!(p,o)--evenly_distributed col = do- let ((1,1),(n,c)) = bounds col- d = n `div` c- forM_ [ 1 .. c ] $ \ o -> do- a <- atleast d $ do i <- [ 1 .. n ] ; return $ col!(i,o)- assert [a]-
− test/VC.hs
@@ -1,42 +0,0 @@-import Prelude hiding ( not )--import Satchmo.Relation-import Satchmo.Code-import Satchmo.Boolean-import Satchmo.Counting-import Satchmo.Solve--import Control.Monad ( guard )-import System.Environment-import System.Timeout---- | command line arguments: n s--- compute vertex cover of size <= s for knight's graph on n x n chess board--main :: IO ()-main = do- argv <- getArgs- let [ n, s ] = map read argv- -- this is just to check whether time-outing works- -- Just (Just a) <- timeout (10^6) $ solve $ knight n s-- Just a <- solve $ knight n s- putStrLn $ table a--knight n s = do- a <- relation ((1,1),(n,n))- m <- atmost s $ do - i <- indices a ; return $ a ! i- assert [m]- sequence_ $ do- p <- indices a- return $ assert $ do- q <- indices a- guard $ p == q || reaches p q- return $ a!q- return $ decode a- -reaches (px,py) (qx,qy) = - 5 == (px - qx)^2 + (py - qy)^2--