NDLI: On sufficient conditions for unsatisfiability of random formulas

Content Provider	ACM Digital Library
Author	Atserias, Albert
Copyright Year	2004
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.
Starting Page	281
Ending Page	311
Page Count	31
File Format	PDF
ISSN	00045411
e-ISSN	1557735X
DOI	10.1145/972639.972645
Journal	Journal of the ACM (JACM)
Volume Number	51
Issue Number	2
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	2004-03-01
Publisher Place	New York
Access Restriction	One Nation One Subscription (ONOS)
Subject Keyword	Random CNF formulas Datalog Pebble games Phase transitions Propositional resolution Satisfiability
Content Type	Text
Resource Type	Article
Subject	Hardware and Architecture Information Systems Control and Systems Engineering Artificial Intelligence Software

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

On the maximum satisfiability of random formulas

Static analysis in datalog extensions

The Local Lemma Is Asymptotically Tight for SAT

On Sufficient Conditions for Unsatisfiability of Random Formulas (2003)

An improved exponential-time algorithm for $\textit{k}-SAT$

MaxSAT resolution for regular propositional logic

Decomposable negation normal form

Sufficient Conditions for the Success of GPS

Propositional proof complexity

On sufficient conditions for unsatisfiability of random formulas

Similar Documents

On the maximum satisfiability of random formulas

Static analysis in datalog extensions

The Local Lemma Is Asymptotically Tight for SAT

On Sufficient Conditions for Unsatisfiability of Random Formulas (2003)

An improved exponential-time algorithm for $\textit{k}-SAT$

MaxSAT resolution for regular propositional logic

Decomposable negation normal form

Sufficient Conditions for the Success of GPS

Propositional proof complexity

On sufficient conditions for unsatisfiability of random formulas