期刊名称：Electronic Colloquium on Computational Complexity
印刷版ISSN：1433-8092
出版年度：2011
卷号：2011
出版社：Universität Trier, Lehrstuhl für Theoretische Computer-Forschung
摘要：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 TC0 formulas (i.e., TC0-Frege proofs) for random 3CNF formulas with n variables and (n14) clauses. By known lower bounds on resolution refutations, this implies an exponential separation of TC0-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.
关键词：Proof Complexity, random 3SAT, Resolution, satisfiability
