A feasible interpolation for random resolution
Logic
2017-02-15 v5 Computational Complexity
Abstract
Random resolution, defined by Buss, Kolodziejczyk and Thapen (JSL, 2014), is a sound propositional proof system that extends the resolution proof system by the possibility to augment any set of initial clauses by a set of randomly chosen clauses (modulo a technical condition). We show how to apply the general feasible interpolation theorem for semantic derivations of Krajicek (JSL, 1997) to random resolution. As a consequence we get a lower bound for random resolution refutations of the clique-coloring formulas.
Cite
@article{arxiv.1604.06560,
title = {A feasible interpolation for random resolution},
author = {Jan Krajicek},
journal= {arXiv preprint arXiv:1604.06560},
year = {2017}
}
Comments
Preprint April 2016, revised September and October 2016