Easily Refutable Subformulas of Large Random 3CNF Formulas

Abstract. A simple nonconstructive argument shows that most 3CNF formulas with cn clauses (where c is a large enough 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 3CNF formulas with cn3/2 clauses (where c is a large enough constant) finds a subformula with O(c2 n) clauses and then proves 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 3CNF formulas with at least poly(log(n)) · n3/2 clauses. Our algorithm is simple enough to run in practice. We present some preliminary experimental results.

• Type: Conference
• Year: 2004
• Where: ICALP
• Authors: Uriel Feige, Eran Ofek
• Keywords: Cn Clauses, Efficient Refutation Algorithm, Formulas, ICALP 2004, Theoretical Computer Science