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