BinaryDecisionDiagrams Documentation
API
BinaryDecisionDiagrams.Diagram
— TypeA Binary Decision Diagram.
index
: the vertex variable (-1 if terminal vertexlow
: low child vertex of BDD (undef if terminal vertex)high
: high child vertex of BDD (undef if terminal vertex)value
: terminal boolean valueid
: unique identifier
Base.:!=
— MethodReturns whether the two given boolean functions are not equivalent.
Base.:==
— MethodReturns whether the two given boolean functions are equivalent.
Base.:|
— MethodReturns a new reduced Diagram restricted to instantiation X.
Base.:⊻
— MethodReturns a xor of the given boolean functions.
Base.hash
— MethodReturns a unique hash for the whole BDD.
Base.sign
— MethodReturns 0 if x is not a literal; else returns the literal's sign.
Base.size
— MethodReturns the number of nodes in the BDD graph.
Base.string
— MethodReturn string representation of Diagram α.
BinaryDecisionDiagrams.:¬
— MethodNegates this boolean function.
BinaryDecisionDiagrams.:∧
— MethodReturns a conjunction over the given boolean functions.
BinaryDecisionDiagrams.:∨
— MethodReturns a disjunction over the given boolean functions.
BinaryDecisionDiagrams.all_valuations
— MethodComputes all possible valuations of scope V and returns as a BitMatrix. Up to 64 variables.
BinaryDecisionDiagrams.and
— MethodReturns a conjunction over the given boolean functions.
BinaryDecisionDiagrams.apply
— MethodReturns a Diagram canonical representation of α ⊕ β, where ⊕ is some binary operator.
BinaryDecisionDiagrams.apply_step
— MethodRecursively computes α ⊕ β. If the result was already computed as an intermediate result, return the cached result in T.
BinaryDecisionDiagrams.atleast!
— MethodConstructs a BDD mapping to true if at least n literals in L are in the input; otherwise false.
BinaryDecisionDiagrams.atleast
— MethodConstructs a BDD mapping to true if at least n literals in L are in the input; otherwise false.
BinaryDecisionDiagrams.atmost!
— MethodConstructs a BDD mapping to true if at most n literals in L are in the input; otherwise false.
BinaryDecisionDiagrams.atmost
— MethodConstructs a BDD mapping to true if at most n literals in L are in the input; otherwise false.
BinaryDecisionDiagrams.conjunctions
— MethodComputes all possible valuations of scope V as conjunctions.
BinaryDecisionDiagrams.convals
— MethodComputes all possible valuations of scope V as both conjunctions and instantiation values.
BinaryDecisionDiagrams.culledfreqs
— MethodReturns an approximation (does not account for some repeated nodes) of how many times each variable is mentioned in α.
BinaryDecisionDiagrams.eliminate
— MethodEliminate a variable through disjunction. Equivalent to the expression (ϕ|x ∨ ϕ|¬x).
BinaryDecisionDiagrams.exactly!
— MethodConstructs a BDD mapping to true if exactly n literals in L are in the input; otherwise false.
BinaryDecisionDiagrams.exactly
— MethodConstructs a BDD mapping to true if exactly n literals in L are in the input; otherwise false.
BinaryDecisionDiagrams.forget
— MethodReturns the resulting BDD after applying the forget
operation. Equivalent to $\phi|_x \vee \phi|_{\neg x}$.
BinaryDecisionDiagrams.from_npbc
— MethodTranslates 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.
BinaryDecisionDiagrams.is_atom
— MethodReturns whether the given Diagram node is an atomic formula (i.e. a variable, ⊥, ⊤, or literal).
BinaryDecisionDiagrams.is_lit
— MethodReturns whether the given Diagram node represents a literal.
BinaryDecisionDiagrams.is_term
— MethodReturns whether this Diagram node is terminal.
BinaryDecisionDiagrams.is_var
— MethodReturns whether the given Diagram node represents a variable.
BinaryDecisionDiagrams.is_⊤
— MethodReturns whether the given Diagram node represents a ⊤.
BinaryDecisionDiagrams.is_⊥
— MethodReturns whether the given Diagram node represents a ⊥.
BinaryDecisionDiagrams.lit_val
— MethodReturns whether a variable x appears as a positive literal in α, given that α is a conjunction of literals.
BinaryDecisionDiagrams.lit_vec
— MethodAssumes ϕ is a full conjunction of literals. Returns ϕ as a zero-one vector and its scope.
BinaryDecisionDiagrams.load
— MethodLoads 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.
BinaryDecisionDiagrams.load_bdd
— MethodLoads a BDD from a file. Use load
instead.
BinaryDecisionDiagrams.load_cnf
— MethodLoads a CNF as a BDD. Use load
instead.
BinaryDecisionDiagrams.load_dnf
— MethodLoads a CNF as a BDD. Use load
instead.
BinaryDecisionDiagrams.map_parents
— MethodComputes a mapping of the parents of each node.
BinaryDecisionDiagrams.marginalize
— MethodMarginalize a variable through some binary operation.
BinaryDecisionDiagrams.mentions
— MethodReturns whether the formula (i.e. BDD) mentions a variable.
BinaryDecisionDiagrams.normal_form
— MethodRuns a BFS on the mapping of parents, starting from either a ⊤ (true) or ⊥ (false) in order to find the corresponding CNF or DNF encoding.
BinaryDecisionDiagrams.or
— MethodReturns a disjunction over the given boolean functions.
BinaryDecisionDiagrams.postorder
— MethodReturns a Vector{Diagram}
containing all nodes in α
in post-order.
BinaryDecisionDiagrams.print_conjunction
— MethodPretty print a conjunction of literals BDD.
BinaryDecisionDiagrams.print_nf
— MethodPretty 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 = ['+', '*', '-'])
BinaryDecisionDiagrams.reduce!
— MethodReduce a Diagram rooted at α inplace, removing duplicate nodes and redundant sub-trees. Returns canonical representation of α.
BinaryDecisionDiagrams.restrict
— MethodReturns a new reduced Diagram restricted to instantiation X.
BinaryDecisionDiagrams.restrict_step
— MethodReturns a new Diagram restricted to instantiation X.
BinaryDecisionDiagrams.restrict_step
— MethodReturns a new Diagram restricted to instantiation X.
BinaryDecisionDiagrams.save
— MethodSaves 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.
BinaryDecisionDiagrams.save_bdd
— MethodSave as BDD. Use the save
function instead.
BinaryDecisionDiagrams.save_cnf
— MethodSave as CNF. Use the save
function instead.
BinaryDecisionDiagrams.save_dnf
— MethodSave as DNF. Use the save
function instead.
BinaryDecisionDiagrams.scope
— MethodReturns all variables in this formula as a Vector{Int}.
BinaryDecisionDiagrams.scopeset
— MethodReturns all variables in this formula as a Set{Int}.
BinaryDecisionDiagrams.shallowhash
— FunctionReturns a shallow hash for the given node (not BDD as a whole).
BinaryDecisionDiagrams.shannon!
— MethodPerforms Shannon's Decomposition on the Diagram α, given a set of variables to isolate. Any decomposition that results in a ⊥ is discarded.
BinaryDecisionDiagrams.shannon
— MethodPerforms Shannon's Decomposition on the Diagram α, given a variable to isolate.
BinaryDecisionDiagrams.shannon
— MethodPerforms Shannon's Decomposition on the Diagram α, given a set of variables to isolate.
BinaryDecisionDiagrams.terminal
— MethodReturns a new terminal node of given boolean value.
BinaryDecisionDiagrams.to_int
— MethodReturns 0 if x is not a literal; else returns an integer representation of x.
BinaryDecisionDiagrams.to_lit
— MethodReturns α as an integer literal. Assumes α is a leaf node.
BinaryDecisionDiagrams.valuations
— MethodCompute all possible valuations of scope V.
BinaryDecisionDiagrams.variable
— MethodReturns a Diagram representing a single variable. If negative, negate variable.
Index
BinaryDecisionDiagrams.Diagram
Base.:!=
Base.:==
Base.:|
Base.:⊻
Base.hash
Base.sign
Base.size
Base.string
BinaryDecisionDiagrams.:¬
BinaryDecisionDiagrams.:∧
BinaryDecisionDiagrams.:∨
BinaryDecisionDiagrams.all_valuations
BinaryDecisionDiagrams.and
BinaryDecisionDiagrams.apply
BinaryDecisionDiagrams.apply_step
BinaryDecisionDiagrams.atleast
BinaryDecisionDiagrams.atleast!
BinaryDecisionDiagrams.atmost
BinaryDecisionDiagrams.atmost!
BinaryDecisionDiagrams.conjunctions
BinaryDecisionDiagrams.convals
BinaryDecisionDiagrams.culledfreqs
BinaryDecisionDiagrams.eliminate
BinaryDecisionDiagrams.exactly
BinaryDecisionDiagrams.exactly!
BinaryDecisionDiagrams.forget
BinaryDecisionDiagrams.from_npbc
BinaryDecisionDiagrams.is_atom
BinaryDecisionDiagrams.is_lit
BinaryDecisionDiagrams.is_term
BinaryDecisionDiagrams.is_var
BinaryDecisionDiagrams.is_⊤
BinaryDecisionDiagrams.is_⊥
BinaryDecisionDiagrams.lit_val
BinaryDecisionDiagrams.lit_vec
BinaryDecisionDiagrams.load
BinaryDecisionDiagrams.load_bdd
BinaryDecisionDiagrams.load_cnf
BinaryDecisionDiagrams.load_dnf
BinaryDecisionDiagrams.map_parents
BinaryDecisionDiagrams.marginalize
BinaryDecisionDiagrams.mentions
BinaryDecisionDiagrams.normal_form
BinaryDecisionDiagrams.or
BinaryDecisionDiagrams.postorder
BinaryDecisionDiagrams.print_conjunction
BinaryDecisionDiagrams.print_nf
BinaryDecisionDiagrams.reduce!
BinaryDecisionDiagrams.restrict
BinaryDecisionDiagrams.restrict_step
BinaryDecisionDiagrams.restrict_step
BinaryDecisionDiagrams.save
BinaryDecisionDiagrams.save_bdd
BinaryDecisionDiagrams.save_cnf
BinaryDecisionDiagrams.save_dnf
BinaryDecisionDiagrams.scope
BinaryDecisionDiagrams.scopeset
BinaryDecisionDiagrams.shallowhash
BinaryDecisionDiagrams.shannon
BinaryDecisionDiagrams.shannon
BinaryDecisionDiagrams.shannon!
BinaryDecisionDiagrams.terminal
BinaryDecisionDiagrams.to_int
BinaryDecisionDiagrams.to_lit
BinaryDecisionDiagrams.valuations
BinaryDecisionDiagrams.variable