On proof complexity of resolution over polynomial calculus

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F67985840%3A_____%2F22%3A00559957" target="_blank" >RIV/67985840:_____/22:00559957 - isvavai.cz</a>

Nalezeny alternativní kódy

RIV/00216208:11320/22:10456573

Výsledek na webu

<a href="https://doi.org/10.1145/3506702" target="_blank" >https://doi.org/10.1145/3506702</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1145/3506702" target="_blank" >10.1145/3506702</a>

Jazyk výsledku

angličtina

Název v původním jazyce

On proof complexity of resolution over polynomial calculus

Popis výsledku v původním jazyce

The proof system Res (PCd,R) is a natural extension of the Resolution proof system that instead of disjunctions of literals operates with disjunctions of degree d multivariate polynomials over a ring R with Boolean variables. Proving super-polynomial lower bounds for the size of Res(PC1,R)-refutations of Conjunctive normal forms (CNFs) is one of the important problems in propositional proof complexity. The existence of such lower bounds is even open for Res(PC1,) when is a finite field, such as 2. In this article, we investigate Res(PCd,R) and tree-like Res(PCd,R) and prove size-width relations for them when R is a finite ring. As an application, we prove new lower bounds and reprove some known lower bounds for every finite field as follows:(1)We prove almost quadratic lower bounds for Res(PCd,)-refutations for every fixed d. The new lower bounds are for the following CNFs:(a)Mod q Tseitin formulas (char() q) and Flow formulas,(b)Random k-CNFs with linearly many clauses.(2)We also prove super-polynomial (more than nk for any fixed k) and also exponential (2nμ for an μ > 0) lower bounds for tree-like Res(PCd,)-refutations based on how big d is with respect to n for the following CNFs:(a)Mod q Tseitin formulas (char()q) and Flow formulas,(b)Random k-CNFs of suitable densities,(c)Pigeonhole principle and Counting mod q principle. The lower bounds for the dag-like systems are the first nontrivial lower bounds for these systems, including the case d=1. The lower bounds for the tree-like systems were known for the case d=1 (except for the Counting mod q principle, in which lower bounds for the case d> 1 were known too). Our lower bounds extend those results to the case where d> 1 and also give new proofs for the case d=1.

Název v anglickém jazyce

On proof complexity of resolution over polynomial calculus

Popis výsledku anglicky

The proof system Res (PCd,R) is a natural extension of the Resolution proof system that instead of disjunctions of literals operates with disjunctions of degree d multivariate polynomials over a ring R with Boolean variables. Proving super-polynomial lower bounds for the size of Res(PC1,R)-refutations of Conjunctive normal forms (CNFs) is one of the important problems in propositional proof complexity. The existence of such lower bounds is even open for Res(PC1,) when is a finite field, such as 2. In this article, we investigate Res(PCd,R) and tree-like Res(PCd,R) and prove size-width relations for them when R is a finite ring. As an application, we prove new lower bounds and reprove some known lower bounds for every finite field as follows:(1)We prove almost quadratic lower bounds for Res(PCd,)-refutations for every fixed d. The new lower bounds are for the following CNFs:(a)Mod q Tseitin formulas (char() q) and Flow formulas,(b)Random k-CNFs with linearly many clauses.(2)We also prove super-polynomial (more than nk for any fixed k) and also exponential (2nμ for an μ > 0) lower bounds for tree-like Res(PCd,)-refutations based on how big d is with respect to n for the following CNFs:(a)Mod q Tseitin formulas (char()q) and Flow formulas,(b)Random k-CNFs of suitable densities,(c)Pigeonhole principle and Counting mod q principle. The lower bounds for the dag-like systems are the first nontrivial lower bounds for these systems, including the case d=1. The lower bounds for the tree-like systems were known for the case d=1 (except for the Counting mod q principle, in which lower bounds for the case d> 1 were known too). Our lower bounds extend those results to the case where d> 1 and also give new proofs for the case 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í

2022

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

ACM Transactions on Computational Logic

ISSN

1529-3785

e-ISSN

1557-945X

Svazek periodika

23

Číslo periodika v rámci svazku

3

Stát vydavatele periodika

US - Spojené státy americké

Počet stran výsledku

24

Strana od-do

16

Kód UT WoS článku

000831583400003

EID výsledku v databázi Scopus

2-s2.0-85135020022