Abstract
A central issue in the solution of many computer aided design problems is to find concise representations for circuit designs and their functional specification. Recently, a restricted type of branching programs (OB-DDs) proved to be extremely useful for representing Boolean functions for various CAD applications [Bry92]. Unfortunatelly, many circuits of practical interest provably require OBDD-representations of exponential size. In the following we systematically study the question up to what extend more concise BP-representations can be successfully used in symbolic Boolean manipulation, too. We prove, in very general settings,
-
The frontier of efficient (deterministic) symbolic Boolean manipulation on the basis of BP-representatious are read-once-only branching programs (BP1).
-
The frontier of efficient probabilistic manipulation with BP-based data structures are parity read-once-only branching programs (⊕-BP1).
Since BP1s and ⊕-BP1s are generally more (sometimes even exponentially more) succinct than OBDD-representations our results make accessible more succinct types of BPs as data structures for practical purposes. (A BP1-package as well as a ⊕-BP1-package are in preparation.) On the other side, our results together with the results obtained in [GM92] show that the solution of basic tasks in Boolean manipulation for less restricted BP-types becomes NP-hard.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
M. Ajtai, L. Babai, P. Hajnal, J. Komlos, P. Pudlak, V. Rödl, E. Szemeredi, G. Turan: Two Lower Bounds for Branching Programs, Proc. 18. ACM STOC, 1986, 30–38.
K. S. Brace, R. E. Bryant, R. L. Rudell: Efficient Implementation of a BDD package. Proc. of 27th Design Automation Conf., 1990, 40–45.
M. Blum, A. K. Chandra, M. N. Wegman: Equivalence of Free Boolean Graphs Can Be Decided Probabilistically in Polynomial Time, IPL 10, 2, 1980, 80–82.
Y. Breitbart, H. B. Hunt III, D. Rosenkrantz: The Size of Binary Decision Diagrams Representing Boolean Functions, submitted to Inf. and Comp. 1991.
R. E. Bryant: Graph-Based Algorithms for Boolean Function Manipulation, IEEE Trans. Computers, C-35, 8, 1986, 677–691.
R. E. Bryant: Symbolic Boolean Manipulation with Ordered Binary Decision Diagrams, to appear in IEEE Trans. Computers, 1992.
J. R. Burch, E. M. Clarke, K. L. McMillan, D.L. Dill: Sequential Circuit Verification Using Symbolic Model Checking, Proc. 27th IEEE DAC'90, 1990, 46–51.
R. L. Constable, H. B. Hunt III, S. Salmi: On the Computational Complexity of Scheme Equivalence, Proc. 8th Princeton Conf. on Information Sciences and Systems, 1974.
S. Fortune, J. Hopcroft, E. M. Schmidt: The Complexity of Equivalence and Containment for Free Single Program Schemes. LNCS 62, 1978, 227–240.
M. Fuita, H. Fujisawa, N. Kawoto: Evaluation and Improvements of Boolean Comparison Method Based on Binary Decision Diagrams, Proc. IEEE ICCAD'88, 1988, 2–5.
J. Gergov, Ch. Meinel: Analysis and Manipulation of Boolean Functions in Terms of Decision Graphs, Proc. WG'92, LNCS, 1992.
J. Gergov, Ch. Meinel: Efficient Analysis and Manipulation of OBDDs Can Be Extended to Read-once-only Branching Programs, Forschungsbericht Nr. 92-10, Univ. Trier, 1992.
R. Lidl, H. Niederreiter: Introduction to Finite Fields and Their Applications. Cambridge University Press, 1986.
M. Krause, Ch. Meinel, S. Waack: Separating the Eraser Turing Machine Classes L e , N Le, co-N Le and P e , TCS 86 (1991), 267–275.
Ch. Meinel: The Power of Polynomial Size Ω-Branching Programs, Proc. STACS'88 (Bourdeaux), LNCS 294, 81–90.
Ch. Meinel: Modified Branching Programs and Their Computational Power, Springer-Verlag, LNCS 370, 1989.
Ch. Meinel: Branching Programs-An Efficient Data Structure for Computer-Aided Circuit Design, Preprint UGH Paderborn, Nr. 93, 1991.
S. Muroga, Y. Kambayashi, H. C. Lai, J. N. Culliney: The Transduction Method, IEEE Trans. Computers, C-38, 1989, 1404–1424.
S. Malik, A. Wang, It. Bryant, A. Sangiovanni-Vincentelli: Logical Verification Using Binary Decision Diagrams in a Logical Synthesis Environment. Proc. IEEE Intern. Conf. on CAD, 1988, 6–9.
D. Sieling, I. Wegener: Graph Driven BDDs — A New Data Structure for Boolean Functions, personal communications, manuscript.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1993 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Gergov, J., Meinel, C. (1993). Frontiers of feasible and probabilistic feasible Boolean manipulation with branching programs. In: Enjalbert, P., Finkel, A., Wagner, K.W. (eds) STACS 93. STACS 1993. Lecture Notes in Computer Science, vol 665. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-56503-5_57
Download citation
DOI: https://doi.org/10.1007/3-540-56503-5_57
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-56503-1
Online ISBN: 978-3-540-47574-3
eBook Packages: Springer Book Archive