Sciweavers

Share
ERSHOV
2001
Springer

Resolution and Binary Decision Diagrams Cannot Simulate Each Other Polynomially

9 years 5 months ago
Resolution and Binary Decision Diagrams Cannot Simulate Each Other Polynomially
There are many different ways of proving formulas in proposition logic. Many of these can easily be characterized as forms of resolution (e.g. [12] and [9]). Others use so-called binary decision diagrams (BDDs) [2, 10]. Experimental evidence suggests that BDDs and resolution based techniques are fundamentally different, in the sense that their performance can differ very much on benchmarks [14]. In this paper 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.
Jan Friso Groote, Hans Zantema
Added 28 Jul 2010
Updated 28 Jul 2010
Type Conference
Year 2001
Where ERSHOV
Authors Jan Friso Groote, Hans Zantema
Comments (0)
books