diff --git a/Factor.hs b/Factor.hs --- a/Factor.hs +++ b/Factor.hs @@ -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 diff --git a/HC.hs b/HC.hs --- a/HC.hs +++ b/HC.hs @@ -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 diff --git a/QBF.hs b/QBF.hs deleted file mode 100644 --- a/QBF.hs +++ /dev/null @@ -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 diff --git a/VC.hs b/VC.hs --- a/VC.hs +++ b/VC.hs @@ -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 diff --git a/satchmo-examples.cabal b/satchmo-examples.cabal --- a/satchmo-examples.cabal +++ b/satchmo-examples.cabal @@ -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 +