Abstract
We allow equations in binary decision diagrams (BDD). The resulting objects are called EQ-BDDs. A straightforward notion of reduced ordered EQ-BDDs (EQ-OBDD) is defined, and it is proved that each EQ-BDD is logically equivalent to an EQ-OBDD. Moreover, on EQOBDDs satisfiability and tautology checking can be done in constant time. Several procedures to eliminate equality from BDDs have been reported in the literature. Typical for our approach is that we keep equalities, and as a consequence do not employ the finite domain property. Furthermore, our setting does not strictly require Ackermann's elimination of function symbols. This makes our setting much more amenable to combinations with other techniques in the realm of automatic theorem proving, such as term rewriting. We introduce an algorithm, which for any propositional formula with equations finds an EQ-OBDD that is equivalent to it. The algorithm has been implemented, and applied to benchmarks known from literature. The performance of a prototype implementation is comparable to existing proposals.
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
W. Ackermann. Solvable Cases of the Decision Problem. Studies in Logic and the Foundations of Mathematics. North-Holland, Amsterdam, 1954. 162, 163, 175
H. R. Andersen and H. Hulgaard. Boolean expression diagrams. In Twelfth Annual IEEE Symposium on Logic in Computer Science, pages 88–98, Warsaw, Poland, 1997. IEEE Computer Society. 164, 176
F. Baader and T. Nipkow. Term Rewriting and All That. Cambridge University Press, 1998. 166
M.G.J. van den Brand, H.A. de Jong, P. Klint, and P.A. Olivier. Efficient Annotated Terms. Software-Practice &amt; Experience, 30:259–291, 2000. See also http://www.cwi.nl/projects/MetaEnv/aterm/. 163, 175
R.E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, C-35(8):677–691, 1986. 161, 163
R.E. Bryant. Symbolic boolean manipulation with ordered binary-decision diagrams. ACM Computing Surveys, 24(3):293–318, 1992. 161, 165
R.E. Bryant, S. German, and M.N. Velev. Exploiting positive equality in a logic of equality with uninterpreted functions. In N. Halbwachs and D Peled, editors, Proc. of Computer Aided Verification, CAV’99, LNCS 1633. Springer-Verlag, 1999. 161, 162, 163, 163, 164, 174
Burch, J.R. and D.L. Dill. Automatic verification of pipelined microprocessors control. In D. L. Dill, editor, Proceedings of Computer Aided Verification, CAV’94, LNCS 818, pages 68–80. Springer-Verlag, June 1994. 162, 163, 164
N. Dershowitz. Termination of rewriting. Journal of Symbolic Computation, 3(1-2):69–115, 1987. 166
A. Goel, K. Sajid, H. Zhou, and A. Aziz. BDD based procedures for a theory of equality with uninterpreted functions. In Proceedings of Computer Aided Verification, CAV’98, LNCS 1427, pages 244–255. Springer-Verlag, 1998. 161, 164, 164, 164, 174
J.W. Klop. Term rewriting systems. In D. Gabbay S. Abramski and T. Maibaum, editors, Handbook of Logic in Computer Science, volume 1. Oxford University Press, 1991. 166
C. Meinel and T. Theobald. Algorithms and Data Structures in VLSI Design: OBDD-Foundations and Applications. Springer-Verlag, 1998. 161, 163, 165, 170
J. Møller, J. Lichtenberg, H. R. Andersen, and H. Hulgaard. Difference decision diagrams. In J. Flum and M. Rodriguez-Artalejo, editors, Computer Science Logic (CSL’99), LNCS 1683. Springer-Verlag, 1999. 161, 164, 164, 164, 177
G. Nelson and D.C. Oppen. Fast decision procedures based on congruence closure. Journal of the Association for Computing Machinery, 27(2):356–364, 1980. 163
S. Owre, S. Rajan, J.M. Rushby, N. Shankar, and M.K. Srivas. PVS: Combining specification, proof checking, and model checking. In R. Alur and T.A. Henzinger, editors, Proceedings of Computer Aided Verification CAV’96, LNCS 1102, pages 411–414. Springer-Verlag, 1996. 163
A. Pnueli, Y. Rodeh, O. Shtrichman, and M. Siegel. Deciding equality formulas by small domains instantiations. In N. Halbwachs and D Peled, editors, Proceedings of Computer Aided Verification, CAV’99, LNCS 1633. Springer-Verlag, 1999. 161, 162, 163, 163, 163, 163, 174, 175, 175, 176, 176, 176
J.C. van de Pol and H. Zantema. Binary decision diagrams by shared rewriting. In M. Nielsen and B. Rovan, editors, Proceedings of Mathematical Foundations of Computer Science, MFCS’00, LNCS 1893. Springer-Verlag, 2000. 164
R.E. Shostak. An algorithm for reasoning about equality. Communications of the ACM, 21(7):583–585, 1978. 163, 165
O. Shtrichman. Benchmarks for satisfiability checking of equality formulas. See http://www.wisdom.weizmann.ac.il/õfers/sat/bench.htm, 1999. 163, 174, 175, 175, 175, 176, 176, 176
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Friso Groote, J., van de Pol, J. (2000). Equational Binary Decision Diagrams. In: Parigot, M., Voronkov, A. (eds) Logic for Programming and Automated Reasoning. LPAR 2000. Lecture Notes in Artificial Intelligence(), vol 1955. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44404-1_11
Download citation
DOI: https://doi.org/10.1007/3-540-44404-1_11
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-41285-4
Online ISBN: 978-3-540-44404-6
eBook Packages: Springer Book Archive