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

J. R. Burch and D. E. Long, Efficient boolean function matching, Proceedings of the 1992 IEEE/ACM International Conference on Computer-aided Design, ICCAD '92, pp.408-411, 1992.

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

D. M. Miller and R. Drechsler, 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.

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

P. Kerntopf, New generalizations of shannon decomposition, 2001.

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

T. C. Development-team, The Coq proof assistant reference manual. LogiCal Project, 2004.

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

A. Mishchenko, 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.

K. S. Brace, R. L. Rudell, and R. E. Bryant, Efficient implementation of a BDD package, Proceedings of the 27th ACM/IEEE Design Automation Conference, DAC '90, pp.40-45, 1990.

F. Somenzi, Binary decision diagrams, 1999.

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

J. Babar, C. Jiang, G. Ciardo, and A. Miner, Binary Decision Diagrams with Edge-Specified Reductions, Tools and Algorithms for the Construction and Analysis of Systems, pp.303-318, 2019.

T. Van-dijk, R. Wille, and R. Meolic, Tagged bdds: Combining reduction rules from different decision diagram types, FMCAD, pp.108-115, 2017.

U. Kebschull, E. Schubert, and W. Rosenstiel, Multilevel logic synthesis based on functional decision diagrams, Proceedings The European Conference on Design Automation, pp.43-47, 1992.

B. Becker and R. Drechsler, How many decomposition types do we need?, 1995.

A. Bernasconi, V. Ciriani, G. Trucco, and T. Villa, On decomposing boolean functions via extended cofactoring, Proceedings of the Conference on Design, Automation and Test in Europe, DATE '09, pp.1464-1469, 2009.

L. Amarú, P. Gaillardon, and G. D. Micheli, 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.

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

V. M. Bertacco, Achieving Scalable Hardware Verification with Symbolic Simulation, 2003.

A. Darwiche and P. Marquis, 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