Witnesses for non-satisfiability of dense random 3CNF formulas

We consider random 3CNF formulas with n variables and m clauses. It is well known that when m > cn (for a sufficiently large constant c), most formulas are not satisfiable. However, it is not known whether such formulas are likely to have polynomial size witnesses that certify that they are not satisfiable. A value of m n3/2 was the forefront of our knowledge in this respect. When m > cn3/2 , such witnesses are known to exist, based on spectral techniques. When m < n3/2, it is known that resolution (which is a common approach for refutation) cannot produce witnesses of size smaller than 2n . Likewise, it is known that certain variants of the spectral techniques do not work in this range. In the current paper we show that when m > cn7/5 , almost all 3CNF formulas have polynomial size witnesses for non-satisfiability. We also show that such a witness can be found in time 2O(n0.2 log n) , whenever it exists. Our approach is based on an extension of the known spectral techniqu...

• Type: Conference
• Year: 2006
• Where: FOCS
• Authors: Uriel Feige, Jeong Han Kim, Eran Ofek
• Keywords: FOCS 2006, Formulas, Polynomial Size Witnesses, Spectral Techniques, Theoretical Computer Science