ECCC-Report TR09-100https://eccc.weizmann.ac.il/report/2009/100Comments and Revisions published for TR09-100en-usSun, 18 Oct 2009 17:30:14 +0200
Paper TR09-100
| On Minimal Unsatisfiability and Time-Space Trade-offs for $k$-DNF Resolution |
Jakob NordstrÃ¶m,
Alexander Razborov
https://eccc.weizmann.ac.il/report/2009/100In the context of proving lower bounds on proof space in $k$-DNF
resolution, [Ben-Sasson and Nordstr&ouml;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&ouml;m 2009] should hold, a fundamentally different approach
would be needed to obtain such results.Sun, 18 Oct 2009 17:30:14 +0200https://eccc.weizmann.ac.il/report/2009/100