Average-Case Separation in Proof Complexity: Short Propositional Refutations for Random 3CNF Formulas
Sebastian Müller, Iddo Tzameret · arXiv (Cornell University) · 2011
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 formulas (i.e., TC-Frege proofs) for random 3CNF formulas with n variables and Ω(n) clauses. By known lower bounds on resolution refutations, this implies an exponential separation of TC -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 [17]. 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. Faculty of Mathematics and Physics, Charles University, Prague, Czech Republic. Email: [email protected]. Supported by the Marie Curie Initial Training Network in Mathematical Logic MALOA From MAthematical LOgic to Applications, PITN-GA-2009-238381 Institute for Theoretical Computer Science, the Institute for Interdisciplinary Information Sciences, Tsinghua University, Beijing, 100084, China. Email: [email protected]. Supported by the National Natural Science Foundation of China Grant and the National Basic Research Program of China Grant; Part of this work was done while the author was a research fellow at the Mathematical Institute of the Academy of Science, Prague, Czech Republic, supported by The Eduard Cech Center for Algebra and Geometry and The John Templeton Foundation. ISSN 1433-8092 Electronic Colloquium on Computational Complexity, Report No. 6 (2011)