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

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