Abstract
We investigate the complexity of problems on Ordered Functional Decision Diagrams (OFDDs) related to satisfiability, i.e. SAT-ONE, SAT-ALL, and SAT-COUNT. We prove that SAT-ALL has a running time linear in the product of the number of satisfying assignments and the size of the given OFDD. Counting the satisfying assignments in an OFDD is proved to be #P-complete, and thus not possible in polynomial time unless P=NP.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
B. Becker, R. Drechsler, and M. Theobald, “On the implementation of a package for efficient representation and manipulation of functional decision diagrams,” IFIP WG 10.5 Workshop on Applications of the Reed-Muller Expansion in Circuit Design, pp. 162-169, Sept. 1993.
B. Becker, R. Drechsler, and R. Werchner, “On the relation between BDDs and FDDs,” LATIN, LNCS 911, pp. 72-83, Apr. 1995.
R.E. Bryant, “Graph — based algorithms for Boolean function manipulation,” IEEE Trans. Comput., vol. C-35, pp. 677-691, Aug. 1986.
R. Drechsler and B. Becker, “Sympathy: Fast exact minimization of Fixed Polarity Reed-Muller expressions for symmetric functions,” Proc. European Design & Test Conf., pp. 91-97, Mar. 1995.
R. Drechsler, A. Sarabi, M. Theobald, B. Becker, and M.A. Perkowski, “Efficient representation and manipulation of switching functions based on Ordered Kro-necker Functional Decision Diagrams,” Proc. Design Automation Conf., pp. 415-419, June 1994.
R. Drechsler, M. Theobald, and B. Becker, “Fast OFDD based minimization of Fixed Polarity Reed-Muller expressions,” to be published in IEEE Trans. Comput., 1996.
U. Kebschull and W. Rosenstiel, “Efficient graph-based computation and manipulation of functional decision diagrams,” Proc. European Conf. on Design Automation, pp. 278-282, Mar. 1993.
U. Kebschull, E. Schubert, and W. Rosenstiel, “Multilevel logic synthesis based on functional decision diagrams,” Proc. European Conf. on Design Automation, pp. 43-47, Mar. 1992.
J. Van Leeuven, editor, Handbook of Theoretical Computer Science, Algorithms and Complexity. The MIT Press, 1990.
C. Meinel, “Modified Branching Programs and their Computational Power,” LNCS 370, Apr. 1989.
E. Schubert, U. Kebschull, and W. Rosenstiel, “FDD based technology mapping for FPGA,” In Proc. EUROASIC, pp. 14-18, Mar. 1992.
D. Sieling and I. Wegener, “Reduction of BDDs in linear time,” Information Processing Letters, 48(3):139-144, 1993.
C.C. Tsai and M. Marek-Sadowska, “Boolean matching using generalized Reed-Muller forms,” Proc. Design Automation Conf., pp. 339-344, June 1994.
C.C. Tsai and M. Marek-Sadowska, “Detecting symmetric variables in Boolean functions using generalized Reed-Muller forms,” In Int’l Symp. Circ. and Systems, 1994.
I. Wegener, The Complexity of Boolean Functions. John Wiley & Sons Ltd., and B.G. Teubner, Stuttgart, 1987.
I. Wegener, “Efficient data structures for Boolean functions,” Discrete Mathematics, 136:347-372, Dec. 1994.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1996 Kluwer Academic Publishers
About this chapter
Cite this chapter
Werchner, R., Harich, T., Drechsler, R., Becker, B. (1996). Satisfiability Problems for OFDDs. In: Sasao, T., Fujita, M. (eds) Representations of Discrete Functions. Springer, Boston, MA. https://doi.org/10.1007/978-1-4613-1385-4_10
Download citation
DOI: https://doi.org/10.1007/978-1-4613-1385-4_10
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4612-8599-1
Online ISBN: 978-1-4613-1385-4
eBook Packages: Springer Book Archive