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 Empty :: ZDD a

pattern Base :: 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

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 set (∅).

base :: ZDD a

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

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

Create a ZDD that contains only a given set.

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

Set of all subsets, i.e. powerset

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

Insertion

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

Insert a set into the ZDD.

Deletion

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

Delete a set from the ZDD.

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 set?

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

The number of sets in the family.

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 sets are disjoint (i.e., their intersection is empty).

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.

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

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

Subsets that does not contain a particular element

Map

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

Insert an item into each element set of ZDD.

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

Delete an item from each element set of ZDD.

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}

Fold

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

Fold over the graph structure of the ZDD.

It takes values for substituting empty and base, and a function for substiting non-terminal node.

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

Strict version of fold

Minimal hitting sets

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

See minimalHittingSetsToda.

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) => 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) => (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) => (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) \]

Misc

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

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 = IntMap Node

data Node

Constructors

NodeEmpty

NodeBase

NodeBranch !Int Int Int

Instances

Eq Node

Defined in Data.DecisionDiagram.ZDD

Methods

(==) :: Node -> Node -> Bool

(/=) :: Node -> Node -> Bool

Read Node

Defined in Data.DecisionDiagram.ZDD

Methods

readsPrec :: Int -> ReadS Node

readList :: ReadS [Node]

readPrec :: ReadPrec Node

readListPrec :: ReadPrec [Node]

Show Node

Defined in Data.DecisionDiagram.ZDD

Methods

showsPrec :: Int -> Node -> ShowS

show :: Node -> String

showList :: [Node] -> ShowS

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

Convert a ZDD into a pointed graph

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

Convert multiple ZDDs into a graph

fromGraph :: (Graph, Int) -> ZDD a

Convert a pointed graph into a ZDD

fromGraph' :: Graph -> IntMap (ZDD a)

Convert nodes of a graph into ZDDs