Randomized feasible interpolation and monotone circuits with a local oracle

TL;DR

This paper extends feasible interpolation to randomized protocols and introduces monotone circuits with a local oracle, linking semantic derivations to small randomized protocols and exploring lower bounds in proof complexity.

Contribution

It generalizes feasible interpolation to randomized protocols and introduces monotone circuits with a local oracle, connecting semantic derivations to communication complexity.

Findings

Randomized feasible interpolation applies to various proof systems.

Short semantic derivations lead to small randomized protocols.

Open problem: lower bounds for monotone CLOs separating NP sets.

Abstract

We generalize the feasible interpolation theorem for semantic derivations from K.(1997) by allowing randomized protocols (protocols in the sense of K.(1997). We also introduce an extension of the monotone circuit model, monotone circuits with a local oracle (CLOs), that does correspond to communication protocols for the monotone Karchmer-Wigderson multi-function $KW^m[U,V]$ making errors. The new randomized feasible interpolation thus shows that a short semantic derivation (from a certain class of derivations larger than in the original method) of the disjointness of $U, V$, $U$ closed upwards, yields a small randomized protocol for and hence a small monotone CLO separating the sets. To establish a lower bound for monotone CLOs separating two NP sets, one closed upwards, is an open problem. This research is motivated by the open problem to establish a lower bound for proof system $R(LIN)$ operating with clauses formed by linear Boolean functions over the 2-element field. The new randomized feasible interpolation applies to this proof system and also to the semantic versions of the cutting planes proof system CP (as randomized protocols efficiently simulate protocols with small real communication complexity of K.(1998)), to small width resolution over CP, R(CP), and to random resolution RR of Buss, Kolodziejczyk and Thapen (2014).