satchmo-examples 1.3 → 1.4
raw patch · 3 files changed
+116/−16 lines, 3 filesdep +satchmo-backendsdep −satchmo-minisatdep ~satchmonew-component:exe:QBF
Dependencies added: satchmo-backends
Dependencies removed: satchmo-minisat
Dependency ranges changed: satchmo
Files
- HC.hs +37/−13
- QBF.hs +71/−0
- satchmo-examples.cabal +8/−3
HC.hs view
@@ -12,8 +12,9 @@ import Data.List (sort) import qualified Data.Array as A-import Control.Monad ( guard, when )+import Control.Monad ( guard, when, forM ) import System.Environment+import Data.Ix ( range) -- | command line arguments: m n -- compute knight's tour on m x n chess board@@ -34,19 +35,29 @@ tour m n = do let s = m * n+ felder = range ((1,1),(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) + forM ( zip [1..s] $ rotate 1 [1..s] ) $ \ (i,i') -> do+ forM felder $ \ j -> + assert $ not ( p!(i,j)) : do+ k <- felder+ guard $ reaches j k+ return $ p ! (i',k) + forM felder $ \ k -> + assert $ not ( p!(i',k)) : do+ j <- felder+ guard $ reaches j k+ return $ p ! (i,j) + ++{-+ forM felder $ \ j -> + forM felder $ \ k -> do+ c <- constant $ reaches j k+ assert [ not $ p!(i,j), not $ p!(i',k)+ , c+ ]+-} return $ do a <- decode p return $ A.array ((1,1),(m,n)) $ do@@ -59,13 +70,26 @@ bijection bnd = do let ((u,l),(o,r)) = bnd a <- relation bnd++ -- official encoding: exactly one per row, exactly one per column 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)++{-+ -- this should be enough: at least one per row, at most one per column+ sequence_ $ do+ x <- A.range (u,o)+ return $ assert $ do y <- A.range (l,r) ; return $ a!(x,y)+ sequence_ $ do+ y <- A.range (l,r)+ return $ monadic assert $ return $ atmost 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
+ QBF.hs view
@@ -0,0 +1,71 @@+-- | Simple state transition system:+-- a state is a list of Booleans,+-- a transition is the flip of exactly one bit.+--+-- Calling the main program with "./State w::Int d::Int"+-- produces the qbf for 'there is a path of length <= 2^d+-- from state False^w to state True^w'.+-- The formula size is linear in w*d.+-- Test cases: "./State 4 2" (satisfiable), "./State 5 2" (unsatisfiable).+--+-- Output is an element near the middle of the path.+-- You may check the about half the bits are flipped (if the depth bound is tight).++import Satchmo.Boolean+import Satchmo.Code+import Satchmo.Counting+import Satchmo.Solver.Quantor +import Satchmo.Solver.Qube ++import Prelude hiding ( not, and, or )++import Data.List ( tails )+import Data.Set ( Set )+import qualified Data.Set as S+import Control.Monad ( guard, forM )+import Data.Ix ( range )+import System.Environment++main = do+ argv <- getArgs+ let [ w, d ] = map read argv+ result <- Satchmo.Solver.Quantor.solve $ form w d+ print result++form :: Int -> Int -> SAT ( Decoder [ Bool ] )+form width depth = do+ start <- forM [ 1 .. width ] $ \ n -> constant False+ goal <- forM [ 1 .. width ] $ \ n -> constant True+ ( p, mid ) <- path depth start goal+ assert [ p ]+ return $ decode mid++-- | is there a path of length <= 2^depth ? +-- If so, the second component is a state from the middle of the path+path :: Int -> [ Boolean ] -> [ Boolean ] -> SAT ( Boolean, [ Boolean ] )+path depth from to =+ if depth > 0 + then do+ mid <- forM [ 1 .. length from ] $ \ _ -> exists+ p <- forM [ 1 .. length from ] $ \ _ -> forall+ q <- forM [ 1 .. length from ] $ \ _ -> forall+ pre <- monadic or [ monadic and [ equals from p , equals mid q ]+ , monadic and [ equals mid p , equals to q ]+ ]+ ( post, _ ) <- path (depth - 1) p q+ ok <- or [ not pre, post ]+ return ( ok, mid )+ else do+ ok <- monadic or [ onestep from to, equals from to ]+ return ( ok, from )++equals :: [ Boolean ] -> [ Boolean ] -> SAT Boolean+equals xs ys = monadic and + $ for ( zip xs ys ) $ \ (x,y) -> fmap not $ xor [x,y]++onestep :: [ Boolean ] -> [ Boolean ] -> SAT Boolean+onestep xs ys = do+ changes <- forM ( zip xs ys ) $ \ (x,y) -> xor [x,y]+ exactly 1 changes++for = flip map
satchmo-examples.cabal view
@@ -1,5 +1,5 @@ Name: satchmo-examples-Version: 1.3+Version: 1.4 License: GPL License-file: gpl-2.0.txt@@ -8,24 +8,29 @@ Homepage: http://dfa.imn.htwk-leipzig.de/satchmo/ Synopsis: examples that show how to use satchmo description: examples that show how to use satchmo+Category: Algorithms Cabal-version: >= 1.2 Build-type: Simple Executable Factor Main-is: Factor.hs hs-source-dirs: .- Build-depends: satchmo, satchmo-minisat, process, base, containers, array+ Build-depends: satchmo, satchmo-backends, process, base, containers, array Executable HC Main-is: HC.hs hs-source-dirs: .- Build-depends: satchmo, satchmo-minisat, process, base, containers, array+ Build-depends: satchmo, satchmo-backends, process, base, containers, array Executable VC Main-is: VC.hs hs-source-dirs: . Build-depends: satchmo, satchmo-funsat, process, base, containers, array +Executable QBF+ Main-is: QBF.hs+ hs-source-dirs: .+ Build-depends: satchmo>=1.4, satchmo-backends, process, base, containers, array