Under the auspices of the Computational Complexity Foundation (CCF)

REPORTS > DETAIL:

### Paper:

TR13-018 | 29th January 2013 16:43

#### Exponential Lower Bounds for Refuting Random Formulas Using Ordered Binary Decision Diagrams

TR13-018
Authors: Luke Friedman, Yixin Xu
Publication: 29th January 2013 20:17
We show that for some constant $\epsilon > 0$, with high probability an OBDD* refutation of an unsatisfiable random 3-CNF formula must be of size at least $2^{\epsilon n}$, and an OBDD+ refutation of an unsatisfiable random 3-XOR formula must be of size at least $2^{\epsilon n}$.