The Community for Technology Leaders
RSS Icon
Subscribe
Issue No.04 - April (2010 vol.59)
pp: 574-575
Ondřej Lhoták , University of Waterloo, Waterloo
Stephen Curial , Xymbiant Systems Inc., Edmonton
José Nelson Amaral , University of Alberta, Edmonton
ABSTRACT
The contribution is an optimal encoding for a set in a Reduced Ordered Binary Decision Diagram (ROBDD) when the number of elements in the set's domain is not a power of 2. The contribution includes a proof that the proposed encoding produces an ROBDD with the minimum number of nodes and discusses related open problems that are not solved by the proposed encoding.
INDEX TERMS
Binary decision diagram, binary encoding, set representation.
CITATION
Ondřej Lhoták, Stephen Curial, José Nelson Amaral, "An Optimal Encoding to Represent a Single Set in an ROBDD", IEEE Transactions on Computers, vol.59, no. 4, pp. 574-575, April 2010, doi:10.1109/TC.2009.121
REFERENCES
[1] M. Berndl, O. Lhoták, F. Qian, L. Hendren, and N. Umanee, "Points-to Analysis Using BDDs," Proc. ACM SIGPLAN '03 Conf. Programming Language Design and Implementation, pp. 103-114, 2003.
[2] R.E. Bryant, "Symbolic Boolean Manipulation with Ordered Binary-Decision Diagrams," ACM Computing Surveys, vol. 24, no. 3, pp. 293-318, 1992.
[3] S. Chang, D. Cheng, and M. Marek-Sadowska, "Minimizing ROBDD Size of Incompletely Specified Multiple Output Functions," Proc. European Design and Test Conf., pp. 620-624, 1994.
[4] O. Coudert and J.C. Madre, "A Unified Framework for the Formal Verification of Sequential Circuits," Proc. IEEE Int'l Conf. Computer-Aided Design (ICCAD '90) pp. 126-129, Nov. 1990.
[5] Y. Hong, P.A. Beerel, J.R. Burch, and K.L. McMillan, "Sibling-Substitution-Based BDD Minimization Using Don't Cares," IEEE Trans. Computer-Aided Design of Integrated Circuits and Systems, vol. 19, no. 1, pp. 44-55, Jan. 2000.
[6] O. Lhoták, S. Curial, and J.N. Amaral, "Using XBDDs and ZBDDs in Points-to Analysis," Software, Practice and Experience, vol. 39, no. 2, 163-188, Feb. 2009.
[7] O. Lhoták and L. Hendren, "Jedd: A BDD-Based Relational Extension of Java," Proc. ACM SIGPLAN '04 Conf. Programming Language Design and Implementation, pp. 158-169, 2004.
[8] K.L. McMillan, Symbolic Model Checking. Kluwer Academic Publishers, 1993.
[9] A.L. Oliveira, L.P. Carloni, T. Villa, and A. Sangiovanni-Vincentelli, "Exact Minimization of Binary Decision Diagrams Using Implicit Techniques," IEEE Trans. Computers, vol. 47, no. 11, pp. 1282-1296, Nov. 1998.
[10] C. Scholl, S. Melchior, G. Hotz, and P. Molitor, "Minimizing ROBDD Sizes of Incompletely Specified Functions by Exploiting Strong Symmetries," Proc. European Design and Test Conf., pp. 229-234, 1997.
[11] T.R. Shiple, R. Johati, A. Sangiovanni-Vincentelli, and R.K. Brayton, "Heuristic Minimization of BDDs Using Don't Cares," Proc. 31st ACM/IEEE Design Automation Conf. (DAC '94), pp. 225-231, June 1994.
[12] J. Whaley and M.S. Lam, "Cloning-Based Context-Sensitive Pointer Alias Analysis Using Binary Decision Diagrams," Proc. ACM SIGPLAN '04 Conf. Programming Language Design and Implementation (PLDI '04), pp. 131-144, 2004.
[13] J. Zhu, "Symbolic Pointer Analysis," Proc. 2002 IEEE/ACM Int'l Conf. Computer-Aided Design, pp. 150-157, 2002.
[14] J. Zhu and S. Calman, "Symbolic Pointer Analysis Revisited," Proc. ACM SIGPLAN '04 Conf. Programming Language Design and Implementation (PLDI '04), pp. 145-157, 2004.
22 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool