In the context of proving lower bounds on proof space in k -DNFresolution, [Ben-Sasson and Nordström 2009] introduced the concept ofminimally unsatisfiable sets of k -DNF formulas and proved that aminimally unsatisfiable k -DNF set with m formulas can have at mostO((mk)k+1) variables. They also gave an example of such setswith (mk2) variables.

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