Under the auspices of the Computational Complexity Foundation (CCF)

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

#### A Space Hierarchy for k-DNF Resolution

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

TR20-037 | 18th March 2020
Michal Garlik

#### Failure of Feasible Disjunction Property for \$k\$-DNF Resolution and NP-hardness of Automating It

We show that for every integer \$k \geq 2\$, the Res(\$k\$) propositional proof system does not have the weak feasible disjunction property. Next, we generalize a recent result of Atserias and Müller [FOCS, 2019] to Res(\$k\$). We show that if NP is not included in P (resp. QP, SUBEXP) then ... more >>>

ISSN 1433-8092 | Imprint