Weizmann Logo
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style



TR09-100 | 16th October 2009 15:45

On Minimal Unsatisfiability and Time-Space Trade-offs for $k$-DNF Resolution


Authors: Jakob Nordström, Alexander Razborov
Publication: 18th October 2009 17:30
Downloads: 3275


In the context of proving lower bounds on proof space in $k$-DNF
resolution, [Ben-Sasson and Nordström 2009] introduced the concept of
minimally unsatisfiable sets of $k$-DNF formulas and proved that a
minimally unsatisfiable $k$-DNF set with $m$ formulas can have at most
$O((mk)^{k+1})$ variables. They also gave an example of such sets
with $\Omega(mk^2)$ variables.

In this paper we significantly improve the lower bound to
$\Omega(m)^k$, which almost matches the upper bound above.
Furthermore, we show that this implies that the analysis of their
technique for proving time-space separations and trade-offs for
$k$-DNF resolution is almost tight. This means that although it is
possible, or even plausible, that stronger results than in [Ben-Sasson
and Nordström 2009] should hold, a fundamentally different approach
would be needed to obtain such results.

ISSN 1433-8092 | Imprint