Short Propositional Refutations for Dense Random 3CNF Formulas

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216208%3A11320%2F12%3A10129471" target="_blank" >RIV/00216208:11320/12:10129471 - isvavai.cz</a>

Výsledek na webu

<a href="http://dx.doi.org/10.1109/LICS.2012.60" target="_blank" >http://dx.doi.org/10.1109/LICS.2012.60</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1109/LICS.2012.60" target="_blank" >10.1109/LICS.2012.60</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Short Propositional Refutations for Dense Random 3CNF Formulas

Popis výsledku v původním jazyce

Random 3CNF formulas constitute an important distribution for measuring the average-case behavior of propositional proof systems. Lower bounds for random 3CNF refutations in many propositional proof systems are known. Most notably are the exponential-size resolution refutation lower bounds for random 3CNF formulas with (n15MINUS SIGN ) clauses [Chvatal and Szemeredi (1988), Ben-Sasson and Wigderson (2001)]. On the other hand, the only known non-trivial upper bound on the size of random 3CNF refutationsin a non-abstract propositional proof system is for resolution with (n2logn) clauses, shown by Beame et al. (2002). In this paper we show that already standard propositional proof systems, within the hierarchy of Frege proofs, admit short refutations forrandom 3CNF formulas, for sufficiently large clause-to-variable ratio. Specifically, we demonstrate polynomial-size propositional refutations whose lines are TC0 formulas (i.e., TC0-Frege proofs) for random 3CNF formulas with n variables

Název v anglickém jazyce

Short Propositional Refutations for Dense Random 3CNF Formulas

Popis výsledku anglicky

Random 3CNF formulas constitute an important distribution for measuring the average-case behavior of propositional proof systems. Lower bounds for random 3CNF refutations in many propositional proof systems are known. Most notably are the exponential-size resolution refutation lower bounds for random 3CNF formulas with (n15MINUS SIGN ) clauses [Chvatal and Szemeredi (1988), Ben-Sasson and Wigderson (2001)]. On the other hand, the only known non-trivial upper bound on the size of random 3CNF refutationsin a non-abstract propositional proof system is for resolution with (n2logn) clauses, shown by Beame et al. (2002). In this paper we show that already standard propositional proof systems, within the hierarchy of Frege proofs, admit short refutations forrandom 3CNF formulas, for sufficiently large clause-to-variable ratio. Specifically, we demonstrate polynomial-size propositional refutations whose lines are TC0 formulas (i.e., TC0-Frege proofs) for random 3CNF formulas with n variables

Druh

D - Stať ve sborníku

CEP obor

BA - Obecná matematika

OECD FORD obor

—

Projekt

—

Návaznosti

I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace

Rok uplatnění

2012

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 statě ve sborníku

27th Annual IEEE Symposium on Logic in Computer Science

ISBN

978-1-4673-2263-8

ISSN

1043-6871

e-ISSN

—

Počet stran výsledku

10

Strana od-do

501-510

Název nakladatele

IEEE Xplore

Místo vydání

Chorvatsko

Místo konání akce

Dubrovník, Chorvatsko

Datum konání akce

25. 6. 2012

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

—