diff --git a/examples/Domino.hs b/examples/Domino.hs new file mode 100644 --- /dev/null +++ b/examples/Domino.hs @@ -0,0 +1,88 @@ +{- +In how many ways can a n x m board be entirely covered by 2 x 1 domino +pieces? + +Usage: ./Domino 4 3 + time stack runghc examples/Domino.hs 4 9 + VERBOSE=1 stack runghc examples/Domino.hs 2 3 + or: ghci> prettySolve 4 3 +-} +module Main where + +import Prelude hiding (bool,not,and,or,any,all,(&&),(||)) +import Control.Monad (guard, when) +import Data.Maybe (isJust) +import System.Environment (getArgs, lookupEnv) +import qualified Data.Map +import qualified Data.Set +import Data.List (tails) + +import Prelude hiding ((&&),(||),not,and,or,all,any) +import OBDD + +dominoes w h = rows ++ cols + where rows = positions [1..h-1] [1..w] $ \x y -> ((x, y), (x+1, y)) + cols = positions [1..h] [1..w-1] $ \x y -> ((x, y), (x, y+1)) + positions xs ys f = f <$> xs <*> ys + +positions w h = (,) <$> [1..h] <*> [1..w] + +dominoFormula w h = + all ( \ f -> exactly_one (map variable $ filter (isCoveredBy f) (dominoes w h) ) + ) (positions w h) + +f `isCoveredBy` p = f == fst p || f == snd p + +exactly_one xs = or xs && atmost_one xs + +atmost_one :: Boolean b => [b] -> b +atmost_one = atmost_one_lin + +atmost_one_lin xs = + let go [] = (true,false) + go [x] = (not x, x) + go xs = let (ys,zs) = splitAt (div (length xs) 2) xs + (y0,y1) = go ys + (z0,z1) = go zs + in (y0 && z0, y1 && z0 || y0 && z1) + (x0,x1) = go xs + in x0 || x1 + +atmost_one_quad xs = not $ or $ do + p <- xs ; q <- xs ; guard $ p < q + return $ and [ OBDD.unit p True, OBDD.unit q True ] + + +prettySolution w h ds = putStr $ concat $ do + x <- [1..h] + y <- [1..w] + let letter = case find (\(domino, _) -> fst domino == (x, y) || snd domino == (x, y)) withNames of + Nothing -> "." + Just (_, letter) -> letter:[] + return $ if y == w then letter ++ "\n" else letter + where withNames = if length names < length ds + then error "not enough names" + else zip ds names + names = ['0'..'9'] ++ ['a'..'z'] ++ ['A'..'Z'] + find f xs = case filter f xs of + [] -> Nothing + x:_ -> Just x + +prettySolve w h = + mapM_ (\ds -> prettySolution w h ds >> putStrLn "") + . map (map fst . filter snd) + . map (Data.Map.toList) $ + models (Data.Set.fromList $ dominoes w h) $ dominoFormula w h + +main = do + args <- getArgs + let [width, height] = case map read args :: [Int] of + [] -> [4, 3] + [width, height] -> [width, height] + let formula = dominoFormula width height + verbose <- lookupEnv "VERBOSE" >>= return . isJust + when verbose $ mapM_ (\ds -> prettySolution width height ds >> putStrLn "") + . map (map fst . filter snd) + . map (Data.Map.toList) $ + models (Data.Set.fromList $ dominoes width height) formula + print $ number_of_models (Data.Set.fromList $ dominoes width height) formula diff --git a/examples/Weight.hs b/examples/Weight.hs --- a/examples/Weight.hs +++ b/examples/Weight.hs @@ -1,10 +1,7 @@ {- -NOTE: the following comment is lying, see https://github.com/jwaldmann/haskell-obdd/issues/5 - -The minimal number of knights needed to occupy or attack -every square on an n×n chessboard -(i.e., domination numbers for the n×n knight graphs) +The maximal number of non-attacking knights on an n×n chessboard +(i.e., independence numbers for the n×n knight graphs) http://mathworld.wolfram.com/KnightsProblem.html diff --git a/obdd.cabal b/obdd.cabal --- a/obdd.cabal +++ b/obdd.cabal @@ -1,5 +1,5 @@ Name: obdd -Version: 0.8.1 +Version: 0.8.2 Cabal-Version: >= 1.8 Build-type: Simple Synopsis: Ordered Reduced Binary Decision Diagrams @@ -13,25 +13,29 @@ An important (for me, in teaching) feature is that I can immediately draw the BDD to an X11 window (via graphviz). For example, to show the effect of different variable orderings, - try this in ghci: + try this in ghci (type 'q' to close the drawing windows). . - > import qualified Prelude as P + > import Prelude hiding (not,(&&),(||),and,or,any,all) > import OBDD > let f [] = false; f (x:y:zs) = x && y || f zs - > display P.$ f P.$ P.map variable [1,2,3,4,5,6] - > display P.$ f P.$ P.map variable [1,4,2,5,3,6] + > display $ f $ map variable [1,2,3,4,5,6] + > display $ f $ map variable [1,4,2,5,3,6] . - If you want better performance, - use + 'OBDD' implements 'Ersatz.Boolean' which re-defines + Boolean operations from the Prelude. The recommended way of using this + is shown in the previous example. + . + If you want better performance, use a library with a persistent BDD base, + e.g., , see . -category: Logic +category: Logic License: GPL License-file: LICENSE Author: Johannes Waldmann Maintainer: Johannes Waldmann -Homepage: https://github.com/jwaldmann/haskell-obdd +Homepage: https://github.com/jwaldmann/haskell-obdd Source-Repository head Type: git @@ -39,15 +43,21 @@ Library Build-Depends: base==4.*, random, mtl, containers>=0.5, array, process-extras, ersatz, text - Hs-Source-Dirs: src + Hs-Source-Dirs: src Exposed-Modules: OBDD OBDD.Data OBDD.Make OBDD.Operation OBDD.Property, OBDD.Display, OBDD.Linopt, OBDD.Cube - Other-Modules: OBDD.IntIntMap, OBDD.VarIntIntMap + Other-Modules: OBDD.IntIntMap, OBDD.VarIntIntMap ghc-options: -funbox-strict-fields test-suite obdd-placement Hs-Source-Dirs : examples Type: exitcode-stdio-1.0 Main-Is: Placement.hs + Build-Depends: base, containers, obdd + +test-suite obdd-domino + Hs-Source-Dirs: examples + Type: exitcode-stdio-1.0 + Main-Is: Domino.hs Build-Depends: base, containers, obdd test-suite obdd-cubism diff --git a/src/OBDD/Data.hs b/src/OBDD/Data.hs --- a/src/OBDD/Data.hs +++ b/src/OBDD/Data.hs @@ -22,9 +22,10 @@ , Node (..) , make , register, checked_register -, cached, top +, top , access - +, not_ +, assocs ) where @@ -71,14 +72,14 @@ -- , icore :: !(Map ( Node v Index ) Index) , icore :: !(VarIntIntMap v Index) + , ifalse :: ! Index + , itrue :: ! Index , next :: !Index , top :: !Index - - , cache :: !(IntIntMap Index) - -- ^ inputs and output for binary op - -- (unary will be simulated by binary) } +assocs :: OBDD v -> [(Index, Node v Index)] +assocs o = IM.toAscList $ core o -- | Apply function in each node, bottom-up. -- return the value in the root node. @@ -104,15 +105,13 @@ -> ( v -> a -> a -> m a ) -> OBDD v -> m a foldM leaf branch o = do - f <- leaf False ; t <- leaf True - let m0 = M.fromList - [(icore_false,f), (icore_true,t)] m <- Control.Monad.foldM ( \ m (i,n) -> do val <- case n of + Leaf b -> leaf b Branch v l r -> branch v (m M.! l) (m M.! r) return $ M.insert i val m - ) m0 $ IM.toAscList $ core o + ) M.empty $ IM.toAscList $ core o return $ m M.! top o -- | Apply function in each node, bottom-up. @@ -158,9 +157,6 @@ ) o interpolate a Nothing res -icore_false = 0 :: Index -icore_true = 1 :: Index - size = unIndex . next -- | Number of satisfying assignments with given set of variables. @@ -173,21 +169,29 @@ empty :: OBDD v empty = OBDD - { core = IM.empty + { core = IM.fromList [(0,Leaf False),(1,Leaf True)] , icore = VIIM.empty + , ifalse = 0 + , itrue = 1 , next = 2 - , top = 0 - , cache = IIM.empty + , top = -1 } data Node v i = Leaf !Bool | Branch !v !i !i deriving ( Eq, Ord ) +not_ o = o { ifalse = itrue o + , itrue = ifalse o + , core = IM.insert (itrue o) (Leaf False) + $ IM.insert (ifalse o) (Leaf True) + $ core o + } + access :: OBDD v -> Node v ( OBDD v ) access s = case top s of - 0 -> Leaf False - 1 -> Leaf True + i | i == ifalse s -> Leaf False + i | i == itrue s -> Leaf True t -> case IM.lookup ( top s ) ( core s ) of Nothing -> error "OBDD.Data.access" Just n -> case n of @@ -261,27 +265,12 @@ put $! s { next = succ i } return i -cached :: Ord v - => (Index, Index) - -> ( State ( OBDD v ) Index ) - -> State ( OBDD v ) Index -cached (l,r) action = do - s <- get - case IIM.lookup (l, r) $ cache s of - Just i -> return i - Nothing -> do - i <- action - s <- get - put $! s { cache = IIM.insert (l, r) i - $ cache s } - return i - register :: Ord v => Node v Index -> State ( OBDD v ) Index register n = case n of - Leaf False -> return 0 - Leaf True -> return 1 + Leaf False -> ifalse <$> get + Leaf True -> itrue <$> get Branch v l r -> if l == r then return l else do s <- get case VIIM.lookup (v, l, r) ( icore s ) of diff --git a/src/OBDD/IntIntMap.hs b/src/OBDD/IntIntMap.hs --- a/src/OBDD/IntIntMap.hs +++ b/src/OBDD/IntIntMap.hs @@ -1,7 +1,7 @@ module OBDD.IntIntMap ( IntIntMap () -, empty, lookup, insert, singleton +, empty, lookup, insert, singleton, (!) ) where @@ -21,6 +21,9 @@ lookup (i, j) (IntIntMap mm) = do m <- M.lookup i mm M.lookup j m + +(!) :: IntIntMap v -> (Int,Int) -> v +IntIntMap m ! (i,j) = m M.! i M.! j insert (i, j) v (IntIntMap mm) = case M.lookup i mm of diff --git a/src/OBDD/Operation.hs b/src/OBDD/Operation.hs --- a/src/OBDD/Operation.hs +++ b/src/OBDD/Operation.hs @@ -1,5 +1,6 @@ {-# language ScopedTypeVariables #-} {-# language PatternGuards #-} +{-# language FlexibleContexts #-} module OBDD.Operation @@ -20,26 +21,34 @@ import Ersatz.Bit import Data.Foldable (toList) +import qualified Data.IntMap as IM +import qualified OBDD.IntIntMap as IIM +import qualified Data.Map as M + +import qualified Control.Monad.State.Strict as T +import Control.Monad (forM_) import qualified Data.List ( sortBy) import Data.Function (on) import Data.Set ( Set ) import qualified Data.Set as S -import Prelude hiding ( (&&), (||), and, or, not, bool ) +import Prelude hiding ( (&&), (||), and, or, not, any, all, bool ) import qualified Prelude import qualified Data.Bool instance Ord v => Boolean (OBDD v) where bool f = constant f - not = unary ( Prelude.not ) + not = not_ ( && ) = symmetric_binary ( Prelude.&& ) ( || ) = symmetric_binary ( Prelude.|| ) - choose no yes sel = (no && not sel) || (yes && sel) + choose no yes sel = + -- https://github.com/jwaldmann/haskell-obdd/issues/10 + (no && not sel) || (yes && sel) xor = symmetric_binary (/=) ( ==> ) = binary ( <= ) - all p = fold_by_size (constant True ) (&&) . map p . toList - any p = fold_by_size (constant False) (||) . map p . toList + all p = fold_by_size true (&&) . map p . toList + any p = fold_by_size false (||) . map p . toList equiv :: Ord v => OBDD v -> OBDD v -> OBDD v equiv = symmetric_binary (==) @@ -57,17 +66,20 @@ in handle $ Data.List.sortBy (compare `on` size) fs +-- | FIXME: this function is nonsensical. There is only one interesting +-- unary Boolean function (negation), and it should be handled differently. unary :: Ord v => ( Bool -> Bool ) -> OBDD v -> OBDD v unary op x = make $ do - let handle x = cached ( top x, top x ) $ case access x of - Leaf p -> register $ Leaf $ op p + let handle x = cachedIM (top x) $ case access x of + Leaf p -> do + T.lift $ register $ Leaf $ op p Branch v l r -> do l' <- handle l r' <- handle r - register $ Branch v l' r' - handle x + T.lift $ register $ Branch v l' r' + flip T.evalStateT IM.empty $ handle x data Symmetricity = Asymmetric | Symmetric deriving Show @@ -82,36 +94,63 @@ -> OBDD v -> OBDD v -> OBDD v symmetric_binary = binary_ Symmetric - binary_ :: Ord v => Symmetricity -> ( Bool -> Bool -> Bool ) -> OBDD v -> OBDD v -> OBDD v - -binary_ sym op x y = make $ do +-- FIXME https://github.com/jwaldmann/haskell-obdd/issues/4 +binary_ _ op x y = make $ do let -- register = checked_register -- for testing -- handle x y | Symmetric <- sym, top x > top y = handle y x - handle x y = cached (top x, top y) $ case ( access x , access y ) of - ( Leaf p , Leaf q ) -> register $ Leaf $ op p q + handle x y = cachedIIM (top x, top y) $ case ( access x , access y ) of + ( Leaf p , Leaf q ) -> do + T.lift $ register $ Leaf $ op p q ( ax, ay ) -> case comp ax ay of LT -> do let Branch v l r = ay l' <- handle x l r' <- handle x r - register $ Branch v l' r' + T.lift $ register $ Branch v l' r' GT -> do let Branch v l r = ax l' <- handle l y r' <- handle r y - register $ Branch v l' r' + T.lift $ register $ Branch v l' r' EQ -> do let Branch v1 l1 r1 = ax Branch v2 l2 r2 = ay v = if v1 == v2 then v1 else error "OBDD.Operation.handle" l' <- handle l1 l2 r' <- handle r1 r2 - register $ Branch v l' r' - handle x y + T.lift $ register $ Branch v l' r' + flip T.evalStateT IIM.empty $ handle x y + +{-# inline cachedM #-} +cachedM arg act = do + c <- T.get + case M.lookup arg c of + Nothing -> do + res <- act ; T.modify' $ M.insert arg res; return res + Just res -> do + return res + +{-# inline cachedIM #-} +cachedIM arg act = do + c <- T.get + case IM.lookup arg c of + Nothing -> do + res <- act ; T.modify' $ IM.insert arg res; return res + Just res -> do + return res + +{-# inline cachedIIM #-} +cachedIIM arg act = do + c <- T.get + case IIM.lookup arg c of + Nothing -> do + res <- act ; T.modify' $ IIM.insert arg res; return res + Just res -> do + return res comp x y = case (x , y) of ( Leaf {} , Leaf {} ) -> EQ