Weizmann Logo
ECCC
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style



REPORTS > KEYWORD > PEBBLE GAME:
Reports tagged with pebble game:
TR05-066 | 4th June 2005
Jakob Nordström

Narrow Proofs May Be Spacious: Separating Space and Width in Resolution

Revisions: 2 , Comments: 1

The width of a resolution proof is the maximal number of literals in any clause of the proof. The space of a proof is the maximal number of memory cells used if the proof is only allowed to resolve on clauses kept in memory. Both of these measures have previously ... more >>>


TR09-034 | 25th March 2009
Eli Ben-Sasson, Jakob Nordström

Understanding Space in Resolution: Optimal Lower Bounds and Exponential Trade-offs

Comments: 1

For current state-of-the-art satisfiability algorithms based on the
DPLL procedure and clause learning, the two main bottlenecks are the
amounts of time and memory used. Understanding time and memory
consumption, and how they are related to one another, is therefore a
question of considerable practical importance. In the field of ... more >>>


TR10-125 | 11th August 2010
Eli Ben-Sasson, Jakob Nordström

Understanding Space in Proof Complexity: Separations and Trade-offs via Substitutions

For current state-of-the-art satisfiability algorithms based on the DPLL procedure and clause learning, the two main bottlenecks are the amounts of time and memory used. In the field of proof complexity, these resources correspond to the length and space of resolution proofs for formulas in conjunctive normal form (CNF). There ... more >>>




ISSN 1433-8092 | Imprint