Some disturbing facts about depth-first left-most variable ordering heuristics for binary decision diagrams

Abstract

Binary decision diagrams (BDDs) have proven to be a very efficient tool to assess fault trees. However, the size of the BDD, and therefore the efficiency of the whole methodology, is highly dependent on the choice of variable ordering. The determination of the best variable ordering is intractable. Therefore, heuristics have been designed to select reasonably good variable orderings. The most popular of these heuristics consists in numbering variables by means of a depth-first left-most (DFLM) traversal of the formula, after possibly some rearrangements of the inputs of the gates. In this article, this heuristic is studied in a systematic way. It is shown to be very sensitive to the way the formula is written. A series of experiments shows also that the notion of locality of variables, which was believed to be a key issue in the determination of good orderings, must be handled with care. These facts are quite disturbing and raise questions about the design of good variable ordering heuristics.

Keywords

fault trees binary decision diagrams variable ordering heuristics

Get full access to this article

View all access options for this article.

References

Bryant

Graph based algorithms for Boolean function manipulation. IEEE Trans. Comput., 1986, 35(8), 677–691

Brace

Rudell

Bryant

Efficient implementation of a BDD package. In Proceedings of the 27th ACM/IEEE Design automation conference, Orland, FL, USA, June 1990, pp. 40–45, (IEEE, Piscataway, NJ)

Coudert

Madre

J.-C.

Fault tree analysis: 10²⁰ prime implicants and Beyond. The Annual reliability and maintainability symposium, ARMS'93, January 1993. Atlanta NC, USA

Rauzy

New algorithms for fault trees analysis. Reliab. Engng Sys., Saf, 1993, 59(2), 203–211

Bryant

Symbolic boolean manipulation with ordered binary decision diagrams. ACM Comput. Surv., 1992, 24, 293–218

Friedman

S. J.

Supowit

K. J.

Finding the optimal variable ordering for binary decision diagrams. IEEE Trans. Comput., 1990, 39(5), 710–713

Bollig

Wegener

Improving the variable ordering of OBDDs is NP-complete. IEEE Trans. Softw. Engng., 1996, 45(9), 993–1001

Aloul

F. A.

Markov

I. L.

Sakallah

K. A.

FORCE: a fast and easy-to-implement variable-ordering heuristic. In Proceedings of Great Lakes Symposium on VLSI, Washington DC, 2003, pp. 116–119

Fujita

Fujisawa

Kawato

Evaluation and improvements of Boolean comparison method based on binary decision diagrams. In Proceedings of IEEE International Conference on Computer aided design, ICCAD'88, Santa Clara, CA, USA, November 1988, pp. 2–5 (IEEE)

10.

Rudell

Dynamic variable ordering for ordered binary decision diagrams. In Proceedings of IEEE International Conference on Computer aided design, ICCAD'93, Santa Clara, CA, USA, November 1993, pp. 42–47 (IEEE)

11.

Panda

Somenzi

Who are the variables in your neighborhood. In Proceedings of IEEE International Conference on Computer aided design, ICCAD'95, San Jose, CA, USA, November 1995, pp. 74–77 (IEEE)

12.

Nikolskaia

Rauzy

Fine-tuning of Boolean formulae preprocessing techniques. In Proceedings of the European safety and reliability association conference, ESREL'99, volume 2, Garching, September 1999, pp. 1027–1032 (A. A. Balkema)

13.

Ibañez Llano

Meléndez Asensio

Nieto Fuentes

Variable ordering schemes to apply to the binary decision diagram methodology for event tree sequences assessment. In Proceedings of. ESREL'06, Estoril, Portugal, October 2006, pp. 1645–1652 (Taylor and Francis Group)

14.

Bouissou

Bruyère

Rauzy

BDD based fault-tree processing: a comparison of variable ordering heuristics. In Proceedings of the ESREL'97, volume 3, Lisbon, Portugal, June 1997, pp. 2045–2052 (Pergamon)

15.

Minato

Ishiura

Yajima

Shared binary decision diagrams with attributed edges for efficient Boolean function manipulation. In L. J. M Claesen, (Ed.), Proceedings of the 27th ACM/IEEE Design automation conference, DAC'90, Orlando, FL, USA, June 1990, pp. 52–57 (ACM).

16.

Aloul

Markov

Sakallah

Improving the efficiency of circuit-to-BDD conversion by gate and input ordering. In Proceedings of the International Conference on Computer design (ICCD), Freiburg, Germany, September 2002, pp. 64–69 (IEEE)

17.

Aloul

Markov

Sakallah

MINCE: A static global variable-ordering heuristic for SAT search and BDD manipulation. J. Univers. Comput. Sci., 2004, 10(12), 1562–1596

18.

Reay

K. A.

Andrews

J. D.

A fault tree analysis strategy using binary decision diagrams. Reliab. Engng Syst. Saf., 2002, 78(1), 45–56

19.

Epstein

Rauzy

Can we trust PRA?

Reliab. Engng and Syst. Saf., 2005, 88(3), 195–205

20.

Fujita

Fujisawa

Matsugana

Variable ordering algorithm for ordered binary decision diagrams and their evaluation. IEEE Trans. Comput.-Aided Des., Integr. Circuits Syst., 1993, 12(1), 6–12

21.

Garey

M. R.

Johnson

D. S.

Computers and intractability: a guide to the theory of NP-completeness, 1979, (Freeman, San Fransisco, CA)

22.

Horton

S. B.

Optimal linear arrangement problem: algorithms and approximation. Thesis, Georgia Institute of Technology, Atlanta, Georgia, USA, May 1997