Marek Karpinski, Yakov Nekrich

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

Jakob Nordström

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

Eli Ben-Sasson, Jakob Nordström

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

Eli Ben-Sasson, Jakob Nordström

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

Jakob Nordström, Alexander Razborov

In the context of proving lower bounds on proof space in $k$-DNF

resolution, [Ben-Sasson and Nordströ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 >>>

Jakob Nordström

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

Eli Ben-Sasson, Jakob Nordström

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

Christoph Berkholz, Jakob Nordström

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