Short Propositional Refutations for Dense Random 3CNF Formulas
The result's identifiers
Result code in 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>
Result on the web
<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>
Alternative languages
Result language
angličtina
Original language name
Short Propositional Refutations for Dense Random 3CNF Formulas
Original language description
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
Czech name
—
Czech description
—
Classification
Type
D - Article in proceedings
CEP classification
BA - General mathematics
OECD FORD branch
—
Result continuities
Project
—
Continuities
I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace
Others
Publication year
2012
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Article name in the collection
27th Annual IEEE Symposium on Logic in Computer Science
ISBN
978-1-4673-2263-8
ISSN
1043-6871
e-ISSN
—
Number of pages
10
Pages from-to
501-510
Publisher name
IEEE Xplore
Place of publication
Chorvatsko
Event location
Dubrovník, Chorvatsko
Event date
Jun 25, 2012
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
—