Weizmann Logo
ECCC
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style



REPORTS > DETAIL:

Revision(s):

Revision #1 to TR11-006 | 3rd June 2011 09:28

Short Propositional Refutations for Dense Random 3CNF Formulas

RSS-Feed




Revision #1
Authors: Sebastian Müller, Iddo Tzameret
Accepted on: 3rd June 2011 09:28
Downloads: 1080
Keywords: 


Abstract:

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 $\Omega(n^{1.5-\epsilon}) $ 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 refutations in a non-abstract propositional proof system is for resolution with $\Omega(n^{2}/\log n) $ 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 for random 3CNF formulas, for sufficiently large clause-to-variable ratio. Specifically, we demonstrate polynomial-size propositional refutations whose lines are $TC^0$ formulas (i.e., $TC^0$-Frege proofs) for random 3CNF formulas with $ n $ variables and $ \Omega(n^{1.4}) $ clauses.

The idea is based on demonstrating efficient propositional correctness proofs of the random 3CNF unsatisfiability witnesses given by Feige, Kim and Ofek (2006). Since the soundness of these witnesses is verified using spectral techniques, we develop an appropriate way to reason about
eigenvectors in propositional systems. To carry out the full argument we work inside weak formal systems of arithmetic and use a general translation scheme to propositional proofs.



Changes to previous version:

Improved introduction and abstract and a changed title. Fixed some typos.


Paper:

TR11-006 | 20th January 2011 17:17

Average-Case Separation in Proof Complexity: Short Propositional Refutations for Random 3CNF Formulas





TR11-006
Authors: Sebastian Müller, Iddo Tzameret
Publication: 21st January 2011 10:06
Downloads: 1411
Keywords: 


Abstract:

Separating different propositional proof systems---that is, demonstrating that one proof system cannot efficiently simulate another proof system---is one of the main goals of proof complexity. Nevertheless, all known separation results between non-abstract proof systems are for specific families of hard tautologies: for what we know, in the average case all (non-abstract) propositional proof systems are no stronger than resolution. In this paper we show that this is not the case by demonstrating polynomial-size propositional refutations whose lines are $TC^0$ formulas (i.e., $TC^0$-Frege proofs) for random 3CNF formulas with $ n $ variables and $ \Omega(n^{1.4}) $ clauses. By known lower bounds on resolution refutations, this implies an exponential separation of $TC^0$-Frege from resolution in the average case.

The idea is based on demonstrating efficient propositional correctness proofs of the random 3CNF unsatisfiability witnesses given by Feige, Kim and Ofek [FOCS'06]. Since the soundness of these witnesses is verified using spectral techniques, we develop an appropriate way to reason about eigenvectors in propositional systems. To carry out the full argument we work inside weak formal systems of arithmetic, use a general translation scheme to propositional proofs and then show how to turn these proofs into random 3CNF refutations.



ISSN 1433-8092 | Imprint