satchmo-examples 1.4.1 → 1.8.1
raw patch · 5 files changed
+36/−94 lines, 5 filesdep −satchmo-funsatdep ~basedep ~satchmodep ~satchmo-backends
Dependencies removed: satchmo-funsat
Dependency ranges changed: base, satchmo, satchmo-backends
Files
- Factor.hs +3/−1
- HC.hs +8/−6
- QBF.hs +0/−71
- VC.hs +11/−7
- satchmo-examples.cabal +14/−9
Factor.hs view
@@ -2,6 +2,8 @@ -- | run like this: ./test/Factor 1000000000001 -- (takes 10 .. 20 seconds depending on your CPU) +{-# language PatternSignatures #-}+ import Prelude hiding ( not ) import Satchmo.Binary.Op.Fixed @@ -15,7 +17,7 @@ main :: IO () main = do [ n ] <- getArgs- res <- solve $ do+ res :: Maybe [ Integer ] <- solve $ do x <- Satchmo.Binary.Op.Flexible.constant $ read n a <- number $ width x notone a
HC.hs view
@@ -1,5 +1,9 @@-{-# language ScopedTypeVariables #-}+-- | compute Knight's tour on a rectangular chess board.+-- example usage: ./dist/build/HC/HC 8 8+-- should find and print a solution in < 10 seconds. +{-# language PatternSignatures #-}+ import Prelude hiding ( not ) import qualified Prelude @@ -48,8 +52,6 @@ j <- felder guard $ reaches j k return $ p ! (i,j) - - {- forM felder $ \ j -> forM felder $ \ k -> do@@ -61,12 +63,12 @@ return $ do a <- decode p return $ A.array ((1,1),(m,n)) $ do- ((i,p),True) <- A.assocs a+ ((i :: Int , p::(Int,Int)),True) <- A.assocs a return (p,i) -bijection :: (A.Ix a, A.Ix b) +bijection :: (A.Ix a, A.Ix b, MonadSAT m) => ((a,b),(a,b)) - -> SAT ( Relation a b )+ -> m ( Relation a b ) bijection bnd = do let ((u,l),(o,r)) = bnd a <- relation bnd
− QBF.hs
@@ -1,71 +0,0 @@--- | 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.Qube.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
VC.hs view
@@ -1,3 +1,10 @@+-- | command line arguments: n s+-- compute vertex cover of size <= s for knight's graph on n x n chess board.+-- (that is, if you put knights there, they control the full board)+-- example: VC 8 12++{-# language PatternSignatures #-}+ import Prelude hiding ( not ) import Satchmo.Relation@@ -5,22 +12,19 @@ import Satchmo.Boolean import Satchmo.Counting --- import Satchmo.Solver.Minisat-import Satchmo.Solver.Funsat+import Satchmo.Solver.Minisat+-- import Satchmo.Solver.Funsat 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.--- example: VC 8 12+import qualified Data.Array as A main :: IO () main = do argv <- getArgs let [ n, s ] = map read argv- Just a <- solve $ knight n s+ Just ( a :: A.Array (Int,Int) Bool ) <- solve $ knight n s putStrLn $ table a knight n s = do
satchmo-examples.cabal view
@@ -1,5 +1,5 @@ Name: satchmo-examples-Version: 1.4.1+Version: 1.8.1 License: GPL License-file: gpl-2.0.txt@@ -9,28 +9,33 @@ Synopsis: examples that show how to use satchmo description: examples that show how to use satchmo Category: Algorithms-Cabal-version: >= 1.2+Cabal-version: >= 1.6 Build-type: Simple Executable Factor Main-is: Factor.hs+ ghc-options: -threaded hs-source-dirs: .- Build-depends: satchmo>=1.4, satchmo-backends>=1.4, process, base, containers, array+ Build-depends: satchmo>=1.8, satchmo-backends>=1.8, process, base == 4.*, containers, array Executable HC Main-is: HC.hs+ ghc-options: -threaded hs-source-dirs: .- Build-depends: satchmo>=1.4, satchmo-backends>=1.4, process, base, containers, array+ Build-depends: satchmo>=1.8, satchmo-backends>=1.8, process, base == 4.*, containers, array Executable VC Main-is: VC.hs+ ghc-options: -threaded hs-source-dirs: .- Build-depends: satchmo>=1.4, satchmo-funsat>=1.4, process, base, containers, array+ Build-depends: satchmo>=1.8, satchmo-backends>=1.8, process, base == 4.*, containers, array -Executable QBF- Main-is: QBF.hs- hs-source-dirs: .- Build-depends: satchmo>=1.4, satchmo-backends>=1.4, process, base, containers, array+-- Executable QBF+-- Main-is: QBF.hs+-- ghc-options: -threaded+-- hs-source-dirs: .+-- Build-depends: satchmo>=1.8, satchmo-backends>=1.8, process, base == 4.*, containers, array+