Volume 3 (2007) Article 2 pp. 25-43

Easily refutable subformulas of large random 3CNF formulas

by Uriel Feige and Eran Ofek

Received: May 2, 2006
Published: February 9, 2007
DOI: 10.4086/toc.2007.v003a002

Download article from ToC site:
[PS (400K)]    [PS.GZ (105K)]    [PS.ZIP (105K)]
[PDF (217K)]    [DVI (168K)]    [TeX (61K)]
Misc.:
[HTML Bibliography] [Bibliography Source] [BibTeX] 
[About the Author(s)]
Keywords: proof complexity, average case analysis, Boolean formula, 3CNF, refutation, spectral method
Categories: complexity theory, proof complexity, average case, formulas, Boolean formulas, CNF-DNF formulas
ACM Classification: F.2.2
AMS Classification: 68Q17, 68Q25

Abstract: [Plain Text Version]

A simple nonconstructive argument shows that most 3-CNF formulas with cn clauses (where c is a sufficiently large constant) are not satisfiable. It is an open question whether there is an efficient refutation algorithm that for most formulas with cn clauses proves that they are not satisfiable. We present a polynomial time algorithm that for most 3-CNF formulas with cn3/2 clauses (where c is a sufficiently large constant) finds a subformula with Θ(c2n) clauses and then uses spectral methods to prove that this subformula is not satisfiable (and hence that the original formula is not satisfiable). Previously, it was only known how to efficiently certify the unsatisfiability of random 3-CNF formulas with at least   polylog(n)n3/2 clauses. Our algorithm is simple enough to run in practice. We present some experimental results.