Average-Case Separation in Proof Complexity:
Short Propositional Refutations for Random 3CNF Formulas
Iddo Tzameret
Abstract: Separating different propositional proof systems--that is,
demonstrating that one proof system cannot efficiently simulate
another proof system--is among 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; also known as
Threshold Logic) 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 (for this clause-to-variable
ratio).
The idea is based on demonstrating efficient propositional correctness
proofs of the random 3CNF unsatisfiability witnesses given by Feige,
Kim and Ofek (FOCS 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, use a
general translation scheme to propositional proofs and then show how
to turn these proofs into random 3CNF refutations.
Joint work with Sebastian Muller.