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.Comment: Preprint April 2016, revised September and October 2016

@article{paperbot208,
  title = {A feasible interpolation for random resolution},
  author = {Jan Krajicek},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 13, Issue 1},
  year = {2017},
  doi = {10.23638/lmcs-13(1:5)2017}
}