diff --git a/src/Data/DecisionDiagram/ZDD.hs b/src/Data/DecisionDiagram/ZDD.hs index 61fe7a8..3f14e4e 100644 --- a/src/Data/DecisionDiagram/ZDD.hs +++ b/src/Data/DecisionDiagram/ZDD.hs @@ -59,6 +59,11 @@ module Data.DecisionDiagram.ZDD -- * Update , change + -- * Minimal hitting sets + , minimalHittingSets + , minimalHittingSetsKnuth + , minimalHittingSetsImai + -- * Conversion , toSetOfIntSets ) where @@ -279,6 +284,46 @@ nonSuperset (ZDD node1) (ZDD node2) = runST $ do ret <- f node1 node2 return (ZDD ret) +minimalHittingSets' :: forall a. ItemOrder a => Bool -> ZDD a -> ZDD a +minimalHittingSets' imai (ZDD node) = runST $ do + h <- C.newSized defaultTableSize + let f F = return T + f T = return F + f p@(Branch top p0 p1) = do + m <- H.lookup h p + case m of + Just ret -> return ret + Nothing -> do + -- TODO: memoize union and difference/nonSuperset? + r0 <- case union (ZDD p0) (ZDD p1) :: ZDD a of + ZDD r -> f r + ZDD r1 <- liftM2 (if imai then difference else nonSuperset) (liftM ZDD (f p0)) (pure (ZDD r0 :: ZDD a)) + let ret = zddNode top r0 r1 + H.insert h p ret + return ret + ret <- f node + return (ZDD ret) + +-- | Minimal hitting sets. +-- +-- D. E. Knuth, "The Art of Computer Programming, Volume 4A: +-- Combinatorial Algorithms, Part 1," Addison-Wesley Professional, +-- 2011. +minimalHittingSetsKnuth :: forall a. ItemOrder a => ZDD a -> ZDD a +minimalHittingSetsKnuth = minimalHittingSets' False + +-- | Minimal hitting sets. +-- +-- T. Imai, "One-line hack of knuth's algorithm for minimal hitting set +-- computation with ZDDs," vol. 2015-AL-155, no. 15, Nov. 2015, pp. 1-3. +-- [Online]. Available: . +minimalHittingSetsImai :: forall a. ItemOrder a => ZDD a -> ZDD a +minimalHittingSetsImai = minimalHittingSets' True + +-- | See 'minimalHittingSetsImai'. +minimalHittingSets :: forall a. ItemOrder a => ZDD a -> ZDD a +minimalHittingSets = minimalHittingSetsImai + -- | Is this the empty set? null :: ZDD a -> Bool null = (empty ==) diff --git a/test/TestZDD.hs b/test/TestZDD.hs index d99c665..663d718 100644 --- a/test/TestZDD.hs +++ b/test/TestZDD.hs @@ -4,9 +4,11 @@ module TestZDD (zddTestGroup) where import Control.Monad +import Data.IntSet (IntSet) import qualified Data.IntSet as IntSet import Data.List import Data.Proxy +import Data.Set (Set) import qualified Data.Set as Set import Test.Tasty import Test.Tasty.QuickCheck @@ -197,6 +199,51 @@ prop_nonSuperset_difference = d = a ZDD.\\ b in counterexample (show (c, d)) $ c `ZDD.isSubsetOf` d +-- ------------------------------------------------------------------------ +-- Minimal hitting sets +-- ------------------------------------------------------------------------ + +isHittingSetOf :: IntSet -> Set IntSet -> Bool +isHittingSetOf s g = all (\e -> not (IntSet.null (s `IntSet.intersection` e))) g + +prop_minimalHittingSetsKnuth_isHittingSet :: Property +prop_minimalHittingSetsKnuth_isHittingSet = + withDefaultOrder $ \(_ :: Proxy o) -> + forAll arbitrary $ \(a :: ZDD o) -> + let b = ZDD.minimalHittingSetsKnuth a + a' = ZDD.toSetOfIntSets a + b' = ZDD.toSetOfIntSets b + in all (`isHittingSetOf` a') b' + +prop_minimalHittingSetsImai_isHittingSet :: Property +prop_minimalHittingSetsImai_isHittingSet = + withDefaultOrder $ \(_ :: Proxy o) -> + forAll arbitrary $ \(a :: ZDD o) -> + let b = ZDD.minimalHittingSetsImai a + a' = ZDD.toSetOfIntSets a + b' = ZDD.toSetOfIntSets b + in all (`isHittingSetOf` a') b' + +prop_minimalHittingSetsKnuth_duality :: Property +prop_minimalHittingSetsKnuth_duality = + withDefaultOrder $ \(_ :: Proxy o) -> + forAll arbitrary $ \(a :: ZDD o) -> + let b = ZDD.minimalHittingSetsKnuth a + in ZDD.minimalHittingSetsKnuth (ZDD.minimalHittingSetsKnuth b) === b + +prop_minimalHittingSetsImai_duality :: Property +prop_minimalHittingSetsImai_duality = + withDefaultOrder $ \(_ :: Proxy o) -> + forAll arbitrary $ \(a :: ZDD o) -> + let b = ZDD.minimalHittingSetsImai a + in ZDD.minimalHittingSetsImai (ZDD.minimalHittingSetsImai b) === b + +prop_minimalHittingSets_Imai_equal_Knuth :: Property +prop_minimalHittingSets_Imai_equal_Knuth = + withDefaultOrder $ \(_ :: Proxy o) -> + forAll arbitrary $ \(a :: ZDD o) -> + ZDD.minimalHittingSetsImai a == ZDD.minimalHittingSetsKnuth a + -- ------------------------------------------------------------------------ -- Misc -- ------------------------------------------------------------------------