TR09-100 Authors: Jakob NordstrÃ¶m, Alexander Razborov

Publication: 18th October 2009 17:30

Downloads: 2062

Keywords:

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.