Skip to content

Commit

Permalink
add minimalHittingSets of ZDD
Browse files Browse the repository at this point in the history
  • Loading branch information
msakai committed Oct 17, 2021
1 parent e497303 commit 9fbb6d0
Show file tree
Hide file tree
Showing 2 changed files with 92 additions and 0 deletions.
45 changes: 45 additions & 0 deletions src/Data/DecisionDiagram/ZDD.hs
Original file line number Diff line number Diff line change
Expand Up @@ -59,6 +59,11 @@ module Data.DecisionDiagram.ZDD
-- * Update
, change

-- * Minimal hitting sets
, minimalHittingSets
, minimalHittingSetsKnuth
, minimalHittingSetsImai

-- * Conversion
, toSetOfIntSets
) where
Expand Down Expand Up @@ -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: <http://id.nii.ac.jp/1001/00145799/>.
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 ==)
Expand Down
47 changes: 47 additions & 0 deletions test/TestZDD.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
-- ------------------------------------------------------------------------
Expand Down

0 comments on commit 9fbb6d0

Please sign in to comment.