Lex-Partitioning: A New Option for BDD Search

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 a...

Full description

Bibliographic Details
Main Authors: Stefan Edelkamp, Peter Kissmann, Álvaro Torralba
Format: Article
Language:English
Published: Open Publishing Association 2012-10-01
Series:Electronic Proceedings in Theoretical Computer Science
Online Access:http://arxiv.org/pdf/1210.6415v1
id doaj-ba59a66bc672440f871a3c09fbe50dbf
record_format Article
spelling doaj-ba59a66bc672440f871a3c09fbe50dbf2020-11-24T23:42:25ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802012-10-0199Proc. GRAPHITE 2012668210.4204/EPTCS.99.8Lex-Partitioning: A New Option for BDD SearchStefan EdelkampPeter KissmannÁlvaro TorralbaFor 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.http://arxiv.org/pdf/1210.6415v1
collection DOAJ
language English
format Article
sources DOAJ
author Stefan Edelkamp
Peter Kissmann
Álvaro Torralba
spellingShingle Stefan Edelkamp
Peter Kissmann
Álvaro Torralba
Lex-Partitioning: A New Option for BDD Search
Electronic Proceedings in Theoretical Computer Science
author_facet Stefan Edelkamp
Peter Kissmann
Álvaro Torralba
author_sort Stefan Edelkamp
title Lex-Partitioning: A New Option for BDD Search
title_short Lex-Partitioning: A New Option for BDD Search
title_full Lex-Partitioning: A New Option for BDD Search
title_fullStr Lex-Partitioning: A New Option for BDD Search
title_full_unstemmed Lex-Partitioning: A New Option for BDD Search
title_sort lex-partitioning: a new option for bdd search
publisher Open Publishing Association
series Electronic Proceedings in Theoretical Computer Science
issn 2075-2180
publishDate 2012-10-01
description 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.
url http://arxiv.org/pdf/1210.6415v1
work_keys_str_mv AT stefanedelkamp lexpartitioninganewoptionforbddsearch
AT peterkissmann lexpartitioninganewoptionforbddsearch
AT alvarotorralba lexpartitioninganewoptionforbddsearch
_version_ 1725504530355847168