@inproceedings{5d77a9cccc954561b2754f1e968ca498,
title = "Resolution and binary decision diagrams cannot simulate each other polynomially",
abstract = "Proving formulas in propositional logic can be done in different ways. Some of these are based on of resolution, others on binary decision diagrams (BDDs). Experimental evidence suggests that BDDs and resolution based techniques are fundamentally different. This paper is an extended abstract of a paper [3] in which we confirm these findings by mathematical proof.We provide examples that are easy for BDDs and exponentially hard for any form of resolution, and vice versa, examples that are easy for resolution and exponentially hard for BDDs.",
author = "J.F. Groote and H. Zantema",
year = "2001",
doi = "10.1007/3-540-45575-2\_5",
language = "English",
isbn = "3-540-43075-X",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "33--38",
editor = "D Bjorner and M. Broy and M Broy and A. Zamulin",
booktitle = "Perspectives of System Informatics (Proceedings PSI2001, Akademgorodok, Novosibirsk, Russia, July 2-6, 2001, Revised Papers)",
address = "Germany",
}