ETAPS 2019
Sat 6 - Thu 11 April 2019 Prague, Czech Republic
Wed 10 Apr 2019 17:00 - 17:30 at SUN I - Symbolic Verification Chair(s): Holger Hermanns

Various versions of binary decision diagrams (BDDs) have been proposed in the past, differing in the reduction rule needed to interpret the meaning of edges skipping levels. The most widely adopted, fully-reduced BDDs and zero-suppressed BDDs, excel at encoding different types of boolean functions (the former when the function has many “don’t-care”, the latter when it tends to have value zero when one of its arguments is nonzero). Recently, new classes of BDDs have been proposed that, at the cost of some additional complexity and larger memory requirements per node, attempt to exploit both cases. We introduce a new type of BDD that we believe is conceptually simpler, yet has small memory requirements in terms of node size, tends to result in fewer nodes, and can easily be extended to include further reduction rules. We present a formal definition, prove canonicity, and provide experimental results to support our efficiency claims.