Abstract: Binary decision diagrams (BDDs) are directed acyclic graphs used to represent functions over boolean variables. They have enjoyed widespread success in a number of domains, including hardware verification, model checking, and combinatorial problems. This talk presents RexBDDs, a form of BDDs that can exploit reduction opportunities beyond reduced ordered BDDs and zero suppressed BDDs, and can incorporate both input complement (swap) and output complement flags on edges. With appropriate restrictions, RexBDDs are a canonical representation and can be manipulated using appropriately-modified versions of BDD "Apply" algorithms. We show, both theoretically and experimentally, that RexBDDs compare favorably against other BDD variants.

Bio:  Andrew Miner is an Associate Professor of Computer Science at Iowa State University. Much of his research involves developing new variants of BDDs, along with improved algorithms, for model checking and probabilistic model checking of Petri nets and other high-level formalisms. He develops and maintains the open-source software projects SMART (Stochastic Model-checking Analyzer for Reliability and Timing) and MEDDLY (Multi-terminal and Edge-valued Decision Diagram LibrarY).  https://www.cs.iastate.edu/~asminer