The canonical pairs of bounded depth Frege systems

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F67985840%3A_____%2F21%3A00535773" target="_blank" >RIV/67985840:_____/21:00535773 - isvavai.cz</a>

Výsledek na webu

<a href="https://doi.org/10.1016/j.apal.2020.102892" target="_blank" >https://doi.org/10.1016/j.apal.2020.102892</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1016/j.apal.2020.102892" target="_blank" >10.1016/j.apal.2020.102892</a>

Jazyk výsledku

angličtina

Název v původním jazyce

The canonical pairs of bounded depth Frege systems

Popis výsledku v původním jazyce

The canonical pair of a proof system P is the pair of disjoint NP sets where one set is the set of all satisfiable CNF formulas and the other is the set of CNF formulas that have P-proofs bounded by some polynomial. We give a combinatorial characterization of the canonical pairs of depth d Frege systems. Our characterization is based on certain games, introduced in this article, that are parametrized by a number k, also called the depth. We show that the canonical pair of a depth d Frege system is polynomially equivalent to the pair (Ad+2,Bd+2) where Ad+2 (respectively, Bd+1) are depth d+1 games in which Player I (Player II) has a positional winning strategy. Although this characterization is stated in terms of games, we will show that these combinatorial structures can be viewed as generalizations of monotone Boolean circuits. In particular, depth 1 games are essentially monotone Boolean circuits. Thus we get a generalization of the monotone feasible interpolation for Resolution, which is a property that enables one to reduce the task of proving lower bounds on the size of refutations to lower bounds on the size of monotone Boolean circuits. However, we do not have a method yet for proving lower bounds on the size of depth d games for d>1.

Název v anglickém jazyce

The canonical pairs of bounded depth Frege systems

Popis výsledku anglicky

The canonical pair of a proof system P is the pair of disjoint NP sets where one set is the set of all satisfiable CNF formulas and the other is the set of CNF formulas that have P-proofs bounded by some polynomial. We give a combinatorial characterization of the canonical pairs of depth d Frege systems. Our characterization is based on certain games, introduced in this article, that are parametrized by a number k, also called the depth. We show that the canonical pair of a depth d Frege system is polynomially equivalent to the pair (Ad+2,Bd+2) where Ad+2 (respectively, Bd+1) are depth d+1 games in which Player I (Player II) has a positional winning strategy. Although this characterization is stated in terms of games, we will show that these combinatorial structures can be viewed as generalizations of monotone Boolean circuits. In particular, depth 1 games are essentially monotone Boolean circuits. Thus we get a generalization of the monotone feasible interpolation for Resolution, which is a property that enables one to reduce the task of proving lower bounds on the size of refutations to lower bounds on the size of monotone Boolean circuits. However, we do not have a method yet for proving lower bounds on the size of depth d games for d>1.

Druh

J_imp - Článek v periodiku v databázi Web of Science

CEP obor

—

OECD FORD obor

10101 - Pure mathematics

Projekt

<a href="/cs/project/GX19-27871X" target="_blank" >GX19-27871X: Efektivní aproximační algoritmy a obvodová složitost</a><br>

Návaznosti

I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace

Rok uplatnění

2021

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název periodika

Annals of Pure and Applied Logic

ISSN

0168-0072

e-ISSN

1873-2461

Svazek periodika

172

Číslo periodika v rámci svazku

2

Stát vydavatele periodika

NL - Nizozemsko

Počet stran výsledku

41

Strana od-do

102892

Kód UT WoS článku

000594715500007

EID výsledku v databázi Scopus

2-s2.0-85092113495