packages feed

satchmo 2.9.6 → 2.9.7

raw patch · 6 files changed

+373/−18 lines, 6 filesdep +lensdep ~base

Dependencies added: lens

Dependency ranges changed: base

Files

Satchmo/Data.hs view
@@ -1,24 +1,36 @@ {-# language TypeFamilies #-}+{-# language GeneralizedNewtypeDeriving #-}  module Satchmo.Data  -( CNF, cnf, clauses--- FIXME: exports should be abstract-, Clause(..), clause, literals-, Literal (..), literal, nicht, positive, variable+( CNF, cnf, singleton, clauses, foldr, filter, size+, Clause, clause, literals, without+, Literal, literal, nicht, positive, variable , Variable  )  where -import Control.Monad.State.Strict+import Prelude hiding ( foldr, filter )+import qualified Prelude+  +import qualified Data.Set as S+import qualified Data.Map as M+import qualified Data.Foldable as F+import Data.Monoid+import Data.List ( nub )  type Variable = Int -data Literal = Literal { variable :: Variable , positive :: Bool }+data Literal =+     Literal { variable :: ! Variable+             , positive :: ! Bool+             }+     deriving ( Eq, Ord )  instance Show Literal where-    show l = ( if positive l then "" else "-" ) ++ show ( variable l )+    show l = ( if positive l then "" else "-" )+             ++ show ( variable l )  literal :: Bool -> Variable -> Literal literal pos v  = Literal { positive = pos, variable = v }@@ -26,21 +38,58 @@ nicht :: Literal -> Literal  nicht x = x { positive = not $ positive x } -newtype CNF     = CNF { clauses :: [ Clause ] }+newtype CNF  = CNF ( S.Set Clause )+    deriving ( Monoid ) -instance Show ( CNF  ) where-    show ( CNF cs ) = unlines $ map show cs+foldr f x (CNF s) = F.foldr f x s+filter p (CNF s) = CNF $ S.filter p s +size (CNF s) = S.size s+                   +clauses (CNF s) = F.toList s++instance Show CNF  where+    show cnf = unlines $ map show $ clauses cnf+ cnf :: [ Clause ] -> CNF -cnf cs = CNF cs+cnf cs = CNF $ S.fromList $ Prelude.filter ( /= CTrue) cs +singleton c = CNF $ S.singleton c -newtype Clause = Clause { literals :: [ Literal ] } +data Clause = Clause  ! ( M.Map Variable Bool )  | CTrue+   deriving ( Eq, Ord )++literals :: Clause ->  [ Literal ]+literals c = case c of+  Clause m -> map ( \ (v,p) -> literal p v ) $ M.toList m++instance Monoid Clause where+  mempty = Clause M.empty+  mappend c1 c2 = case c1 of+    CTrue -> CTrue+    Clause m1 -> case c2 of+      CTrue -> CTrue+      Clause m2 ->+        let common = M.intersection m1 m2+        in  if M.isSubmapOf common m1 && M.isSubmapOf common m2+            then Clause $ M.union m1 m2+            else CTrue+ instance Show ( Clause ) where-    show ( Clause xs ) = unwords ( map show xs ++ [ "0" ] )+  show c = case c of+    CTrue -> "# True"+    Clause m -> unwords ( map show (literals c) ++ [ "0" ] )  clause ::  [ Literal ] -> Clause -clause ls = Clause { literals = ls }-+clause ls = Prelude.foldr+            ( \ l c -> case c of+                 CTrue -> CTrue           +                 Clause m -> case M.lookup (variable l) m of+                   Nothing -> Clause $ M.insert (variable l) (positive l) m+                   Just p -> if p == positive l then Clause m else CTrue+            ) mempty ls +without c w = case c of+  -- CTrue -> CTrue -- ?+  Clause m -> Clause $ M.filterWithKey ( \ v p -> w /= v ) m
+ Satchmo/Fourier_Motzkin.hs view
@@ -0,0 +1,106 @@+{-# language TupleSections #-}++module Satchmo.Fourier_Motzkin where++import Satchmo.Data++import qualified Data.Map.Strict as M+import qualified Data.Set as S+import Control.Monad ( guard )+import Data.Monoid+import Data.List ( sortBy, nub )+import Data.Function (on)+import System.IO++type Solver = CNF -> IO (Maybe (M.Map Variable Bool))++fomo :: Solver+fomo cnf = do+  print_info "fomo" cnf+  ( remove_satisfied $ trivial $ onesided $  eliminate fomo ) cnf++print_info msg cnf = do+  hPutStrLn stderr $ unwords [ msg, show $ size cnf, "\n" ]+  -- hPutStrLn stderr $ show cnf ++ "\n"++remove_satisfied cont cnf = do+  print_info "remove_satisfied" cnf+  let vars polar cl = S.fromList $ do+        lit <- literals cl;+        guard $ positive lit == polar+        return $ variable lit+      remaining = Satchmo.Data.filter+        ( \ cl -> disjoint ( vars True cl ) ( vars False cl ))+        cnf+  cont cnf++trivial :: Solver -> Solver+trivial cont cnf = do+  print_info "trivial" cnf+  if null $ clauses cnf+     then return $ Just M.empty+     else if clause [] `elem` clauses cnf+          then return $ Nothing+          else cont cnf++onesided :: Solver -> Solver+onesided cont cnf = do+  print_info "onesided" cnf+  let pos = occurrences True  cnf+      neg = occurrences False cnf+      onlypos = M.keys $ M.difference pos neg+      onlyneg = M.keys $ M.difference neg pos+      assigned = M.fromList+          $ map (,True) onlypos ++ map (,False) onlyneg+      ks = M.keysSet assigned+      others = Satchmo.Data.filter+         ( \ cl -> disjoint ks+                   $ S.fromList $ map variable $ literals cl) +         cnf+  hPutStrLn stderr $ unwords [ "assigned", show assigned , "\n" ]       +  later <- ( if size others < size cnf then fomo else cont ) others+  return $ fmap ( M.union assigned ) later++disjoint s t = S.null $ S.intersection s t++eliminate :: Solver -> Solver+eliminate cont nf = do+  print_info "eliminate" nf+  let pos = occurrences True  nf+      neg = occurrences False nf+      reductions = M.intersectionWith+         ( \ xs ys -> let lx = length xs+                          ly = length xs+                      in  lx*ly - lx - ly+         ) pos neg+      resolve v = cnf $ do+        cp <- pos M.! v+        let cpv = cp `without` v+        cn <- neg M.! v+        let cnv = cn `without` v+        return $  cpv <> cnv+      others v = Satchmo.Data.filter+        ( \ cl -> not $ elem v $ map variable $ literals cl )+        nf+      reconstruct v m = Prelude.or $ do+        cp <- pos M.! v+        return $ Prelude.not $ Prelude.or $ do+          lit <- literals $ cp `without` v+          let v = M.findWithDefault False ( variable lit ) m+          return $ if positive lit then v else Prelude.not v +  case sortBy (compare `on` snd) $ M.toList reductions of+        (v,c): _ -> do+           hPutStrLn stderr $ unwords [ "completely resolve", show v, "count", show c ]+           later <- cont $ others v <> resolve v+           return $ fmap+                    ( \ m -> M.insert v (reconstruct v m) m)+                    later++-- | map each var to list of clauses where it occurs +occurrences :: Bool -> CNF -> M.Map Variable [Clause]+occurrences polarity  =+  flip Satchmo.Data.foldr M.empty $ \ cl ->+    M.unionWith (++) $ M.fromList $ do+      lit <- literals cl+      guard $ positive lit == polarity+      return ( variable lit, [cl] )
+ Satchmo/SAT/CNF.hs view
@@ -0,0 +1,87 @@+-- | use this module to get the actual+-- conjunctive normal form (a list of clauses).+-- You can then send this to minisat,+-- and do your own statistics and preprocessing first++{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE DoAndIfThenElse #-}+{-# LANGUAGE PatternSignatures #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE TemplateHaskell #-}+++module Satchmo.SAT.CNF++( SAT+, fresh+, emit+, solve+)++where++import qualified MiniSat as API++import Satchmo.Data+import Satchmo.Boolean hiding ( not )+import Satchmo.Code+import Satchmo.MonadSAT+import Satchmo.Fourier_Motzkin ( fomo )++import Control.Monad+import Control.Monad.State.Strict+import Control.Monad.Reader++import Control.Applicative+import Control.Lens+import Data.Monoid+import Data.Foldable+import qualified Data.Map.Strict as M+import System.IO++data S = S { _next :: ! Variable+           , _output :: ! CNF+           -- , _assignment :: ! (M.Map Variable Bool)+           }++$(makeLenses ''S)++newtype SAT a = SAT { unSAT :: StateT S IO a }+  deriving ( Functor, Applicative, Monad, MonadIO, MonadState S )++instance MonadFix SAT -- dummy++instance MonadSAT SAT where+  fresh = do+      x <- get+      modify ( next %~ succ )+      return $ literal True $ x ^. next++  emit cl = do      +      modify ( output %~ ( singleton cl <> ) )++  note msg = liftIO $ hPutStrLn stderr msg++  type Decoder SAT = Reader (M.Map Variable Bool)+  decode_variable v = do m <- ask ; return $ m M.! v+      +instance Decode (Reader (M.Map Variable Bool)) Boolean Bool where+    decode b = case b of+        Constant c -> return c+        Boolean  l -> do +            v <- -- decode_variable $ variable l+              do m <- ask ; return $ M.findWithDefault False ( variable l ) m+            return $ if positive l then v else not v++solve :: SAT (Decoder SAT a) -> IO (Maybe a)+solve action = do+  (a,s) <- runStateT (unSAT action)+           $ S { _next = 1, _output = cnf [] }+  mm <- fomo $ s^.output+  return $ case mm of+    Nothing -> Nothing+    Just m -> Just $ runReader a m+
Satchmo/SAT/Tmpfile.hs view
@@ -13,7 +13,7 @@  where -import Satchmo.Data+import Satchmo.Data hiding ( size ) import Satchmo.Code import Satchmo.Boolean import Satchmo.Boolean.Data
+ examples/RamseyFM.hs view
@@ -0,0 +1,105 @@+-- | find colouring without complete subgraphs+-- example usage: ./dist/build/Ramsey/Ramsey 3 3 3 16+-- last number is size of graph,+-- earlier numbers are sizes of forbidden cliques++{-# language PatternSignatures #-}++import Prelude hiding ( not, and, or, product )+import qualified Prelude++import Satchmo.Relation+import Satchmo.Code+import Satchmo.Boolean hiding ( implies )+import Satchmo.Counting++import qualified Satchmo.Binary as B++import Satchmo.SAT.CNF++import Data.List (sort, tails)+import qualified Data.Array as A+import Control.Monad ( guard, when, forM, foldM, void )+import System.Environment+import Data.Ix ( range)+++main :: IO ()+main = do+    argv <- getArgs+    let ns = map read $ case argv of+          [] -> [ "3", "3", "5" ] -- small numbers, else it will blow up+          _ -> argv+        cs = init ns +        n = last ns+    Just ( p : fs ) <- solve $ ramsey cs n+    forM ( zip [ 1.. ] fs ) $ \ (k, f) -> do +        putStrLn $ unwords [ "colour", show k ]+        printA f+    putStrLn "with isomorphism" ; printA p++printA :: A.Array (Int,Int) Bool -> IO ()+printA a = putStrLn $ unlines $ do+         let ((u,l),(o,r)) = A.bounds a+         x <- [u .. o]+         return $ unwords $ do +             y <- [ l ..r ]+             return $ case a A.! (x,y) of+                  True -> "* " ; False -> ". "++ramsey (cs :: [Int]) (n :: Int) = do+    fs <- forM cs $ \ c -> +         relation ((1 :: Int,1 :: Int),(n,n))+    +    p <- relation ((1,1),(n,n))+    -- forM fs $ isomorphism p++    -- forM fs $ cyclic 3++    when False $ void $ do+        forM [ 1 .. n ] $ \ x -> +            forM [ x + 1 .. n ] $ \ y -> +                assertM $ exactly 1 $ +                    for fs $ \ f -> f ! (x,y) +    when True $ void $ do+        forM [ 1 .. n ] $ \ x -> +            forM [ x + 1 .. n ] $ \ y -> +                assert $ for fs $ \ f -> f ! (x,y)++    forM ( zip cs fs ) $ \ (c,f) -> +        forM ( cliquesA c [1..n] ) $ \ xs ->+            assert $ for ( cliquesA 2 xs ) $ \ [x,y] -> not $ f ! (x,y)+    return $ forM (p : fs) decode+    +isomorphism p e = do+    assertM $ regular 1 p+    assertM $ regular 1 $ mirror p+    e' <- foldM product ( mirror p ) [ e, p ]+    assertM $ implies e e'+    assertM $ implies e' e++cyclic off f = forM ( indices f ) $ \ (i,j) -> +    when ( off < i Prelude.&& i < j ) +         $ assert_fun2 (==) ( f!(i,j) ) (f!(i-off,j-off))++cliquesA k xs = +      let -- spec:  c!(i,j) == cliques i (drop j xs)+          bnd = ((0,0),(k, length xs))+          c = A.array bnd $ do+            (i,j) <- A.range bnd+            return ( (i,j)+                   , if i == 0 then [ [] ]+                     else if i > length xs - j then []               +                     else c A.! (i,j+1) +                          ++ map (xs !! j : ) ( c A.! (i-1,j+1))+                   )             +      in  c A.! (k,0)         ++cliques 0 xs = return []+cliques k xs | k > length xs = []+cliques k (x:xs) =+    cliques k xs ++ map (x :) ( cliques (k-1) xs )++for = flip map++assertM this = do x <- this ; assert [x]
satchmo.cabal view
@@ -1,5 +1,5 @@ Name:           satchmo-Version:        2.9.6+Version:        2.9.7  License:        GPL License-file:	gpl-2.0.txt@@ -21,7 +21,7 @@ Library     ghc-options: -funbox-strict-fields     Build-depends:  mtl, process, containers, base == 4.*,-               array, bytestring, directory, minisat >= 0.1+        lens, array, bytestring, directory, minisat >= 0.1     Exposed-modules:         Satchmo.Data         -- Satchmo.Data.Default@@ -55,6 +55,8 @@         Satchmo.SAT         Satchmo.SAT.Tmpfile         Satchmo.SAT.Mini+        Satchmo.SAT.CNF+        Satchmo.Fourier_Motzkin         -- Satchmo.SAT.BS         -- Satchmo.SAT.Seq         -- Satchmo.SAT.Sequence@@ -101,6 +103,12 @@   Type: exitcode-stdio-1.0   hs-source-dirs: examples   Main-Is: Ramsey.hs+  Build-Depends: base, array, satchmo++Test-Suite RamseyFM+  Type: exitcode-stdio-1.0+  hs-source-dirs: examples+  Main-Is: RamseyFM.hs   Build-Depends: base, array, satchmo