PaperlayerView exact revision on arXiv

Source-linked AI summary

XBDD: A Highly Optimized ROBDD with Per-Edge Variable-Flip Maps

Yinglong Gan, Jintao Yu, Shenggang Ying, Yusen Li, Xin Hong

arXiv:2609.36778v2cs.DS

TL;DR

Existing ROBDDs do not directly share sub-functions that differ only in input polarity, although complement edges handle output-polarity differences. XBDD adds per-edge variable-flip maps to enable that sharing; on IWLS’93 circuits it reduces node count and memory versus CUDD, with construction-time tradeoffs.

  • Problem

    Existing ROBDD representations capture output-polarity differences with complement edges but do not directly capture input-polarity differences, limiting sharing of related sub-functions.

    Source: §I · p. 1

  • Method

    XBDD associates a variable-flip map with each edge and uses normalization and map-aware cofactor operations to integrate those maps into ROBDD construction.

    Source: §I · pp. 1–2

  • Results

    XBDD reduces final node count by up to 93% and memory consumption by 61% versus CUDD, with construction time ranging from 24% faster to 41% slower.

    Source: §I · p. 2

  • Takeaways & Limitations

    Input-polarity similarity exposes sharing opportunities missed by existing ROBDD representations, and polarity-sensitive function families can shrink from exponential to linear size.

    Source: §I · p. 2

    Constructive uniqueness does not require all syntactically valid XBDD edges for a function to be identical; eliminating symmetry-related forms would require more expensive checks on every XITE call.

    Source: D. Constructive Uniqueness · p. 8

Abstract

from arXiv · show

The Reduced Ordered Binary Decision Diagram (ROBDD) is a canonical representation of Boolean functions and is widely used in tasks such as equivalence checking and satisfiability checking of combinational circuits. Classical ROBDD packages greatly improve the efficiency of building ROBDDs through a series of optimization techniques, and compress the node scale of the ROBDD through complement edges. However, existing implementations do not take into account the local polarity differences of isomorphic Boolean functions, and still produce a distinct node for each polarity combination, thereby causing an explosion in the number of nodes. This paper proposes XBDD, a highly optimized ROBDD that, on the basis of fully implementing complement edges and their accompanying engineering techniques, introduces a per-edge variable-flip map. XBDD attaches a flip map to each edge to indicate which input variables must be negated when that edge is followed. This allows nodes that differ only in local input polarities to be merged, further reducing the node count. For certain function families, this sharing even yields exponential compression. We also propose methods that use a bitmap and a map pool to substantially reduce the extra overhead brought by the map, and propose normalization and cofactor operators for the map. In addition, XBDD implements several other engineering optimizations to further improve both time and space efficiency. Experiments show that XBDD trades a controllable time cost for a significant space gain, validating the effectiveness of the per-edge variable-flip map.

I. INTRODUCTION

XBDD extends complement-edge sharing to input-polarity variants with per-edge variable-flip maps. The paper reports lower node counts and memory use than CUDD on IWLS’93 circuits, alongside a controllable construction-time tradeoff.

I. INTRODUCTION

  • Complement edges capture output-polarity differences, but existing ROBDDs do not directly capture input-polarity differences, leaving some related sub-functions represented separately.The functions may be neither identical nor complements, despite similar computations.Source: §I · p. 1
  • XBDD attaches a variable-flip map to each edge, recording which input variables change polarity so that matching sub-functions can reuse underlying nodes.This extends complement-edge sharing from output-polarity variants to input-polarity variants.Source: §I · p. 1
  • Against CUDD, XBDD reduces final node count by up to 93% and memory consumption by 61%, with construction time ranging from 24% faster to 41% slower.For polarity-sensitive function families, XBDD also reduces representation size from exponential to linear.Source: §I · p. 2
  • Normalization and map-aware cofactor operations establish constructive uniqueness under a fixed variable order, while polarity-sensitive families can shrink from exponential to linear size.The paper develops these operations to integrate maps into ROBDD construction.Source: §I · pp. 1–2
  • Bitmap encoding, map interning, compact node and table structures, and adaptive caching and garbage collection are used to control map overhead.The implementation combines these techniques to keep additional memory and runtime overhead low.Source: §I · pp. 1–2

II. BACKGROUND AND MOTIVATION

  • The background section reviews ROBDD fundamentals and ITE-based construction, then explains how complement edges increase node sharing and motivate XBDD.This frames the gap between sharing identical or complementary sub-functions and sharing input-polarity variants.Source: §II · p. 2

A. Basic Concepts of ROBDD

  • ROBDDs use a fixed variable order and eliminate redundant tests or merge duplicate nodes; under that order, each Boolean function has a unique representation.Unique tables detect equivalent nodes, while computed tables reuse previously evaluated operations.Source: A. Basic Concepts of ROBDD · p. 2

B. ROBDD Construction with ITE

ROBDD construction uses ITE as a common recursive primitive for Boolean operations. It expands at the highest variable, recursively constructs both branches, then reduces and canonicalizes the result through node and operation tables.

B. ROBDD Construction with ITE

  • ITE returns G when F is 1 and H when F is 0.The displayed definition expresses the operator using its three Boolean-function inputs.Source: B. ROBDD Construction with ITE · pp. 2–3
  • ITE provides a common recursive primitive for Boolean operations, including conjunction and direct representation of F.For example, F ∧ G is ite(F, G, 0), while F is ite(F, 0, 1).Source: B. ROBDD Construction with ITE · pp. 2–3
  • ITE selects the highest variable in its fixed order, obtains cofactors, and recursively constructs the two branches before creating a node or eliminating a redundant test.If the two branch results are equal, the test is redundant; otherwise, a node labeled by the selected variable is required.Source: B. ROBDD Construction with ITE · p. 3
  • Conventional ROBDD cofactors come directly from the root’s low and high edges when its variable matches; if the root is below the variable, both cofactors use the same node.Source: B. ROBDD Construction with ITE · p. 3
  • Node construction eliminates equal-child tests and reuses nodes with an existing structural key; a computed table caches ITE calls to avoid repeating recursive work.The unique-table key is (v, E, T).Source: B. ROBDD Construction with ITE · p. 3

C. Complement Edges in ROBDDs

Complement edges let ROBDDs share functions with opposite output polarity, but not sub-functions that differ in input polarity. XBDD adds per-edge variable-flip maps so those input-polarity variants can reuse underlying nodes.

C. Complement Edges in ROBDDs

  • Complement edges let functions with opposite output polarity share underlying nodes, but they do not capture differences in input polarity.This leaves structurally similar sub-functions with input-polarity variants represented separately.Source: C. Complement Edges in ROBDDs · p. 3

III. XBDD DESIGN

  • XBDD encodes input-polarity transformations on edges, allowing a broader class of structurally similar sub-functions to share nodes.The edge carries the polarity transformation rather than requiring separate nodes for variants with opposite input polarities.Source: §III · pp. 3–4, A. Per-Edge Variable-Flip Map · p. 4

A. Per-Edge Variable-Flip Map

  • An XBDD edge carries a target node, a complement bit, and a flip map that transforms selected inputs before evaluation and can complement the output afterward.Each XBDD object has a root edge that determines its function; distinct root edges may reference a shared node DAG.Source: A. Per-Edge Variable-Flip Map · p. 4

B. Normalization and Cofactor

Variable-flip maps allow equivalent structures to arise in multiple forms, so XBDD normalizes nodes before interning them and uses map-aware cofactors to recover branches during construction.

B. Normalization and Cofactor

  • Normalization removes redundant tests, fixes branch order, lifts common edge attributes, and interns the resulting structural key.Deterministic branch ordering and lifting common complement and flip information let equivalent forms reach the same key and reuse a node.Source: B. Normalization and Cofactor · p. 5
  • Normalization preserves the represented Boolean function while converting equivalent forms into a shared structural representation.If branches are swapped, the current variable is added to the incoming flip map to restore the original interpretation.Source: B. Normalization and Cofactor · pp. 5–6
  • Map-aware Cof selects the requested branch after accounting for whether the incoming flip map reverses the current variable.When the high branch is selected, its relative complement bit and flip map compose with the incoming edge; the fixed variable is then removed from the map.Source: B. Normalization and Cofactor · p. 6
  • Norm combines two cofactors into a normalized shared structure, while Cof recovers branches during recursive construction.Together, the operators provide the basis for XITE.Source: B. Normalization and Cofactor · pp. 5–6

C. XBDD Construction

XBDD retains ITE's recursive construction structure, replacing ordinary cofactor extraction and direct branch insertion with map-aware Cof and Norm operations. Its XITE procedure supports Boolean operators through the same high-level construction interface as conventional ROBDDs.

C. XBDD Construction

  • XBDD replaces ordinary cofactor extraction with map-aware Cof and passes recursive branches through Norm before unique-table lookup.Cof selects the correct branch using the incoming flip map; Norm imposes canonical ordering and returns a normalized edge for node sharing.Source: C. XBDD Construction · p. 6
  • XITE retains ITE's recursive structure while computing map-aware cofactors and combining recursive results with Norm.It handles terminal cases and cached results, selects the top variable, recursively solves both subproblems, and normalizes their results.Source: C. XBDD Construction · p. 6
  • Boolean operators including AND, OR, XOR, and NOT use XITE forms analogous to conventional ITE calls.The variable-flip map extends the representation and local edge operations without changing the high-level construction interface.Source: C. XBDD Construction · p. 6
  • Normalization at each nonterminal XITE call provides the basis for unique representations under a fixed variable order.The paper states that edges generated through this construction procedure have a unique representation for their Boolean functions.Source: C. XBDD Construction · pp. 6–7

D. Constructive Uniqueness

Under a fixed variable order, XBDD guarantees uniqueness for edges generated through its construction procedure, preserving root-edge equivalence checks. It deliberately does not require every well-formed edge for a function to have the same form.

D. Constructive Uniqueness

  • Normalization and cofactor extraction are mutually consistent, allowing a generated nonterminal edge to be reconstructed from its two cofactors.Cofactor extraction reverses normalization’s branch exchange and attribute transformations; applying normalization again returns the original edge.Source: D. Constructive Uniqueness · p. 7
  • The uniqueness proof proceeds by induction on variable level, comparing cofactors when both generated edges have the same root variable.When only one edge has a root at the current level, independence of that variable makes the case impossible after redundancy elimination.Source: D. Constructive Uniqueness · p. 7
  • Terminal normalization removes flip-map information, leaving constants with unique terminal representations.Constant 1 is represented by (⊤, 0, ∅), and constant 0 by (⊤, 1, ∅).Source: D. Constructive Uniqueness · p. 7
  • Generated XBDD edges represent the same Boolean function if and only if they are identical, preserving equivalence checks by comparing root edges.This constructive uniqueness applies to representations produced through XITE, not every well-formed XBDD edge.Source: D. Constructive Uniqueness · p. 7
  • Global symmetry analysis could select a preferred form for every equivalent edge, but would make normalization substantially more expensive and burden every XITE call.XBDD instead uses lightweight local normalization and guarantees uniqueness for representations produced through its construction interface.Source: D. Constructive Uniqueness · p. 8

E. Node Compression with Variable-Flip Maps

Variable-flip maps let XBDD share sub-functions that differ only in selected input polarities. For the stated function family, this changes the representation-size bound from Ω(2k) nodes for complement-edge ROBDDs to O(k) nodes for XBDD.

E. Node Compression with Variable-Flip Maps

  • XBDD encodes selected input-polarity differences in incoming edge maps, allowing otherwise distinct polarity variants to share underlying nodes.Fig. 2 contrasts separate ROBDD nodes with XBDD’s shared nodes and edge-map representation.Source: E. Node Compression with Variable-Flip… · p. 8, Figure 2 · p. 8
  • For Fk under the stated variable order, complement-edge ROBDDs require Ω(2k) nodes, while XBDD represents it with O(k) nodes.The proof attributes the difference to polarity variants that cannot be merged by complement edges but share conjunction structure in XBDD.Source: E. Node Compression with Variable-Flip… · p. 8
  • Complement edges cannot merge the family’s 2k pairwise-distinct residual functions because, for k > 1, no two are complements.XBDD instead shares their common conjunction structure and encodes polarity differences in edge maps.Source: E. Node Compression with Variable-Flip… · p. 8
  • For general circuits, the achievable node reduction depends on how often sub-functions differ primarily in input polarity.The exponential-to-linear result is established for a class of polarity-sensitive functions.Source: E. Node Compression with Variable-Flip… · pp. 8–9

IV. IMPLEMENTATION

Variable-flip maps add metadata and map operations during construction, so XBDD uses implementation optimizations to keep their costs from offsetting memory savings.

IV. IMPLEMENTATION

  • Variable-flip maps introduce extra metadata and map operations during XBDD construction.The maps are used to support additional structural sharing.Source: §IV · p. 9
  • XBDD combines compact map encoding, memory-efficient core data structures, and runtime optimizations to manage the added overhead.Source: §IV · p. 9
  • The implementation targets the trade-off between map-maintenance costs and memory savings from reducing nodes.Source: §IV · p. 9

A. Compact Variable-Flip Map Representation

XBDD stores flip maps as bitmaps and interns repeated maps in a pool. Its core structures use compact node and unique-table representations to control memory and access costs.

A. Compact Variable-Flip Map Representation

  • A flip map is a bitmap over variable identifiers, enabling symmetric difference through word-wise XOR and membership updates through bit operations.When n ≤ 64, the map fits in one machine word and major operations are effectively constant-time.Source: A. Compact Variable-Flip Map… · p. 9
  • A global map pool stores each distinct bitmap once and assigns it a 32-bit handle, which nodes and computed-cache entries store instead of the full map.Interning also reduces map equality to integer comparison, and the empty map uses handle zero.Source: A. Compact Variable-Flip Map… · p. 9

B. Memory-Efficient Core Data Structures

  • XBDD stores nodes contiguously using 32-bit NodeIds, packs the complement flag into a child identifier, and stores one map handle per node.Normalization makes the low-edge map empty; each node occupies 16 bytes, including a 16-bit reference counter and variable-level field.Source: B. Memory-Efficient Core Data Structures · p. 9
  • The level-partitioned unique table uses an independent open-addressing table per variable level, limiting rehashing and supporting locality during recursive construction.The lookup key includes child identifiers, the relative complement bit, and the relative high-edge map handle; the level is implicit in the partition.Source: B. Memory-Efficient Core Data Structures · p. 9

C. Runtime Optimizations

XBDD uses cache, recursion, and garbage-collection optimizations to limit the runtime and metadata costs of flip maps. The evaluation compares XBDD with CUDD on nine IWLS’93 circuits under a shared fixed variable order and reports four construction and representation metrics.

C. Runtime Optimizations

  • Cache and recursion optimizations target the additional work introduced by variable-flip maps during construction.XBDD uses a compact adaptive computed cache, skips caching transient subproblems, and applies adaptive garbage collection.Source: C. Runtime Optimizations · p. 10

V. EVALUATION

  • The evaluation tests whether flip maps reduce node count and memory, measures runtime costs, examines map reuse, and checks predicted exponential-to-linear compression.It compares XBDD with CUDD on nine IWLS’93 circuits: C1355, C1908, C3540, C499, C880, cm150a, comp, mux, and my_adder.Source: §V · p. 10, A. Experimental Setup · p. 10

A. Experimental Setup

  • Both packages build from the same BLIF descriptions using a fixed variable order, and each experiment averages 50 runs on the same CPU core.The four metrics are final nodes, peak nodes, total package memory, and wall time.Source: A. Experimental Setup · p. 10

B. Overall Performance

XBDD reduces space on the evaluated circuits, but the magnitude of the gain and the runtime tradeoff vary with circuit structure and scale. Map interning substantially reduces duplicate map storage, with its savings increasing as the variable count grows.

B. Overall Performance

  • Across evaluated circuits, XBDD consistently reduces space, with C1355 and C499 requiring about 7% of CUDD’s final nodes, a reduction of approximately 93%.The node-count benefit is smaller on C880, while my_adder has the same final node count in both representations.Source: B. Overall Performance · pp. 10–11, Table III · p. 11
  • Across all evaluated circuits, XBDD uses 39%–77% of CUDD’s memory, while its fixed-capacity computed cache can limit proportional savings on smaller circuits.On C1355 and C499, node count falls about 93% but memory falls only about 40%; the initial 262144 cache slots occupy about 8 MB.Source: B. Overall Performance · p. 11

C. Space–Time Tradeoff

  • All evaluated circuits use less memory with XBDD, but runtime overhead is most visible on smaller circuits and decreases as construction scale grows.XBDD is 41% slower on C1355 and 39% slower on C499; it is 13% slower on C3540 while using 26% less memory.Source: C. Space–Time Tradeoff · p. 11
  • Structural compression can offset map overhead: XBDD is 24% faster than CUDD on comp while using only 39% of its memory.On my_adder, construction times are nearly identical and XBDD uses 57% of CUDD’s memory.Source: C. Space–Time Tradeoff · p. 11

D. Map Interning Efficiency

  • Map interning eliminates 89.84%–99.95% of duplicate map instances, and dynamic hit rates range from 96.24% to 99.98%.For mux, 436,628 map references collapse to 199 distinct maps, which are stored once and referenced by 32-bit identifiers.Source: D. Map Interning Efficiency · pp. 11–12
  • For C1355 with M = 342,888 references and P = 15,024 distinct maps, interning keeps storage below 2.1 MB versus 15.7 MB uninterned at n = 384, a 7.9× reduction.Interned storage uses a 32-bit handle per reference and stores each distinct bitmap once; the storage gap widens linearly in n.Source: D. Map Interning Efficiency · p. 12, Figure 4 · p. 12
  • Map reuse converts a potentially substantial per-edge storage cost into a small shared metadata structure.The map pool retains one copy of each distinct bitmap rather than a full bitmap at every occurrence.Source: D. Map Interning Efficiency · p. 12

E. Exponential Compression Case Study

For the polarity-sensitive function family Fk, the paper compares XBDD and CUDD under a fixed variable order and finds linear versus approximately exponential node-count growth. XBDD targets local input-polarity differences within the ROBDD framework, and the conclusion identifies dynamic ordering and larger or parallel workloads as future work.

E. Exponential Compression Case Study

  • For Fk under a fixed variable order, CUDD’s node count approximately doubles as k increases, while XBDD’s grows linearly.The experiment constructs k = 14, . . . , 20; at k = 20, CUDD requires 3,145,725 nodes and XBDD requires 60.Source: E. Exponential Compression Case Study · p. 12
  • The case study confirms that per-edge variable-flip maps reduce this family’s representation from exponential to linear size.The family’s c variables determine the polarities of its x variables, which XBDD encodes in edge maps.Source: E. Exponential Compression Case Study · p. 12
  • Real circuits need not exhibit the family’s polarity structure at every level, so practical gains reflect differing degrees of the structural opportunity.The paper relates this variability to whether similar local structures occur in the circuits.Source: E. Exponential Compression Case Study · p. 12

VI. RELATED WORK

  • XBDD remains within the ROBDD framework and targets sub-functions with the same structure but differing input-variable polarities.The related-work discussion distinguishes this target from approaches exploiting other forms of redundancy and from complement edges, which encode output inversion.Source: §VI · p. 13

VII. CONCLUSION

  • Normalization and map-aware cofactor operations preserve constructive uniqueness, while bitmap encoding and map interning help keep added overhead small.The conclusion describes XBDD as enabling input-polarity variants to reuse underlying structure.Source: §VII · p. 13
  • The conclusion reports reduced node count and memory on IWLS’93 circuits with moderate runtime overhead that decreases as construction scale grows.Future work will study interaction with dynamic variable ordering and applicability to larger and parallel BDD workloads.Source: §VII · p. 13
Loading 2609.36778v2…