Data.DecisionDiagram.BDD

Reduced Ordered Binary Decision Diagrams (ROBDD).

References:

• Bryant, "Graph-Based Algorithms for Boolean Function Manipulation," in IEEE Transactions on Computers, vol. C-35, no. 8, pp. 677-691, Aug. 1986, doi: 10.1109/TC.1986.1676819. https://www.cs.cmu.edu/~bryant/pubdir/ieeetc86.pdf

The BDD type

data BDD a where

Reduced ordered binary decision diagram representing boolean function

Bundled Patterns

pattern Leaf :: Bool -> BDD a

pattern Branch :: Int -> BDD a -> BDD a -> BDD a

Smart constructor that takes the BDD reduction rules into account

Instances

Eq (BDD a)

Defined in Data.DecisionDiagram.BDD

Methods

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

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

Read (BDD a)

Defined in Data.DecisionDiagram.BDD

Methods

readsPrec :: Int -> ReadS (BDD a)

readList :: ReadS [BDD a]

readPrec :: ReadPrec (BDD a)

readListPrec :: ReadPrec [BDD a]

Show (BDD a)

Defined in Data.DecisionDiagram.BDD

Methods

showsPrec :: Int -> BDD a -> ShowS

show :: BDD a -> String

showList :: [BDD a] -> ShowS

Hashable (BDD a)

Defined in Data.DecisionDiagram.BDD

Methods

hashWithSalt :: Int -> BDD a -> Int

hash :: BDD a -> Int

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

Boolean operations

true :: BDD a

True

false :: BDD a

False

var :: Int -> BDD a

A variable \(x_i\)

notB :: BDD a -> BDD a

Negation of a boolean function

(.&&.) :: forall a. ItemOrder a => BDD a -> BDD a -> BDD a infixr 3

Conjunction of two boolean function

(.||.) :: forall a. ItemOrder a => BDD a -> BDD a -> BDD a infixr 2

Disjunction of two boolean function

xor :: forall a. ItemOrder a => BDD a -> BDD a -> BDD a

XOR

(.=>.) :: forall a. ItemOrder a => BDD a -> BDD a -> BDD a infixr 1

Implication

(.<=>.) :: forall a. ItemOrder a => BDD a -> BDD a -> BDD a infix 1

Equivalence

ite :: forall a. ItemOrder a => BDD a -> BDD a -> BDD a -> BDD a

If-then-else

andB :: forall f a. (Foldable f, ItemOrder a) => f (BDD a) -> BDD a

Conjunction of a list of BDDs.

orB :: forall f a. (Foldable f, ItemOrder a) => f (BDD a) -> BDD a

Disjunction of a list of BDDs.

Pseudo-boolean constraints

pbAtLeast :: forall a w. (ItemOrder a, Real w) => IntMap w -> w -> BDD a

Pseudo-boolean constraint, w1*x1 + w2*x2 + … ≥ k.

pbAtMost :: forall a w. (ItemOrder a, Real w) => IntMap w -> w -> BDD a

Pseudo-boolean constraint, w1*x1 + w2*x2 + … ≤ k.

pbExactly :: forall a w. (ItemOrder a, Real w) => IntMap w -> w -> BDD a

Pseudo-boolean constraint, w1*x1 + w2*x2 + … = k.

If weight type is Integral, pbExactlyIntegral is more efficient.

pbExactlyIntegral :: forall a w. (ItemOrder a, Real w, Integral w) => IntMap w -> w -> BDD a

Similar to pbExactly but more efficient.

Quantification

forAll :: forall a. ItemOrder a => Int -> BDD a -> BDD a

Universal quantification (∀)

exists :: forall a. ItemOrder a => Int -> BDD a -> BDD a

Existential quantification (∃)

existsUnique :: forall a. ItemOrder a => Int -> BDD a -> BDD a

Unique existential quantification (∃!)

forAllSet :: forall a. ItemOrder a => IntSet -> BDD a -> BDD a

Universal quantification (∀) over a set of variables

existsSet :: forall a. ItemOrder a => IntSet -> BDD a -> BDD a

Existential quantification (∃) over a set of variables

existsUniqueSet :: forall a. ItemOrder a => IntSet -> BDD a -> BDD a

Unique existential quantification (∃!) over a set of variables

Query

support :: BDD a -> IntSet

All the variables that this BDD depends on.

evaluate :: (Int -> Bool) -> BDD a -> Bool

Evaluate a boolean function represented as BDD under the valuation given by (Int -> Bool), i.e. it lifts a valuation function from variables to BDDs.

numNodes :: BDD a -> Int

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

See also toGraph.

Restriction / Cofactor

restrict :: forall a. ItemOrder a => Int -> Bool -> BDD a -> BDD a

Compute \(F|_{x_i} \) or \(F|_{\neg x_i} \).

\[ F|_{x_i}(\ldots, x_{i-1}, x_{i+1}, \ldots) = F(\ldots, x_{i-1}, \mathrm{True}, x_{i+1}, \ldots) \] \[ F|_{\neg x_i}(\ldots, x_{i-1}, x_{i+1}, \ldots) = F(\ldots, x_{i-1}, \mathrm{False}, x_{i+1}, \ldots) \]

restrictSet :: forall a. ItemOrder a => IntMap Bool -> BDD a -> BDD a

Compute \(F|_{\{x_i = v_i\}_i} \).

restrictLaw :: forall a. ItemOrder a => BDD a -> BDD a -> BDD a

Compute generalized cofactor of F with respect to C.

Note that C is the first argument.

Substition / Composition

subst :: forall a. ItemOrder a => Int -> BDD a -> BDD a -> BDD a

subst x N M computes substitution M[x ↦ N].

Note the order of the arguments. This operation is also known as Composition.

substSet :: forall a. ItemOrder a => IntMap (BDD a) -> BDD a -> BDD a

Simultaneous substitution.

Note that this is not the same as repeated application of subst.

Satisfiability

anySat :: BDD a -> Maybe (IntMap Bool)

Find one satisfying partial assignment

allSat :: BDD a -> [IntMap Bool]

Enumerate all satisfying partial assignments

anySatComplete :: ItemOrder a => IntSet -> BDD a -> Maybe (IntMap Bool)

Find one satisfying (complete) assignment over a given set of variables

The set of variables must be a superset of support.

allSatComplete :: ItemOrder a => IntSet -> BDD a -> [IntMap Bool]

Enumerate all satisfying (complete) assignment over a given set of variables

The set of variables must be a superset of support.

countSat :: forall a b. (ItemOrder a, Num b, Bits b, HasCallStack) => IntSet -> BDD a -> b

Count the number of satisfying (complete) assignment over a given set of variables.

The set of variables must be a superset of support.

It is polymorphic in return type, but it is recommended to use Integer or Natural because the size can be larger than fixed integer types such as Int64.

>>> countSat (IntSet.fromList [1..128]) (true :: BDD AscOrder)
340282366920938463463374607431768211456
>>> import Data.Int
>>> maxBound :: Int64
9223372036854775807

uniformSatM :: forall a g m. (ItemOrder a, StatefulGen g m, HasCallStack) => IntSet -> BDD a -> g -> m (IntMap Bool)

Sample an assignment from uniform distribution over complete satisfiable assignments (allSatComplete) of the BDD.

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 = uniformSatM xs bdd gen
s1 <- g
s2 <- g

is more efficient than

s1 <- uniformSatM xs bdd gen
s2 <- uniformSatM xs bdd gen

.

(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))))

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

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

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

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

Fold

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

Fold over the graph structure of the BDD.

It takes two functions that substitute Branch and Leaf respectively.

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

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

Strict version of fold

Unfold

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

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

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

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

Fixpoints

lfp :: ItemOrder a => (BDD a -> BDD a) -> BDD a

Least fixed point.

Monotonicity of the operator is assumed but not checked.

gfp :: ItemOrder a => (BDD a -> BDD a) -> BDD a

Greatest fixed point.

Monotonicity of the operator is assumed but not checked.

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 :: BDD a -> (Graph Sig, Int)

Convert a BDD 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 (BDD a) -> (Graph Sig, t Int)

Convert multiple BDDs into a graph

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

Convert a pointed graph into a BDD

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

Convert nodes of a graph into BDDs