Class BinaryDecisionDiagram

Namespace: LogicalOptimizer

Assembly: LogicalOptimizer.Bdd.dll

Reduced Ordered Binary Decision Diagram over a variable order, with a shared unique table (hash-consing) and memoized ite. Because ROBDDs are canonical, two expressions are equivalent exactly when they build to the same node — ideal for repeated equivalence queries against one baseline. A node budget turns pathological orderings into a clean exception instead of memory blowup (callers can fall back to the SAT-based EquivalenceChecker).

The diagram uses CUDD-style complement edges: an "edge" is an int that packs a node index and a complement bit (the low bit); a function and its negation share the very same node, halving memory, and Negate(int) is an O(1) bit flip. There is a single terminal node (ONE); FALSE is the complemented edge to it. The canonical invariant is that the THEN (high) edge of every stored node is always regular (non-complemented); when a node would be built with a complemented then-edge, both children are complemented and a complemented edge to the normalized node is returned. That single rule keeps the representation canonical, so equivalence is still edge equality.

Variable position is decoupled from variable identity: the stored Variable field of a node is a stable variable id, and LogicalOptimizer.BinaryDecisionDiagram._varLevel maps each id to its current level (position, top to bottom). That indirection lets BuildWithSiftedOrder(AstNode, int, int, CancellationToken) reorder variables in place with adjacent-level swaps instead of rebuilding the whole diagram.

public sealed class BinaryDecisionDiagram

Inheritance: object

BinaryDecisionDiagram

Inherited Members: object.Equals(object)

object.Equals(object, object)

object.GetHashCode()

object.GetType()

object.ReferenceEquals(object, object)

object.ToString()

Fields

DefaultNodeBudget

public const int DefaultNodeBudget = 1000000

Field Value

int

Properties

NodeCount

Live node count including the single terminal.

public int NodeCount { get; }

Property Value

int

Variables

Variable names in current top-to-bottom (level) order.

public IReadOnlyList<string> Variables { get; }

Property Value

IReadOnlyList<string>

Methods

AreEquivalent(AstNode, AstNode, int)

Canonical equivalence: build both sides in one manager and compare roots. Null when the node budget was exceeded (verdict unknown — fall back to SAT).

public static bool? AreEquivalent(AstNode left, AstNode right, int nodeBudget = 1000000)

Parameters

left AstNode
right AstNode
nodeBudget int

Returns

bool?

Build(AstNode, int, CancellationToken)

Build a diagram for one expression in its own manager.

public static BinaryDecisionDiagram Build(AstNode ast, int nodeBudget = 1000000, CancellationToken cancellationToken = default)

Parameters

ast AstNode
nodeBudget int
cancellationToken CancellationToken

Returns

BinaryDecisionDiagram

BuildWithBestOrder(AstNode, int, CancellationToken)

Build trying several variable-order heuristics (sorted, first-appearance DFS, reversed) and keep the smallest diagram. The order is the dominant factor in BDD size — e.g. an adder ordered a1,b1,a2,b2 is linear while a1,a2,b1,b2 is exponential. Orders whose build exceeds the budget are skipped; throws only when every candidate exceeds it.

public static BinaryDecisionDiagram BuildWithBestOrder(AstNode ast, int nodeBudget = 1000000, CancellationToken cancellationToken = default)

Parameters

ast AstNode
nodeBudget int
cancellationToken CancellationToken

Returns

BinaryDecisionDiagram

BuildWithSiftedOrder(AstNode, int, int, CancellationToken)

Sifting (Rudell-style, in place): starting from the best heuristic order, each variable in turn is bubbled up to the top and down to the bottom using only adjacent-level swaps and left where the diagram is smallest; passes repeat until one finds no improvement. Unlike a rebuild, a single swap rewrites only the two affected levels, so this is far cheaper than reconstructing the diagram per trial position while finding orders the static heuristics cannot. The number of trial swaps is bounded by maxRebuilds; the result is never larger than BuildWithBestOrder(AstNode, int, CancellationToken).

public static BinaryDecisionDiagram BuildWithSiftedOrder(AstNode ast, int nodeBudget = 1000000, int maxRebuilds = 400, CancellationToken cancellationToken = default)

Parameters

ast AstNode
nodeBudget int
maxRebuilds int
cancellationToken CancellationToken

Returns

BinaryDecisionDiagram

CountSatisfyingAssignments()

Number of satisfying assignments of the built function over all manager variables.

public BigInteger CountSatisfyingAssignments()

Returns

BigInteger

EnumerateSatisfyingAssignments()

Lazily enumerate ALL total satisfying assignments in lexicographic variable order (false before true). The count can be exponential — combine with Take/TakeWhile or use CountSatisfyingAssignments() first.

public IEnumerable<IReadOnlyDictionary<string, bool>> EnumerateSatisfyingAssignments()

Returns

IEnumerable<IReadOnlyDictionary<string, bool>>

Evaluate(IReadOnlyDictionary<string, bool>)

Evaluate the built function at one assignment (defaults missing variables to false).

public bool Evaluate(IReadOnlyDictionary<string, bool> assignment)

Parameters

assignment IReadOnlyDictionary<string, bool>

Returns

bool

FindSatisfyingAssignment()

A total assignment satisfying the function. Any non-false node has one: reduction collapses all-zero subgraphs into the false terminal itself.

public IReadOnlyDictionary<string, bool> FindSatisfyingAssignment()

Returns

IReadOnlyDictionary<string, bool>

IsContradiction()

The built function is constant false.

public bool IsContradiction()

Returns

bool

IsTautology()

The built function is constant true.

public bool IsTautology()

Returns

bool

Load(Stream, ResourceBudget?, CancellationToken)

Experimental (until v4). Read a diagram back from a blob produced by Save(Stream) into a valid hash-consed manager. The load is fully validated — magic, format version (a newer version is refused, not misread), engine byte (a d-DNNF blob is a typed error here), CRC-32 checksum, and the node table's structure: a genuine variable-order permutation, variable indices in range, children strictly before their parent (acyclic) and at a deeper level (a reduced ORDERED diagram), no duplicate or redundant nodes, and a valid root. The checksum only catches corruption; it does not replace the structural checks.

The read is budgeted and never trusts a length field to pre-size an allocation: a header claiming a huge node count is checked against budget and against the actual stream, so a hostile blob aborts with NodeBudgetExceededException or a truncation error rather than allocating unboundedly. Any malformed input is a CircuitSerializationException.

public static BinaryDecisionDiagram Load(Stream source, ResourceBudget? budget = null, CancellationToken cancellationToken = default)

Parameters

source Stream: The stream to read the blob from.
budget ResourceBudget: Load budget; the node table is bounded by BddNodeLimit. Defaults to Default.
cancellationToken CancellationToken: Cancels a long load.

Returns

BinaryDecisionDiagram

Exceptions

ArgumentNullException: source is null.
CircuitSerializationException: The blob is malformed, corrupt, a newer version, or the wrong engine.
NodeBudgetExceededException: The blob's declared size exceeds the load budget.
OperationCanceledException: The token was cancelled.

Save(Stream)

Experimental (until v4). Serialize this diagram to a compact, self-describing binary blob (little-endian, CRC-32 checked). The output is deterministic — the same diagram always produces identical bytes — and can be read back with Load(Stream, ResourceBudget?, CancellationToken) into a valid hash-consed manager whose queries (variable set, model count, evaluation, enumeration) answer identically. Both the variable identities and the current variable ORDER are stored, so a sifted order round-trips exactly.

The format is EXPERIMENTAL: it may change before v4 and carries no cross-version compatibility guarantee other than the version gate, which makes a future build refuse (rather than misread) a blob it does not understand. The engine byte makes a BDD blob a typed error if it is loaded as a d-DNNF circuit. No reflection or object deserialization is used.

public void Save(Stream destination)

Parameters

destination Stream: The stream the blob is written to.

Exceptions

ArgumentNullException: destination is null.