論文

査読有り
2002年5月

Streaming BDD manipulation

IEEE TRANSACTIONS ON COMPUTERS
  • S Minato

51
5
開始ページ
474
終了ページ
485
記述言語
英語
掲載種別
研究論文(学術雑誌)
DOI
10.1109/TC.2002.1004587
出版者・発行元
IEEE COMPUTER SOC

Binary Decision Diagrams (BDDs) are now commonly used for handling Boolean functions because of their excellent efficiency in terms of time and space. However, the conventional BDD manipulation algorithm is strongly based on the hash table technique, so it always encounters the memory overflow problem when handling large-scale BDD data. This paper proposes a new streaming BDD manipulation method that never causes memory overflow or swap out. This method allows us to handle very large-scale BDD stream data beyond the memory limitation. Our method can be characterized as follows: 1) it gives a continuous tradeoff curve between memory usage and stream data length, 2) valid solutions for a partial Boolean space can be obtained if we break the process before finishing, and 3) easily accelerated by pipelined multiprocessing, An experimental result demonstrates that we can succeed in finding a number of solutions to a SAT problem using commodity PC with a 64 MB memory, where as the conventional BDD manipulator would have required a 100GB memory, BDD manipulation has been considered as an intensively memory-consuming procedure, but now we can also utilize the hard disk and network resources as well, The method leads to a new approach to BDD manipulation.

リンク情報
DOI
https://doi.org/10.1109/TC.2002.1004587
CiNii Articles
http://ci.nii.ac.jp/naid/120000959511
Web of Science
https://gateway.webofknowledge.com/gateway/Gateway.cgi?GWVersion=2&SrcAuth=JSTA_CEL&SrcApp=J_Gate_JST&DestLinkType=FullRecord&KeyUT=WOS:000175244500003&DestApp=WOS_CPL
ID情報
  • DOI : 10.1109/TC.2002.1004587
  • ISSN : 0018-9340
  • eISSN : 1557-9956
  • CiNii Articles ID : 120000959511
  • Web of Science ID : WOS:000175244500003

エクスポート
BibTeX RIS