Data.DecisionDiagram.ZDD

Zero-Suppressed binary decision diagram.

References:

• S. Minato, "Zero-Suppressed BDDs for Set Manipulation in Combinatorial Problems," 30th ACM/IEEE Design Automation Conference, 1993, pp. 272-277, doi: 10.1145/157485.164890. https://www.researchgate.net/publication/221062015_Zero-Suppressed_BDDs_for_Set_Manipulation_in_Combinatorial_Problems

ZDD type

data ZDD a where

Zero-suppressed binary decision diagram representing family of sets

Bundled Patterns

pattern Leaf :: Bool -> ZDD a

pattern Branch :: Int -> ZDD a -> ZDD a -> ZDD a

Smart constructor that takes the ZDD reduction rules into account

Instances

ItemOrder a => IsList (ZDD a)

Defined in Data.DecisionDiagram.ZDD

Associated Types

type Item (ZDD a)

Methods

fromList :: [Item (ZDD a)] -> ZDD a

fromListN :: Int -> [Item (ZDD a)] -> ZDD a

toList :: ZDD a -> [Item (ZDD a)]

Eq (ZDD a)

Defined in Data.DecisionDiagram.ZDD

Methods

(==) :: ZDD a -> ZDD a -> Bool

(/=) :: ZDD a -> ZDD a -> Bool

Read (ZDD a)

Defined in Data.DecisionDiagram.ZDD

Methods

readsPrec :: Int -> ReadS (ZDD a)

readList :: ReadS [ZDD a]

readPrec :: ReadPrec (ZDD a)

readListPrec :: ReadPrec [ZDD a]

Show (ZDD a)

Defined in Data.DecisionDiagram.ZDD

Methods

showsPrec :: Int -> ZDD a -> ShowS

show :: ZDD a -> String

showList :: [ZDD a] -> ShowS

Hashable (ZDD a)

Defined in Data.DecisionDiagram.ZDD

Methods

hashWithSalt :: Int -> ZDD a -> Int

hash :: ZDD a -> Int

type Item (ZDD a)

Defined in Data.DecisionDiagram.ZDD

type Item (ZDD a) = IntSet

pattern Empty :: ZDD a

Synonym of Leaf False

pattern Base :: ZDD a

Synonym of Leaf True

Item ordering

class ItemOrder a where

Methods

compareItem :: proxy a -> Int -> Int -> Ordering

Instances

ItemOrder DescOrder

Defined in Data.DecisionDiagram.BDD.Internal.ItemOrder

Methods

compareItem :: proxy DescOrder -> Int -> Int -> Ordering

ItemOrder AscOrder

Defined in Data.DecisionDiagram.BDD.Internal.ItemOrder

Methods

compareItem :: proxy AscOrder -> Int -> Int -> Ordering

data AscOrder

Instances

ItemOrder AscOrder

Defined in Data.DecisionDiagram.BDD.Internal.ItemOrder

Methods

compareItem :: proxy AscOrder -> Int -> Int -> Ordering

data DescOrder

Instances

ItemOrder DescOrder

Defined in Data.DecisionDiagram.BDD.Internal.ItemOrder

Methods

compareItem :: proxy DescOrder -> Int -> Int -> Ordering

withDefaultOrder :: forall r. (forall a. ItemOrder a => Proxy a -> r) -> r

Currently the default order is AscOrder

withAscOrder :: forall r. (Proxy AscOrder -> r) -> r

withDescOrder :: forall r. (Proxy DescOrder -> r) -> r

withCustomOrder :: forall r. (Int -> Int -> Ordering) -> (forall a. ItemOrder a => Proxy a -> r) -> r

Construction

empty :: ZDD a

The empty family (∅).

>>> toSetOfIntSets (empty :: ZDD AscOrder)
fromList []

base :: ZDD a

The family containing only the empty set ({∅}).

>>> toSetOfIntSets (base :: ZDD AscOrder)
fromList [fromList []]

singleton :: forall a. ItemOrder a => IntSet -> ZDD a

Create a ZDD that contains only a given set.

>>> toSetOfIntSets (singleton (IntSet.fromList [1,2,3]) :: ZDD AscOrder)
fromList [fromList [1,2,3]]

subsets :: forall a. ItemOrder a => IntSet -> ZDD a

Set of all subsets, i.e. powerset

combinations :: forall a. (ItemOrder a, HasCallStack) => IntSet -> Int -> ZDD a

Set of all k-combination of a set

fromListOfIntSets :: forall a. ItemOrder a => [IntSet] -> ZDD a

Create a ZDD from a list of IntSet

fromSetOfIntSets :: forall a. ItemOrder a => Set IntSet -> ZDD a

Create a ZDD from a set of IntSet

Pseudo-boolean constraints

subsetsAtLeast :: forall a w. (ItemOrder a, Real w) => IntMap w -> w -> ZDD a

Set of all subsets whose sum of weights is at least k.

subsetsAtMost :: forall a w. (ItemOrder a, Real w) => IntMap w -> w -> ZDD a

Set of all subsets whose sum of weights is at most k.

subsetsExactly :: forall a w. (ItemOrder a, Real w) => IntMap w -> w -> ZDD a

Set of all subsets whose sum of weights is exactly k.

Note that combinations is a special case where all weights are 1.

If weight type is Integral, subsetsExactlyIntegral is more efficient.

subsetsExactlyIntegral :: forall a w. (ItemOrder a, Real w, Integral w) => IntMap w -> w -> ZDD a

Similar to subsetsExactly but more efficient.

Insertion

insert :: forall a. ItemOrder a => IntSet -> ZDD a -> ZDD a

Insert a set into the ZDD.

>>> toSetOfIntSets (insert (IntSet.fromList [1,2,3]) (fromListOfIntSets (map IntSet.fromList [[1,3], [2,4]])) :: ZDD AscOrder)
fromList [fromList [1,2,3],fromList [1,3],fromList [2,4]]

Deletion

delete :: forall a. ItemOrder a => IntSet -> ZDD a -> ZDD a

Delete a set from the ZDD.

>>> toSetOfIntSets (delete (IntSet.fromList [1,3]) (fromListOfIntSets (map IntSet.fromList [[1,2,3], [1,3], [2,4]])) :: ZDD AscOrder)
fromList [fromList [1,2,3],fromList [2,4]]

Query

member :: forall a. ItemOrder a => IntSet -> ZDD a -> Bool

Is the set a member of the family?

notMember :: forall a. ItemOrder a => IntSet -> ZDD a -> Bool

Is the set not in the family?

null :: ZDD a -> Bool

Is this the empty family?

size :: Integral b => ZDD a -> b

The number of sets in the family.

Any Integral type can be used as a result type, but it is recommended to use Integer or Natural because the size can be larger than Int64 for example:

>>> size (subsets (IntSet.fromList [1..128]) :: ZDD AscOrder) :: Integer
340282366920938463463374607431768211456
>>> import Data.Int
>>> maxBound :: Int64
9223372036854775807

isSubsetOf :: ItemOrder a => ZDD a -> ZDD a -> Bool

(s1 `isSubsetOf` s2) indicates whether s1 is a subset of s2.

isProperSubsetOf :: ItemOrder a => ZDD a -> ZDD a -> Bool

(s1 `isProperSubsetOf` s2) indicates whether s1 is a proper subset of s2.

disjoint :: ItemOrder a => ZDD a -> ZDD a -> Bool

Check whether two families are disjoint (i.e., their intersection is empty).

numNodes :: ZDD a -> Int

Count the number of nodes in a ZDD viewed as a rooted directed acyclic graph.

Please do not confuse it with size.

See also toGraph.

Combine

union :: forall a. ItemOrder a => ZDD a -> ZDD a -> ZDD a

Union of two family of sets.

unions :: forall f a. (Foldable f, ItemOrder a) => f (ZDD a) -> ZDD a

Unions of a list of ZDDs.

intersection :: forall a. ItemOrder a => ZDD a -> ZDD a -> ZDD a

Intersection of two family of sets.

difference :: forall a. ItemOrder a => ZDD a -> ZDD a -> ZDD a

Difference of two family of sets.

(\\) :: forall a. ItemOrder a => ZDD a -> ZDD a -> ZDD a

See difference

nonSuperset :: forall a. ItemOrder a => ZDD a -> ZDD a -> ZDD a

Given a family P and Q, it computes {S∈P | ∀X∈Q. X⊈S}

Sometimes it is denoted as P ↘ Q.

>>> toSetOfIntSets (fromListOfIntSets (map IntSet.fromList [[1,2,3], [1,3], [3,4]]) `nonSuperset` singleton (IntSet.fromList [1,3]) :: ZDD AscOrder)
fromList [fromList [3,4]]

Filter

subset1 :: forall a. ItemOrder a => Int -> ZDD a -> ZDD a

Select subsets that contain a particular element and then remove the element from them

>>> toSetOfIntSets $ subset1 2 (fromListOfIntSets (map IntSet.fromList [[1,2,3], [1,3], [2,4]]) :: ZDD AscOrder)
fromList [fromList [1,3],fromList [4]]

subset0 :: forall a. ItemOrder a => Int -> ZDD a -> ZDD a

Subsets that does not contain a particular element

>>> toSetOfIntSets $ subset0 2 (fromListOfIntSets (map IntSet.fromList [[1,2,3], [1,3], [2,4], [3,4]]) :: ZDD AscOrder)
fromList [fromList [1,3],fromList [3,4]]

Map

mapInsert :: forall a. ItemOrder a => Int -> ZDD a -> ZDD a

Insert an item into each element set of ZDD.

>>> toSetOfIntSets (mapInsert 2 (fromListOfIntSets (map IntSet.fromList [[1,2,3], [1,3], [1,4]])) :: ZDD AscOrder)
fromList [fromList [1,2,3],fromList [1,2,4]]

mapDelete :: forall a. ItemOrder a => Int -> ZDD a -> ZDD a

Delete an item from each element set of ZDD.

>>> toSetOfIntSets (mapDelete 2 (fromListOfIntSets (map IntSet.fromList [[1,2,3], [1,3], [1,2,4]])) :: ZDD AscOrder)
fromList [fromList [1,3],fromList [1,4]]

change :: forall a. ItemOrder a => Int -> ZDD a -> ZDD a

change x p returns {if x∈s then s∖{x} else s∪{x} | s∈P}

>>> toSetOfIntSets (change 2 (fromListOfIntSets (map IntSet.fromList [[1,2,3], [1,3], [1,2,4]])) :: ZDD AscOrder)
fromList [fromList [1,2,3],fromList [1,3],fromList [1,4]]

(Co)algebraic structure

data Sig a

Signature functor of binary decision trees, BDD, and ZDD.

Constructors

SLeaf !Bool

SBranch !Int a a

Instances

Functor Sig

Defined in Data.DecisionDiagram.BDD.Internal.Node

Methods

fmap :: (a -> b) -> Sig a -> Sig b

(<$) :: a -> Sig b -> Sig a

Foldable Sig

Defined in Data.DecisionDiagram.BDD.Internal.Node

Methods

fold :: Monoid m => Sig m -> m

foldMap :: Monoid m => (a -> m) -> Sig a -> m

foldMap' :: Monoid m => (a -> m) -> Sig a -> m

foldr :: (a -> b -> b) -> b -> Sig a -> b

foldr' :: (a -> b -> b) -> b -> Sig a -> b

foldl :: (b -> a -> b) -> b -> Sig a -> b

foldl' :: (b -> a -> b) -> b -> Sig a -> b

foldr1 :: (a -> a -> a) -> Sig a -> a

foldl1 :: (a -> a -> a) -> Sig a -> a

toList :: Sig a -> [a]

null :: Sig a -> Bool

length :: Sig a -> Int

elem :: Eq a => a -> Sig a -> Bool

maximum :: Ord a => Sig a -> a

minimum :: Ord a => Sig a -> a

sum :: Num a => Sig a -> a

product :: Num a => Sig a -> a

Traversable Sig

Defined in Data.DecisionDiagram.BDD.Internal.Node

Methods

traverse :: Applicative f => (a -> f b) -> Sig a -> f (Sig b)

sequenceA :: Applicative f => Sig (f a) -> f (Sig a)

mapM :: Monad m => (a -> m b) -> Sig a -> m (Sig b)

sequence :: Monad m => Sig (m a) -> m (Sig a)

Eq a => Eq (Sig a)

Defined in Data.DecisionDiagram.BDD.Internal.Node

Methods

(==) :: Sig a -> Sig a -> Bool

(/=) :: Sig a -> Sig a -> Bool

Ord a => Ord (Sig a)

Defined in Data.DecisionDiagram.BDD.Internal.Node

Methods

compare :: Sig a -> Sig a -> Ordering

(<) :: Sig a -> Sig a -> Bool

(<=) :: Sig a -> Sig a -> Bool

(>) :: Sig a -> Sig a -> Bool

(>=) :: Sig a -> Sig a -> Bool

max :: Sig a -> Sig a -> Sig a

min :: Sig a -> Sig a -> Sig a

Read a => Read (Sig a)

Defined in Data.DecisionDiagram.BDD.Internal.Node

Methods

readsPrec :: Int -> ReadS (Sig a)

readList :: ReadS [Sig a]

readPrec :: ReadPrec (Sig a)

readListPrec :: ReadPrec [Sig a]

Show a => Show (Sig a)

Defined in Data.DecisionDiagram.BDD.Internal.Node

Methods

showsPrec :: Int -> Sig a -> ShowS

show :: Sig a -> String

showList :: [Sig a] -> ShowS

Generic (Sig a)

Defined in Data.DecisionDiagram.BDD.Internal.Node

Associated Types

type Rep (Sig a) :: Type -> Type

Methods

from :: Sig a -> Rep (Sig a) x

to :: Rep (Sig a) x -> Sig a

Hashable a => Hashable (Sig a)

Defined in Data.DecisionDiagram.BDD.Internal.Node

Methods

hashWithSalt :: Int -> Sig a -> Int

hash :: Sig a -> Int

type Rep (Sig a)

Defined in Data.DecisionDiagram.BDD.Internal.Node

type Rep (Sig a) = D1 ('MetaData "Sig" "Data.DecisionDiagram.BDD.Internal.Node" "decision-diagrams-0.2.0.0-BSEhlfGrdNZAqDzeTNl72J" 'False) (C1 ('MetaCons "SLeaf" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Bool)) :+: C1 ('MetaCons "SBranch" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a))))

pattern SEmpty :: Sig a

Synonym of SLeaf False

pattern SBase :: Sig a

Synonym of SLeaf True

inSig :: Sig (ZDD a) -> ZDD a

Sig-algebra stucture of ZDD, \(\mathrm{in}_\mathrm{Sig}\).

outSig :: ZDD a -> Sig (ZDD a)

Sig-coalgebra stucture of ZDD, \(\mathrm{out}_\mathrm{Sig}\).

Fold

fold :: (Int -> b -> b -> b) -> (Bool -> b) -> ZDD a -> b

Fold over the graph structure of the ZDD.

It takes two functions that substitute Branch and Leaf respectively.

Note that its type is isomorphic to (Sig b -> b) -> ZDD a -> b.

fold' :: (Int -> b -> b -> b) -> (Bool -> b) -> ZDD a -> b

Strict version of fold

Unfold

unfoldHashable :: forall a b. (ItemOrder a, Eq b, Hashable b) => (b -> Sig b) -> b -> ZDD a

Top-down construction of ZDD, memoising internal states using Hashable instance.

unfoldOrd :: forall a b. (ItemOrder a, Ord b) => (b -> Sig b) -> b -> ZDD a

Top-down construction of ZDD, memoising internal states using Ord instance.

Minimal hitting sets

minimalHittingSets :: forall a. ItemOrder a => ZDD a -> ZDD a

See minimalHittingSetsToda.

>>> toSetOfIntSets (minimalHittingSets (fromListOfIntSets (map IntSet.fromList [[1], [2,3,5], [2,3,6], [2,4,5], [2,4,6]]) :: ZDD AscOrder))
fromList [fromList [1,2],fromList [1,3,4],fromList [1,5,6]]

minimalHittingSetsToda :: forall a. ItemOrder a => ZDD a -> ZDD a

Minimal hitting sets.

• T. Toda, “Hypergraph Transversal Computation with Binary Decision Diagrams,” SEA 2013: Experimental Algorithms. Available: http://dx.doi.org/10.1007/978-3-642-38527-8_10.
• HTC-BDD: Hypergraph Transversal Computation with Binary Decision Diagrams https://www.disc.lab.uec.ac.jp/toda/htcbdd.html

minimalHittingSetsKnuth :: forall a. ItemOrder a => ZDD a -> ZDD a

Minimal hitting sets.

D. E. Knuth, "The Art of Computer Programming, Volume 4A: Combinatorial Algorithms, Part 1," Addison-Wesley Professional, 2011.

minimalHittingSetsImai :: forall a. ItemOrder a => ZDD a -> ZDD a

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/.

Random sampling

uniformM :: forall a g m. (ItemOrder a, StatefulGen g m, HasCallStack) => ZDD a -> g -> m IntSet

Sample a set from uniform distribution over elements of the ZDD.

The function constructs a table internally and the table is shared across multiple use of the resulting action (m IntSet). Therefore, the code

let g = uniformM zdd gen
s1 <- g
s2 <- g

is more efficient than

s1 <- uniformM zdd gen
s2 <- uniformM zdd gen

.

Min/Max

findMinSum :: forall a w. (ItemOrder a, Num w, Ord w, HasCallStack) => (Int -> w) -> ZDD a -> (w, IntSet)

Find a minimum element set with respect to given weight function

\[ \min_{X\in S} \sum_{x\in X} w(x) \]

findMaxSum :: forall a w. (ItemOrder a, Num w, Ord w, HasCallStack) => (Int -> w) -> ZDD a -> (w, IntSet)

Find a maximum element set with respect to given weight function

\[ \max_{X\in S} \sum_{x\in X} w(x) \]

>>> findMaxSum (IntMap.fromList [(1,2),(2,4),(3,-3)] IntMap.!) (fromListOfIntSets (map IntSet.fromList [[1], [2], [3], [1,2,3]]) :: ZDD AscOrder)
(4,fromList [2])

Misc

flatten :: ItemOrder a => ZDD a -> IntSet

Unions of all member sets

>>> flatten (fromListOfIntSets (map IntSet.fromList [[1,2,3], [1,3], [3,4]]) :: ZDD AscOrder)
fromList [1,2,3,4]

Conversion

toListOfIntSets :: ZDD a -> [IntSet]

Convert the family to a list of IntSet.

toSetOfIntSets :: ZDD a -> Set IntSet

Convert the family to a set of IntSet.

Conversion from/to graphs

type Graph f = IntMap (f Int)

Graph where nodes are decorated using a functor f.

The occurrences of the parameter of f represent out-going edges.

toGraph :: ZDD a -> (Graph Sig, Int)

Convert a ZDD into a pointed graph

Nodes 0 and 1 are reserved for SLeaf False and SLeaf True even if they are not actually used. Therefore the result may be larger than numNodes if the leaf nodes are not used.

toGraph' :: Traversable t => t (ZDD a) -> (Graph Sig, t Int)

Convert multiple ZDDs into a graph

fromGraph :: HasCallStack => (Graph Sig, Int) -> ZDD a

Convert a pointed graph into a ZDD

fromGraph' :: HasCallStack => Graph Sig -> IntMap (ZDD a)

Convert nodes of a graph into ZDDs