Lex-Partitioning: A New Option for BDD Search

Stefan Edelkamp
Peter Kissmann
Álvaro Torralba

For the exploration of large state spaces, symbolic search using binary decision diagrams (BDDs) can save huge amounts of memory and computation time. State sets are represented and modified by accessing and manipulating their characteristic functions. BDD partitioning is used to compute the image as the disjunction of smaller subimages.

In this paper, we propose a novel BDD partitioning option. The partitioning is lexicographical in the binary representation of the states contained in the set that is represented by a BDD and uniform with respect to the number of states represented. The motivation of controlling the state set sizes in the partitioning is to eventually bridge the gap between explicit and symbolic search.

Let n be the size of the binary state vector. We propose an O(n) ranking and unranking scheme that supports negated edges and operates on top of precomputed satcount values. For the uniform split of a BDD, we then use unranking to provide paths along which we partition the BDDs. In a shared BDD representation the efforts are O(n). The algorithms are fully integrated in the CUDD library and evaluated in strongly solving general game playing benchmarks.

In Anton Wijs, Dragan Bošnački and Stefan Edelkamp: Proceedings First Workshop on GRAPH Inspection and Traversal Engineering (GRAPHITE 2012), Tallinn, Estonia, 1st April 2012, Electronic Proceedings in Theoretical Computer Science 99, pp. 66–82.
Published: 23rd October 2012.

ArXived at: https://dx.doi.org/10.4204/EPTCS.99.8 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org