arXiv · 1604.06560
A feasible interpolation for random resolution
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.
Explore related subjects
Keep this discovery
Jan Krajicek. 2016-04-22. A feasible interpolation for random resolution. https://doi.org/10.23638/lmcs-13(1%3A5)2017
Cite the original work for its findings. Save a collection to share your selection of sources.