BinaryDecisionDiagrams Documentation

A Binary Decision Diagram.

• index: the vertex variable (-1 if terminal vertex
• low: low child vertex of BDD (undef if terminal vertex)
• high: high child vertex of BDD (undef if terminal vertex)
• value: terminal boolean value
• id: unique identifier

Returns whether the two given boolean functions are not equivalent.

Returns whether the two given boolean functions are equivalent.

Returns a new reduced Diagram restricted to instantiation X.

Returns a xor of the given boolean functions.

Returns a unique hash for the whole BDD.

Returns 0 if x is not a literal; else returns the literal's sign.

Returns the number of nodes in the BDD graph.

Return string representation of Diagram α.

Negates this boolean function.

Returns a conjunction over the given boolean functions.

Returns a disjunction over the given boolean functions.

Computes all possible valuations of scope V and returns as a BitMatrix. Up to 64 variables.

Returns a conjunction over the given boolean functions.

Returns a Diagram canonical representation of α ⊕ β, where ⊕ is some binary operator.

Recursively computes α ⊕ β. If the result was already computed as an intermediate result, return the cached result in T.

Constructs a BDD mapping to true if at least n literals in L are in the input; otherwise false.

Constructs a BDD mapping to true if at least n literals in L are in the input; otherwise false.

Constructs a BDD mapping to true if at most n literals in L are in the input; otherwise false.

Constructs a BDD mapping to true if at most n literals in L are in the input; otherwise false.

Computes all possible valuations of scope V as conjunctions.

Computes all possible valuations of scope V as both conjunctions and instantiation values.

Returns an approximation (does not account for some repeated nodes) of how many times each variable is mentioned in α.

Eliminate a variable through disjunction. Equivalent to the expression (ϕ|x ∨ ϕ|¬x).

Constructs a BDD mapping to true if exactly n literals in L are in the input; otherwise false.

Constructs a BDD mapping to true if exactly n literals in L are in the input; otherwise false.

Returns the resulting BDD after applying the forget operation. Equivalent to $\phi|_x \vee \phi|_{\neg x}$.

Translates a cardinality constraint in normal pseudo-boolean constraint form into a BDD.

Since cardinality constraints correspond to having coefficients set to one, we ignore the C's.

Argument L corresponds to the vector of literals to be chosen from; b is how many literals in L are selected.

See Eén and Sörensson 2006.

Returns whether the given Diagram node is an atomic formula (i.e. a variable, ⊥, ⊤, or literal).

Returns whether the given Diagram node represents a literal.

Returns whether this Diagram node is terminal.

Returns whether the given Diagram node represents a variable.

Returns whether the given Diagram node represents a ⊤.

Returns whether the given Diagram node represents a ⊥.

Returns whether a variable x appears as a positive literal in α, given that α is a conjunction of literals.

Assumes ϕ is a full conjunction of literals. Returns ϕ as a zero-one vector and its scope.

Loads a BDD from given file.

Supported file formats:

• CNF (.cnf);
• DNF (.dnf);
• BDD (.bdd).

To load as any of these file formats, simply set the filename with the desired extension.

Keyword arguments are passed down to the open function.

Loads a BDD from a file. Use load instead.

Loads a CNF as a BDD. Use load instead.

Loads a CNF as a BDD. Use load instead.

Computes a mapping of the parents of each node.

Marginalize a variable through some binary operation.

Returns whether the formula (i.e. BDD) mentions a variable.

Runs a BFS on the mapping of parents, starting from either a ⊤ (true) or ⊥ (false) in order to find the corresponding CNF or DNF encoding.

Returns a disjunction over the given boolean functions.

Returns a Vector{Diagram} containing all nodes in α in post-order.

Pretty print a conjunction of literals BDD.

Pretty print BDD as a normal form (CNF or DNF).

Caution: may exponentially explode.

Alternatively, pretty prints using the given glyphs (default ∧, ∨ and ¬).

ϕ = (1 ∧ ¬2) ∨ (2 ∧ 3)
print_nf(α; out = false)

ϕ = (1 ∧ ¬2) ∨ (2 ∧ 3)
print_nf(α; out = false, which = "dnf", glyphs = ['+', '*', '-'])

Reduce a Diagram rooted at α inplace, removing duplicate nodes and redundant sub-trees. Returns canonical representation of α.

Returns a new reduced Diagram restricted to instantiation X.

Returns a new Diagram restricted to instantiation X.

Returns a new Diagram restricted to instantiation X.

Saves a BDD as a file.

Supported file formats:

• CNF (.cnf);
• DNF (.dnf);
• BDD (.bdd).

To save as any of these file formats, simply set the filename with the desired extension.

Keyword arguments are passed down to the open function.

Save as BDD. Use the save function instead.

Save as CNF. Use the save function instead.

Save as DNF. Use the save function instead.

Returns all variables in this formula as a Vector{Int}.

Returns all variables in this formula as a Set{Int}.

Returns a shallow hash for the given node (not BDD as a whole).

Performs Shannon's Decomposition on the Diagram α, given a set of variables to isolate. Any decomposition that results in a ⊥ is discarded.

Performs Shannon's Decomposition on the Diagram α, given a variable to isolate.

Performs Shannon's Decomposition on the Diagram α, given a set of variables to isolate.

Returns a new terminal node of given boolean value.

Returns 0 if x is not a literal; else returns an integer representation of x.

Returns α as an integer literal. Assumes α is a leaf node.

Compute all possible valuations of scope V.

Returns a Diagram representing a single variable. If negative, negate variable.