A feasible interpolation for random resolution

TL;DR

This paper applies a feasible interpolation theorem to the random resolution proof system, establishing lower bounds for refutations of clique-coloring formulas, thereby advancing understanding of its proof complexity.

Contribution

It introduces a method to derive lower bounds for random resolution using feasible interpolation, connecting semantic derivations to proof complexity.

Findings

Lower bounds for random resolution refutations of clique-coloring formulas

Application of feasible interpolation theorem to semantic derivations

Enhanced understanding of proof complexity in 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.