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

Most state-of-the-art satisfiability algorithms today are variants of
the DPLL procedure augmented with clause learning. The main bottleneck
for such algorithms, other than the obvious one of time, is the amount
of memory used. In the field of proof complexity, the resources of
time and memory correspond to the length ... 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. 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 >>>