Weizmann Logo
ECCC
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style



REPORTS > DETAIL:

Paper:

TR13-018 | 29th January 2013 16:43

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

RSS-Feed




TR13-018
Authors: Luke Friedman, Yixin Xu
Publication: 29th January 2013 20:17
Downloads: 2977
Keywords: 


Abstract:

A propositional proof system based on ordered binary decision diagrams (OBDDs) was introduced by Atserias et al. Krajicek proved exponential lower bounds for a strong variant of this system using feasible interpolation, and Tveretina et al. proved exponential lower bounds for restricted versions of this system for refuting formulas derived from the Pigeonhole Principle.
In this paper we prove the first lower bounds for refuting randomly generated unsatisfiable formulas in restricted versions of this OBDD-based proof system.
In particular we consider two systems OBDD* and OBDD+; OBDD* is restricted by having a fixed, predetermined variable order for all OBDDs in its refutations, and OBDD+ is restricted by having a fixed order in which the clauses of the input formula must be processed.
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}$.



ISSN 1433-8092 | Imprint