Under the auspices of the Computational Complexity Foundation (CCF)

TR04-118 | 21st December 2004
Marek Karpinski, Yakov Nekrich

#### A Note on Traversing Skew Merkle Trees

We consider the problem of traversing skew (unbalanced) Merkle
trees and design an algorithm for traversing a skew Merkle tree
in time O(log n/log t) and space O(log n (t/log t)), for any choice
of parameter t\geq 2.
This algorithm can be of special interest in situations when
more >>>

TR07-114 | 28th September 2007
Jakob Nordström

#### A Simplified Way of Proving Trade-off Results for Resolution

We present a greatly simplified proof of the length-space
trade-off result for resolution in Hertel and Pitassi (2007), and
also prove a couple of other theorems in the same vein. We point
out two important ingredients needed for our proofs to work, and
discuss possible conclusions to be drawn regarding ... more >>>

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

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

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 >>>

TR09-047 | 20th April 2009
Eli Ben-Sasson, Jakob Nordström

#### A Space Hierarchy for k-DNF Resolution

The k-DNF resolution proof systems are a family of systems indexed by
the integer k, where the kth member is restricted to operating with
formulas in disjunctive normal form with all terms of bounded arity k
(k-DNF formulas). This family was introduced in [Krajicek 2001] as an
extension of the ... more >>>

TR09-100 | 16th October 2009
Jakob Nordström, Alexander Razborov

#### On Minimal Unsatisfiability and Time-Space Trade-offs for \$k\$-DNF Resolution

In the context of proving lower bounds on proof space in \$k\$-DNF
resolution, [Ben-Sasson and Nordstr&ouml;m 2009] introduced the concept of
minimally unsatisfiable sets of \$k\$-DNF formulas and proved that a
minimally unsatisfiable \$k\$-DNF set with \$m\$ formulas can have at most
\$O((mk)^{k+1})\$ variables. They also gave an example of ... more >>>

TR10-045 | 15th March 2010
Jakob Nordström

#### On the Relative Strength of Pebbling and Resolution

Revisions: 1

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 ... 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 >>>

TR16-135 | 31st August 2016
Christoph Berkholz, Jakob Nordström

#### Near-Optimal Lower Bounds on Quantifier Depth and Weisfeiler-Leman Refinement Steps

We prove near-optimal trade-offs for quantifier depth versus number of variables in first-order logic by exhibiting pairs of n-element structures that can be distinguished by a k-variable first-order sentence but where every such sentence requires quantifier depth at least n^?(k/log k). Our trade-offs also apply to first-order counting logic, and ... more >>>

ISSN 1433-8092 | Imprint