NDLI: On the Relative Strength of Pebbling and Resolution

Please wait, while we are loading the content...

ACM Transactions on Computational Logic (TOCL) : Volume 17

ACM Transactions on Computational Logic (TOCL) : Volume 16

ACM Transactions on Computational Logic (TOCL) : Volume 15

ACM Transactions on Computational Logic (TOCL) : Volume 14

ACM Transactions on Computational Logic (TOCL) : Volume 13

Issue 4, October 2012

Issue 3, August 2012

Issue 2, April 2012

Nominal Unification from a Higher-Order Perspective

Interactive Realizers: A New Approach to Program Extraction from Nonconstructive Proofs

Model Checking of Recursive Probabilistic Systems

Annotated Probabilistic Temporal Logic: Approximate Fixpoint Implementation

Simplification Rules for Intuitionistic Propositional Tableaux

Complexity of Data Dependence Problems for Program Schemas with Concurrency

On the Relative Strength of Pebbling and Resolution

The Complexity of Reasoning for Fragments of Autoepistemic Logic

An Implicit Characterization of PSPACE

Issue 1, January 2012

ACM Transactions on Computational Logic (TOCL) : Volume 12

ACM Transactions on Computational Logic (TOCL) : Volume 11

ACM Transactions on Computational Logic (TOCL) : Volume 10

ACM Transactions on Computational Logic (TOCL) : Volume 9

ACM Transactions on Computational Logic (TOCL) : Volume 8

ACM Transactions on Computational Logic (TOCL) : Volume 7

ACM Transactions on Computational Logic (TOCL) : Volume 6

ACM Transactions on Computational Logic (TOCL) : Volume 5

ACM Transactions on Computational Logic (TOCL) : Volume 4

ACM Transactions on Computational Logic (TOCL) : Volume 3

ACM Transactions on Computational Logic (TOCL) : Volume 2

ACM Transactions on Computational Logic (TOCL) : Volume 1

On the Relative Strength of Pebbling and Resolution

Content Provider	ACM Digital Library
Author	Nordström, Jakob
Copyright Year	2012
Abstract	The last decade has seen a revival of interest in pebble games in the context of proof complexity. Pebbling has proven to be a useful tool for studying resolution-based proof systems when comparing the strength of different subsystems, showing bounds on proof space, and establishing size-space trade-offs. The typical approach has been to encode the pebble game played on a graph as a CNF formula and then argue that proofs of this formula must inherit (various aspects of) the pebbling properties of the underlying graph. Unfortunately, the reductions used here are not tight. To simulate resolution proofs by pebblings, the full strength of nondeterministic black-white pebbling is needed, whereas resolution is only known to be able to simulate deterministic black pebbling. To obtain strong results, one therefore needs to find specific graph families which either have essentially the same properties for black and black-white pebbling (not at all true in general) or which admit simulations of black-white pebblings in resolution. This article contributes to both these approaches. First, we design a restricted form of black-white pebbling that can be simulated in resolution and show that there are graph families for which such restricted pebblings can be asymptotically better than black pebblings. This proves that, perhaps somewhat unexpectedly, resolution can strictly beat black-only pebbling, and in particular that the space lower bounds on pebbling formulas in Ben-Sasson and Nordström [2008] are tight. Second, we present a versatile parametrized graph family with essentially the same properties for black and black-white pebbling, which gives sharp simultaneous trade-offs for black and black-white pebbling for various parameter settings. Both of our contributions have been instrumental in obtaining the time-space trade-off results for resolution-based proof systems in Ben-Sasson and Nordström [2011].
Starting Page	1
Ending Page	43
Page Count	43
File Format	PDF
ISSN	15293785
e-ISSN	1557945X
DOI	10.1145/2159531.2159538
Volume Number	13
Issue Number	2
Journal	ACM Transactions on Computational Logic (TOCL)
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	2012-04-01
Publisher Place	New York
Access Restriction	One Nation One Subscription (ONOS)
Subject Keyword	Proof complexity Pebble games Pebbling formula Resolution Space Trade-off
Content Type	Text
Resource Type	Article
Subject	Theoretical Computer Science Logic Computational Mathematics Computer Science

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 Relative Strength of Pebbling and Resolution

A On the Relative Strength of Pebbling and Resolution

On the relative strength of pebbling and resolution (Extended Abstract) (2010)

On the relative strength of pebbling and resolution (2012).

Pebble Games, Proof Complexity, and Time-Space Trade-offs

PEBBLE GAMES, PROOF COMPLEXITY, AND TIME-SPACE TRADE-OFFS (2013)

PEBBLE GAMES, PROOF COMPLEXITY, AND TIME-SPACE TRADE-OFFS (2013)

Some trade-off results for polynomial calculus: extended abstract

On the Proof Complexity of Paris-Harrington and Off-Diagonal Ramsey Tautologies

On the Relative Strength of Pebbling and Resolution

Similar Documents

On the Relative Strength of Pebbling and Resolution

A On the Relative Strength of Pebbling and Resolution

On the relative strength of pebbling and resolution (Extended Abstract) (2010)

On the relative strength of pebbling and resolution (2012).

Pebble Games, Proof Complexity, and Time-Space Trade-offs

PEBBLE GAMES, PROOF COMPLEXITY, AND TIME-SPACE TRADE-OFFS (2013)

PEBBLE GAMES, PROOF COMPLEXITY, AND TIME-SPACE TRADE-OFFS (2013)

Some trade-off results for polynomial calculus: extended abstract

On the Proof Complexity of Paris-Harrington and Off-Diagonal Ramsey Tautologies

On the Relative Strength of Pebbling and Resolution