Resolution and Binary Decision Diagrams Cannot Simulate Each Other Polynomially

1. Ben-Sasson, E., and Wigderson, A. Short proofs are narrow-resolution made simple. In Proceedings of the 31st Annual ACM Symposium on Theory of Computing (1999), pp. 517–526.

   Google Scholar 

2. Bryant, R. E. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers C-35, 8 (1986), 677–691.

   Article  Google Scholar 

3. Groote, J. F., and Zantema, H. Resolution and binary decision diagrams cannot simulate each other polynomially. Journal of Discrete Applied Mathematics (2001). To appear.

   Google Scholar 

4. Haken, A. The intractability of resolution. Theoretical Computer Science 39 (1985), 297–308.

   Article  MATH  MathSciNet  Google Scholar 

5. Meinel, C., and Theobald, T. Algorithms and Data Structures in VLSI Design: OBDD— Foundations and Applications. Springer, 1998.

   Google Scholar 

6. Tseitin, G. On the complexity of derivation in propositional calculus. In Studies in Constructive Mathematics and Mathematical Logic, part 2 (1968), pp. 115–125. Reprinted in J. Siekmann and G. Wrightson (editors),Automation of reasoning vol. 2, pp. 466–483.,Springer-Verlag Berlin, 1983.

   Google Scholar 

7. Uribe, T. E., and Stickel, M. E. Ordered binary decision diagrams and the Davis-Putnam procedure. In First conference on Constraints in Computational Logic(1994), J.-P. Jouannaud, Ed., vol. 845of Lecture Notes in Computer Science, Springer, pp. 34–49.

   Google Scholar 

8. Urquhart, A. Hard examples for resolution. Journal of the ACM 34, 1 (1987), 209–219.

   Article  MathSciNet  Google Scholar 

9. Urquhart, A. The complexity of propositional proofs. The Bulletin of Symbolic Logic 1, 4 (1995), 425–467.

   Article  MathSciNet  Google Scholar 

10. Zantema, H., and van de Pol, J. C. A rewriting approach to binary decision diagrams. Journal of Logic and Algebraic Programming (2001). To appear.

    Google Scholar 

Download references