ECCC-Report TR07-126https://eccc.weizmann.ac.il/report/2007/126Comments and Revisions published for TR07-126en-usFri, 07 Dec 2007 12:02:45 +0200
Paper TR07-126
| On the relative efficiency of resolution-like proofs and ordered binary decision diagram proofs |
Nathan Segerlind
https://eccc.weizmann.ac.il/report/2007/126We show that tree-like OBDD proofs of unsatisfiability require an exponential increase ($s \mapsto 2^{s^{\Omega(1)}}$) in proof size to simulate unrestricted resolution, and that unrestricted OBDD proofs of unsatisfiability require an almost-exponential increase ($s \mapsto 2^{ 2^{\left( \log s \right)^{\Omega(1)}}}$) in proof size to simulate $\Res{O(\log n)}$. The ``OBDD proof system'' that we consider has lines that are ordered binary decision diagrams in the same variables as the input formula, and is allowed to combine two previously derived OBDDs by any sound inference rule. In particular, this system abstracts satisfiability algorithms based upon explicit construction of OBDDs and satisfiability algorithms based upon symbolic quantifier elimination.
Fri, 07 Dec 2007 12:02:45 +0200https://eccc.weizmann.ac.il/report/2007/126