On Protocols for Monotone Feasible Interpolation

TL;DR

This paper investigates various types of communication protocols used in monotone feasible interpolation, comparing their strengths and implications for proof complexity lower bounds, particularly focusing on protocols with equality and inequalities.

Contribution

It introduces a comparison framework for three kinds of protocols and establishes relationships among their strengths, highlighting the significance of protocols with equality for proof complexity lower bounds.

Findings

Protocols with equality are at least as strong as those with inequality.

Protocols with equality are as strong as those with a conjunction of two inequalities.

Exponential lower bounds are known for protocols with inequality.

Abstract

Feasible interpolation is a general technique for proving proof complexity lower bounds. The monotone version of the technique converts, in its basic variant, lower bounds for monotone Boolean circuits separating two NP-sets to proof complexity lower bounds. In a generalized version of the technique, dag-like communication protocols are used instead of monotone Boolean circuits. We study three kinds of protocols and compare their strength. Our results establish the following relationships in the sense of polynomial reducibility: Protocols with equality are at least as strong as protocols with inequality and protocols with equality have the same strength as protocols with a conjunction of two inequalities. Exponential lower bounds for protocols with inequality are known. Obtaining lower bounds for protocols with equality would immediately imply lower bounds for resolution with parities (R(LIN)).