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 the exact ... more >>>

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

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

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

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