Graph-based algorithms for boolean function manipulation, IEEE Trans. Comput, vol.35, pp.677-691, 1986. ,

Efficient boolean function matching, Proceedings of the 1992 IEEE/ACM International Conference on Computer-aided Design, ICCAD '92, pp.408-411, 1992. ,

Shared binary decision diagram with attributed edges for efficient boolean function manipulation, 27th ACM/IEEE Design Automation Conference, pp.52-57, 1990. ,

Dual edge operations in reduced ordered binary decision diagrams, Circuits and Systems, 1998. ISCAS '98. Proceedings of the 1998 IEEE International Symposium on, vol.6, pp.159-162, 1998. ,

A unifying theoretical background for some bdd-based data structures, Form. Methods Syst. Des, vol.11, pp.223-237, 1997. ,

New generalizations of shannon decomposition, 2001. ,

Improving the variable ordering of OBDDs is NP-complete, IEEE Transactions on Computers, vol.45, pp.993-1002, 1996. ,

The Coq proof assistant reference manual. LogiCal Project, 2004. ,

Zero-suppressed bdds for set manipulation in combinatorial problems, Proceedings of the 30th International Design Automation Conference, DAC '93, pp.272-277, 1993. ,

An introduction to zero-suppressed binary decision diagrams, tech. rep., in 'Proceedings of the 12th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning, 2001. ,

Efficient implementation of a BDD package, Proceedings of the 27th ACM/IEEE Design Automation Conference, DAC '90, pp.40-45, 1990. ,

Binary decision diagrams, 1999. ,

Chain reduction for binary and zero-suppressed decision diagrams, CoRR, 2017. ,

Binary Decision Diagrams with Edge-Specified Reductions, Tools and Algorithms for the Construction and Analysis of Systems, pp.303-318, 2019. ,

Tagged bdds: Combining reduction rules from different decision diagram types, FMCAD, pp.108-115, 2017. ,

Multilevel logic synthesis based on functional decision diagrams, Proceedings The European Conference on Design Automation, pp.43-47, 1992. ,

How many decomposition types do we need?, 1995. ,

On decomposing boolean functions via extended cofactoring, Proceedings of the Conference on Design, Automation and Test in Europe, DATE '09, pp.1464-1469, 2009. ,

Biconditional bdd: A novel canonical bdd for logic synthesis targeting xor-rich circuits, 2013 Design, Automation Test in Europe Conference Exhibition (DATE), pp.1014-1017, 2013. ,

Boolean function representation based on disjoint-support decompositions, Proceedings International Conference on Computer Design. VLSI in Computers and Processors, pp.27-32, 1996. ,

Achieving Scalable Hardware Verification with Symbolic Simulation, 2003. ,

A Knowledge Compilation Map, vol.17, pp.229-264, 2002. ,

, Shows the representation of solutions of the CNF satlib/uf20-91/uf20-01.cnf using four different models ?DD-O-NU 5a (aka. ROBDD+N), ?DD-O-C 10 5b (aka. ZDD), ?DD-O-UC 0 5c (aka. ESRBDD) and our latest model ?DD-U-NUC 5d, Figure, vol.5