Weizmann Logo
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style

Reports tagged with k-DNF resolution:
TR09-047 | 20th April 2009
Eli Ben-Sasson, Jakob Nordström

A Space Hierarchy for k-DNF Resolution

Comments: 1

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

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