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

TL;DR

This paper improves lower bounds on the size of minimally unsatisfiable k-DNF sets, nearly matching known upper bounds, and demonstrates that existing proof techniques for time-space trade-offs in k-DNF resolution are nearly optimal.

Contribution

It significantly tightens the lower bounds on minimally unsatisfiable k-DNF sets, nearly matching the upper bounds, and shows existing methods are close to optimal for proving time-space trade-offs.

Findings

Lower bound improved to Omega(m)^k for minimally unsatisfiable k-DNF sets.

Analysis of existing proof techniques for time-space trade-offs is nearly tight.

Existing bounds suggest that stronger results require fundamentally different approaches.

Abstract

In the context of proving lower bounds on proof space in k-DNF resolution, [Ben-Sasson and Nordstrom 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 Nordstrom 2009] should hold, a fundamentally different approach would be needed to obtain such results.