Abstract
We investigate a new class of metrics to find good variable orders for decision diagrams in symbolic state-space generation. Most of the previous work on static ordering is centered around the concept of minimum variable span, which can also be found in the literature under several other names. We use a similar concept, but applied to event span, and generalize it to a family of metrics parameterized by a moment, where the metric of moment 0 is the combined event span. Finding a good variable order is then reduced to optimizing one of these metrics, and we design extensive experiments to evaluate them. First, we investigate how the actual optimal order performs in state-space generation, when it can be computed by evaluating all possible permutations. Then, we study the performance of these metrics on selected models and compare their impact on two different state-space generation algorithms: classic breadth-first and our own saturation strategy. We conclude that the new metric of moment 1 is the best choice. In particular, the saturation algorithm seems to benefit the most from using it, as it achieves the better performance in nearly 80% of the cases.
Work supported in part by the National Aeronautics and Space Administration under grant NCC1-02043 and by the National Science Foundation under grants CNS-0501747 and CNS-0501748.
Chapter PDF
Similar content being viewed by others
Keywords
- Genetic Algorithm
- Variable Order
- Binary Decision Diagram
- Symbolic Model Check
- Order Binary Decision Diagram
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Aziz, A., Tasiran, S., Brayton, R.K.: BDD Variable Ordering for Interacting Finite State Machines. In: 31st ACM/IEEE Design Automation Conference (DAC), San Diego, CA, June 1994, ch. 18.3, San Diego Convention Center (1994)
Aloul, F.A., Markov, I.L., Sakallah, K.A.: MINCE: A static global variableordering heuristic for SAT search and BDD manipulation. J. UCS 10(12), 1562–1596 (2004)
Borrione, D., Vidal, J.: Improving static ordering of BDDs for reachability analysis, April 29 (2002)
Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Trans. Comput. 35(8), 677–691 (1986)
Bryant, R.E.: Symbolic boolean manipulation with ordered binary-decision diagrams. ACM Comp. Surv. 24(3), 293–318 (1992)
Burch, J.R., Clarke, E.M., Long, D.E.: Symbolic model checking with partitioned transistion relations. In: VLSI, pp. 49–58 (1991)
Chauhan, P., Clarke, E., Jha, S., Kukula, J., Veith, H., Wang, D.: Using combinatorial optimization methods for quantification scheduling. In: Margaria, T., Melham, T.F. (eds.) CHARME 2001. LNCS, vol. 2144, pp. 293–302. Springer, Heidelberg (2001)
Ciardo, G., Jones, R.L., Miner, A.S., Siminiceanu, R.I.: Logical and stochastic modeling with smart. In: Kemper, P., Sanders, W.H. (eds.) TOOLS 2003. LNCS, vol. 2794, pp. 78–97. Springer, Heidelberg (2003)
Ciardo, G., Lüttgen, G., Siminiceanu, R.I.: Efficient symbolic state-space construction for asynchronous systems. In: Nielsen, M., Simpson, D. (eds.) ICATPN 2000. LNCS, vol. 1825, pp. 103–122. Springer, Heidelberg (2000)
Ciardo, G., Lüttgen, G., Siminiceanu, R.I.: Saturation: An efficient iteration strategy for symbolic state-space generation. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 328–342. Springer, Heidelberg (2001)
Ciardo, G., Marmorstein, R., Siminiceanu, R.: Saturation unbound. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 379–393. Springer, Heidelberg (2003)
Ciardo, G., Yu, A.J.: Saturation-based symbolic reachability analysis using conjunctive and disjunctive partitioning. In: Borrione, D., Paul, W. (eds.) CHARME 2005. LNCS, vol. 3725, pp. 146–161. Springer, Heidelberg (2005)
Geist, D., Beer, I.: Efficient model checking by automated ordering of transition relation. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol. 818, pp. 299–310. Springer, Heidelberg (1994)
Drechsler, R., Becker, B., Gockel, N.: A genetic algorithm for variable ordering of OBDDs. In: Int’l Workshop on Logic Synthesis, May 1995, ACM/IEEE (1995)
Fujita, M., Fujisawa, H., Matsunaga, Y.: Variable ordering algorithms for ordered binary decision diagrams and their evaluation. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 12(1), 6–12 (1993)
Garey, M.R., Johnson, D.S.: Computers and Intractability: A Guide to the Theory of NP-Completeness. Freeman Press, New York (1979)
Grumberg, O., Livne, S., Markovitch, S.: Learning to order BDD variables in verification. Journal of Artificial Intelligence Research 18, 83–116 (2003)
Hung, W.N.N., Song, X.: BDD variable ordering by scatter search. In: ICCD, pp. 368–373 (2001)
Kam, T., Villa, T., Brayton, R., Sangiovanni-Vincentelli, A.: Multi-valued decision diagrams: theory and applications. Multiple-Valued Logic 4(1–2), 9–62 (1998)
Lu, Y., Jain, J., Clarke, E.M., Fujita, M.: Efficient variable ordering using a BDD based sampling. In: Design Automation Conference, pp. 687–692 (2000)
Michalewicz, Z.: Genetic Algorithms + Data Structures = Evolution Programs. Springer, New York (1996)
Moon, I.-H., Kukula, J.H., Ravi, K., Somenzi, F.: To split or to conjoin: the question in image computation. In: Proceedings of the 37th Conference on Design Automation (DAC 2000), June 5–9, pp. 23–28. ACM/IEEE (2000)
Moreira, A.M., Déharbe, D., Costa, U.S.: Advances in BDD reduction using parallel genetic algorithms (May 2001)
Rudell, R.: Dynamic Variable Ordering for Ordered Binary Decision Diagrams. In: IEEE /ACM International Conference on CAD, Santa Clara, California, November 1993, pp. 42–47. ACM/IEEE, IEEE Computer Society Press (1993)
Ranjan, R., Aziz, A., Brayton, R., Plessier, B., Pixley, C.: Efficient BDD algorithms for FSM synthesis and verification (May 1995)
Wu, Y., Robert, J.: Personal communication (October 2005)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Siminiceanu, R.I., Ciardo, G. (2006). New Metrics for Static Variable Ordering in Decision Diagrams. In: Hermanns, H., Palsberg, J. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2006. Lecture Notes in Computer Science, vol 3920. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11691372_6
Download citation
DOI: https://doi.org/10.1007/11691372_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-33056-1
Online ISBN: 978-3-540-33057-8
eBook Packages: Computer ScienceComputer Science (R0)