satchmo 1.0 → 1.1

raw patch · 10 files changed

+298/−142 lines, 10 files

Files

• Satchmo/Binary.hs +2/−120
• Satchmo/Binary/Data.hs +74/−0
• Satchmo/Binary/Op/Fixed.hs +90/−0
• Satchmo/Binary/Op/Flexible.hs +63/−0
• Satchmo/Boolean/Data.hs +4/−1
• TODO +6/−3
• satchmo.cabal +9/−5
• test/Binary.hs +15/−12
• test/Factor.hs +32/−0
• test/VC.hs +3/−1

@@ -2,127 +2,9 @@  module Satchmo.Binary  -( Number, width, number, fixed-, add, times-, equals+( module Satchmo.Binary.Op.Flexible )  where -import Prelude hiding ( and, or, not )--import qualified Satchmo.Code as C-import Satchmo.Boolean-import Satchmo.Counting--type Booleans = [ Boolean ]--data Number = Number -            { encode :: Booleans -- lsb first-            , decode :: C.Decoder Integer-            }--instance C.Decode Number Integer where-    decode = decode--width :: Number -> Int-width n = length $ encode n---- | declare a number variable (bit width)-number :: Int -> SAT Number-number w = do-    xs <- sequence $ replicate w boolean-    return $ make xs--make :: [ Boolean ] -> Number-make xs = Number-           { encode = xs-           , decode = do ys <- mapM C.decode xs ; return $ fromBinary ys-           }--fromBinary :: [ Bool ] -> Integer-fromBinary xs = foldr ( \ x y -> 2*y + if x then 1 else 0 ) 0 xs--toBinary :: Int -> Integer -> [ Bool ]-toBinary 0 0 = []-toBinary b n | b > 0 = -    let (d,m) = divMod n 2-    in  toEnum ( fromIntegral m ) : toBinary (b-1) d---- | declare a number constant (bit width, value)-fixed :: Int -> Integer -> SAT Number-fixed b n = do-    xs <- mapM constant $ toBinary b n-    return $ make xs---- | result width is 1 + largest argument width-add :: Number -> Number -> SAT Number-add ( Number { encode = xs } ) ( Number { encode = ys } ) = do-    false <- constant False-    ( zs, carry ) <- add_with_carry false xs ys-    return $ make $ zs ++ [carry]---- | result width is largest argument width--- if overflow, then unsatisfiable-restricted_add :: Number -> Number -> SAT Number -restricted_add a b = do-    c <- add a b-    restricted ( max (width a) (width b)) c---- | give only lower k bits, upper bits must be zero,--- (else unsatisfiable)-restricted :: Int -> Number -> SAT Number-restricted w ( Number { encode = xs } ) = do-    let ( low, high ) = splitAt w xs-    sequence $ do x <- high ; return $ assert [ not x ]-    return $ make low---- | result has max length of both inputs-add_with_carry :: Boolean -               -> Booleans -> Booleans-               -> SAT ( Booleans, Boolean )-add_with_carry cin [] [] = return ( [], cin )-add_with_carry cin (x:xs) [] = do-    z <- xor [ cin, x ]-    c <- and [ cin, x ]-    ( zs, cout ) <- add_with_carry c xs []-    return ( z : zs, cout )-add_with_carry cin [] (y:ys) = do-    add_with_carry cin (y:ys) []-add_with_carry cin (x:xs ) (y:ys) = do-    z  <- xor [ cin, x, y ]-    c <- atleast 2 [ cin, x, y ]-    ( zs, cout ) <- add_with_carry c xs ys-    return ( z : zs, cout )--times :: Number -> Number -> SAT Number-times ( Number { encode = [x] } ) ys = times1 x ys-times ( Number { encode = x:xs } ) ys = do-    xys  <- times1 x ys-    xsys <- times (make xs) ys-    zs <- shift xsys-    add xys zs---- | multiply by 2-shift :: Number -> SAT Number-shift ( Number { encode = xs } ) = do-    false <- constant False -    return $ make $ false : xs--times1 :: Boolean -> Number -> SAT Number-times1 x ( Number { encode = ys } ) = do-    zs <- mapM ( \ y -> and [x,y] ) ys-    return $ make zs--equals :: Number -> Number -> SAT Boolean-equals ( Number { encode = xs } ) ( Number { encode = ys } ) = do-    equals' xs ys--equals' :: Booleans -> Booleans -> SAT Boolean-equals' [] [] = constant True-equals' (x:xs) (y:ys) = do-    z <- xor [x, y]-    rest <- equals' xs ys-    and [ not z, rest ]-equals' xs [] = and $ map not xs-equals' [] ys = and $ map not ys+import Satchmo.Binary.Op.Flexible

@@ -0,0 +1,74 @@+{-# language MultiParamTypeClasses #-}++module Satchmo.Binary.Data++( Number, bits, make+, width, number, constant+, equals, iszero+)++where++import Prelude hiding ( and, or, not )++import qualified Satchmo.Code as C++import Satchmo.Boolean hiding ( constant )+import qualified  Satchmo.Boolean as B++import Satchmo.Counting++data Number = Number +            { bits :: [ Boolean ] -- lsb first+            , decode :: C.Decoder Integer+            }++instance C.Decode Number Integer where+    decode = decode++width :: Number -> Int+width n = length $ bits n++-- | declare a number variable (bit width)+number :: Int -> SAT Number+number w = do+    xs <- sequence $ replicate w boolean+    return $ make xs++make :: [ Boolean ] -> Number+make xs = Number+           { bits = xs+           , decode = do ys <- mapM C.decode xs ; return $ fromBinary ys+           }++fromBinary :: [ Bool ] -> Integer+fromBinary xs = foldr ( \ x y -> 2*y + if x then 1 else 0 ) 0 xs++toBinary :: Integer -> [ Bool ]+toBinary 0 = []+toBinary n  = +    let (d,m) = divMod n 2+    in  toEnum ( fromIntegral m ) : toBinary d++-- | declare a number constant +constant :: Integer -> SAT Number+constant n = do+    xs <- mapM B.constant $ toBinary n+    return $ make xs++iszero :: Number -> SAT Boolean+iszero a = equals a $ make []++equals :: Number -> Number -> SAT Boolean+equals a b = do+    equals' ( bits a ) ( bits b )++equals' :: Booleans -> Booleans -> SAT Boolean+equals' [] [] = B.constant True+equals' (x:xs) (y:ys) = do+    z <- xor [x, y]+    rest <- equals' xs ys+    and [ not z, rest ]+equals' xs [] = and $ map not xs+equals' [] ys = and $ map not ys+

@@ -0,0 +1,90 @@+{-# language MultiParamTypeClasses #-}++-- | operations with fixed bit width.+-- still they are non-overflowing:+-- if overflow occurs, the constraints are not satisfiable.+-- the bit width of the result of binary operations+-- is the max of the bit width of the inputs.++module Satchmo.Binary.Op.Fixed++( restricted+, add, times+, module Satchmo.Binary.Data+)++where++import Prelude hiding ( and, or, not )++import qualified Satchmo.Code as C++import Satchmo.Boolean+import Satchmo.Binary.Data+import qualified Satchmo.Binary.Op.Flexible as Flexible++import Satchmo.Counting++-- | give only lower k bits, upper bits must be zero,+-- (else unsatisfiable)+restricted :: Int -> Number -> SAT Number+restricted w a = do+    let ( low, high ) = splitAt w $ bits a+    sequence $ do x <- high ; return $ assert [ not x ]+    return $ make low++-- | result bit width is max of argument bit widths.+-- if overflow occurs, then formula is unsatisfiable.+add :: Number -> Number -> SAT Number+add a b = do+    false <- Satchmo.Boolean.constant False+    let w = max ( width a ) ( width b )+    zs <- add_with_carry w false ( bits a ) ( bits b )+    return $ make zs ++add_with_carry :: Int -> Boolean -> Booleans -> Booleans -> SAT Booleans+add_with_carry w c xxs yys = case ( xxs, yys ) of+    _ | w <= 0 -> do+        sequence_ $ do p <- c : xxs ++ yys ; return $ assert [ not p ]+        return []+    ( [] , [] ) -> return [ c ]+    ( [], y : ys) -> do+        r <- xor [ c, y ]+        d <- and [ c, y ]+        rest <- add_with_carry (w-1) d [] ys+        return $ r : rest+    ( x : xs, [] ) -> add_with_carry w c yys xxs+    (x : xs, y:ys) -> do+        r <- xor [c,x,y]+        d <- atleast 2 [c,x,y]+        rest <- add_with_carry (w-1) d xs ys+        return $ r : rest++-- | result bit width is at most max of argument bit widths.+-- if overflow occurs, then formula is unsatisfiable.+times :: Number -> Number -> SAT Number+times a b = do +    let w = max ( width a ) ( width b ) +    restricted_times w a b++restricted_times :: Int -> Number -> Number -> SAT Number+restricted_times w a b = case bits a of+    [] -> return $ make []+    _ | w <= 0 -> do+        monadic assert [ Flexible.iszero a, Flexible.iszero b ]+        return $ make []+    x : xs -> do +        xys  <- Flexible.times1 x b+        xsys <- if null $ bits b +                then return $ make [] +                else do+                       zs <- restricted_times (w-1) b (make xs)+                       Flexible.shift zs+        s <- Flexible.add xys xsys+        restricted w s++        ++++

@@ -0,0 +1,63 @@+{-# language MultiParamTypeClasses, PatternGuards #-}++-- | operations from this module cannot overflow.+-- instead they increase the bit width.++module Satchmo.Binary.Op.Flexible++( add, times+, add_with_carry, times1, shift+, module Satchmo.Binary.Data+)++where++import Prelude hiding ( and, or, not )++import Satchmo.Boolean+import qualified Satchmo.Code as C+import Satchmo.Binary.Data+import Satchmo.Counting++add :: Number -> Number -> SAT Number+add a b = do+    false <- Satchmo.Boolean.constant False+    ( zs, carry ) <- add_with_carry false (bits a) (bits b)+    return $ make $ zs ++ [carry]++add_with_carry :: Boolean +               -> Booleans -> Booleans+               -> SAT ( Booleans, Boolean )+add_with_carry cin [] [] = return ( [], cin )+add_with_carry cin (x:xs) [] = do+    z <- xor [ cin, x ]+    c <- and [ cin, x ]+    ( zs, cout ) <- add_with_carry c xs []+    return ( z : zs, cout )+add_with_carry cin [] (y:ys) = do+    add_with_carry cin (y:ys) []+add_with_carry cin (x:xs ) (y:ys) = do+    z  <- xor [ cin, x, y ]+    c <- atleast 2 [ cin, x, y ]+    ( zs, cout ) <- add_with_carry c xs ys+    return ( z : zs, cout )++times :: Number -> Number -> SAT Number+times a b | [x] <- bits a = times1 x b+times a b | x:xs <- bits a = do+    xys  <- times1 x b+    xsys <- times (make xs) b+    zs <- shift xsys+    add xys zs++-- | multiply by 2+shift :: Number -> SAT Number+shift a = do+    false <- Satchmo.Boolean.constant False +    return $ make $ false : bits a++times1 :: Boolean -> Number -> SAT Number+times1 x b = do+    zs <- mapM ( \ y -> and [x,y] ) $ bits b+    return $ make zs+

@@ -2,7 +2,8 @@  module Satchmo.Boolean.Data  -( Boolean, boolean, constant+( Boolean, Booleans+, boolean, constant , not, assert, monadic ) @@ -28,6 +29,8 @@              , decode :: C.Decoder Bool              }      | Constant { value :: Bool }++type Booleans = [ Boolean ]  isConstant :: Boolean -> Bool isConstant ( Constant {} ) = True

@@ -1,8 +1,11 @@ * minisat needs to be in the $PATH (for execution),-  but this is not checked during installation.+  this should be checked during installation. -* actually, should provide several backends (separate package satchmo-minisat etc.,+* should provide several backends (separate package satchmo-minisat etc.,   similar as hsql with backends like hsql-mysql etc.) -* need timeout handler for calling the SAT solver.+* add timeout handler for calling the SAT solver.+  ++* implement fixed-width integer arithmetics 

@@ -1,5 +1,5 @@ Name:           satchmo-Version:        1.0+Version:        1.1 License:        GPL License-file:	gpl-2.0.txt Author:         Johannes Waldmann@@ -9,21 +9,25 @@ 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 SAT solver "minisat" installed. Build-depends:  mtl, process, containers, base, array Exposed-modules:-        Satchmo.Boolean         Satchmo.Solve+        Satchmo.Boolean 	Satchmo.Counting-	Satchmo.Binary 	Satchmo.Code+	Satchmo.Binary+	Satchmo.Binary.Op.Fixed+	Satchmo.Binary.Op.Flexible Other-modules:+	Satchmo.Binary.Data+        Satchmo.Boolean.Op         Satchmo.Boolean.Data-	Satchmo.Boolean.Op 	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: 

@@ -2,14 +2,17 @@  import Prelude hiding ( not ) -import Satchmo.Boolean+import Satchmo.Boolean hiding ( constant ) import Satchmo.Code-import Satchmo.Binary++import Satchmo.Binary.Op.Fixed+-- import Satchmo.Binary.Op.Flexible+ import Satchmo.Solve   assert_positive x = do -    n <- fixed 0 0 +    n <- constant 0      e <- equals n x      assert [ not e ] @@ -25,13 +28,13 @@  test1 = do      x <- number 4 -    y <- fixed 4 12 +    y <- constant 12      assert_equals x y     return $ decode (x,y)  test2 = do -    x <- fixed 5 3-    y <- fixed 5 9+    x <- constant 3+    y <- constant 9     z <- add x y     return $ decode [x,y,z] @@ -39,7 +42,7 @@     x <- number 5      xx <- add x x     xxx <- add xx x-    y <- fixed 5 15 +    y <- constant 15      assert_equals xxx y      return $ decode [ x, y ] @@ -47,20 +50,20 @@     x <- number  8     y <- number  8     xy <- times x y-    z <- fixed 8 63+    z <- constant 63     assert_equals xy z     return $ decode [x, y, z]  test5 = do -    x <- number  8-    y <- number  8+    x <- number  10+    y <- number  10     xy <- times x y-    z <- fixed 10 1001+    z <- constant 1001     assert_equals xy z     return $ decode [x, y, z]  ramanujan = do-    let bits = 5+    let bits = 11     a <- number  bits     b <- number  bits     c <- number  bits

@@ -0,0 +1,32 @@+-- | 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 ]

@@ -8,6 +8,7 @@  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@@ -16,7 +17,8 @@ main = do     argv <- getArgs     let [ n, s ] = map read argv-    Just a <- solve $ knight n s+    -- this is just to check whether time-outing works+    Just (Just a) <- timeout (10^6) $ solve $ knight n s     putStrLn $ table a  knight n s = do