Logic in Computer Science (LICS 2005)

Paper: Definability on a Random 3-CNF Formula (at LICS 2005)

Authors: Albert Atserias

Abstract

We consider the question of certifying unsatisfiability of random 3-CNF formulas. At which densities can we hope for a simple sufficient condition for unsatisfiability that holds almost surely? We study this question from the point of view of definability theory. The main result is that first-order logic cannot express any sufficient condition that holds almost surely on random 3-CNF formulas with n2-a clauses, for any irrational positive number a. In contrast, it can when the number of clauses is n2+a, for any positive a. As an intermediate step, our proof exploits the planted distribution for 3-CNF formulas in a new technical way. Moreover, the proof requires us to extend the methods of Shelah and Spencer for proving the zero-one law for sparse random graphs to arbitrary relational languages.

BibTeX

  @InProceedings{Atserias-DefinabilityonaRand,
    author = 	 {Albert Atserias},
    title = 	 {Definability on a Random 3-CNF Formula},
    booktitle =  {Proceedings of the Twentieth Annual IEEE Symp. on Logic in Computer Science, {LICS} 2005},
    year =	 2005,
    editor =	 {Prakash Panangaden},
    month =	 {June}, 
    pages =      {458--466},
    location =   {Chicago, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }