Thumbnail
Access Restriction
Subscribed

Author Atserias, Albert
Source ACM Digital Library
Content type Text
Publisher Association for Computing Machinery (ACM)
File Format PDF
Copyright Year ©2004
Language English
Subject Domain (in DDC) Computer science, information & general works ♦ Data processing & computer science
Subject Keyword Random CNF formulas ♦ Datalog ♦ Pebble games ♦ Phase transitions ♦ Propositional resolution ♦ Satisfiability
Abstract A descriptive complexity approach to random 3-SAT is initiated. We show that unsatisfiability of any significant fraction of random 3-CNF formulas cannot be certified by any property that is expressible in Datalog. Combined with the known relationship between the complexity of constraint satisfaction problems and expressibility in Datalog, our result implies that any constraint propagation algorithm working with small constraints will fail to certify unsatisfiability almost always. Our result is a consequence of designing a winning strategy for one of the players in the existential pebble game. The winning strategy makes use of certain extension axioms that we introduce and hold almost surely on a random 3-CNF formula. The second contribution of our work is the connection between finite model theory and propositional proof complexity. To make this connection explicit, we establish a tight relationship between the number of pebbles needed to win the game and the width of the Resolution refutations. As a consequence to our result and the known size--width relationship in Resolution, we obtain new proofs of the exponential lower bounds for Resolution refutations of random 3-CNF formulas and the Pigeonhole Principle.
ISSN 00045411
Age Range 18 to 22 years ♦ above 22 year
Educational Use Research
Education Level UG and PG
Learning Resource Type Article
Publisher Date 2004-03-01
Publisher Place New York
e-ISSN 1557735X
Journal Journal of the ACM (JACM)
Volume Number 51
Issue Number 2
Page Count 31
Starting Page 281
Ending Page 311


Open content in new tab

   Open content in new tab
Source: ACM Digital Library