# BinaryDecisionDiagrams Documentation

## API

BinaryDecisionDiagrams.DiagramType

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
BinaryDecisionDiagrams.from_npbcMethod

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.

BinaryDecisionDiagrams.loadMethod

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.

BinaryDecisionDiagrams.print_nfMethod

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 = ['+', '*', '-'])
BinaryDecisionDiagrams.saveMethod

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.