On minimal unsatisfiability and time-space trade-offs for k-DNF resolution
(2011) 38th International Colloquium on Automata, Languages and Programming, ICALP 2011 In Lecture Notes in Computer Science 6755(PART 1). p.642-653- Abstract
A well-known theorem by Tarsi states that a minimally unsatisfiable CNF formula with m clauses can have at most m - 1 variables, and this bound is exact. In the context of proving lower bounds on proof space in k-DNF resolution, [Ben-Sasson and Nordström 2009] extended the concept of minimal unsatisfiability to sets of k-DNF formulas and proved that a minimally unsatisfiable k-DNF set with m formulas can have at most (mk) k + 1 variables. This result is far from tight, however, since they could only present explicit constructions of minimally unsatisfiable sets with Ω(mk 2) variables. In the current paper, we revisit this combinatorial problem and significantly improve the lower bound to (Ω(m)) k , which... (More)
A well-known theorem by Tarsi states that a minimally unsatisfiable CNF formula with m clauses can have at most m - 1 variables, and this bound is exact. In the context of proving lower bounds on proof space in k-DNF resolution, [Ben-Sasson and Nordström 2009] extended the concept of minimal unsatisfiability to sets of k-DNF formulas and proved that a minimally unsatisfiable k-DNF set with m formulas can have at most (mk) k + 1 variables. This result is far from tight, however, since they could only present explicit constructions of minimally unsatisfiable sets with Ω(mk 2) variables. In the current paper, we revisit this combinatorial problem and significantly improve the lower bound to (Ω(m)) k , which almost matches the upper bound above. Furthermore, using similar ideas we show that the analysis of the technique in [Ben-Sasson and Nordström 2009] 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.
(Less)
- author
- Nordström, Jakob LU and Razborov, Alexander
- publishing date
- 2011
- type
- Chapter in Book/Report/Conference proceeding
- publication status
- published
- subject
- host publication
- Automata, Languages and Programming : 38th International Colloquium, ICALP 2011, Proceedings - 38th International Colloquium, ICALP 2011, Proceedings
- series title
- Lecture Notes in Computer Science
- volume
- 6755
- issue
- PART 1
- edition
- PART 1
- pages
- 12 pages
- publisher
- Springer
- conference name
- 38th International Colloquium on Automata, Languages and Programming, ICALP 2011
- conference location
- Zurich, Switzerland
- conference dates
- 2011-07-04 - 2011-07-08
- external identifiers
-
- scopus:79959927201
- ISSN
- 1611-3349
- 0302-9743
- ISBN
- 9783642220050
- DOI
- 10.1007/978-3-642-22006-7_54
- language
- English
- LU publication?
- no
- id
- ee9f0ac1-5471-4dd5-abc2-b966511d49fd
- date added to LUP
- 2020-12-18 22:27:57
- date last changed
- 2025-04-04 14:29:04
@inproceedings{ee9f0ac1-5471-4dd5-abc2-b966511d49fd,
abstract = {{<p>A well-known theorem by Tarsi states that a minimally unsatisfiable CNF formula with m clauses can have at most m - 1 variables, and this bound is exact. In the context of proving lower bounds on proof space in k-DNF resolution, [Ben-Sasson and Nordström 2009] extended the concept of minimal unsatisfiability to sets of k-DNF formulas and proved that a minimally unsatisfiable k-DNF set with m formulas can have at most (mk) <sup>k + 1</sup> variables. This result is far from tight, however, since they could only present explicit constructions of minimally unsatisfiable sets with Ω(mk <sup>2</sup>) variables. In the current paper, we revisit this combinatorial problem and significantly improve the lower bound to (Ω(m)) <sup>k</sup> , which almost matches the upper bound above. Furthermore, using similar ideas we show that the analysis of the technique in [Ben-Sasson and Nordström 2009] 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.</p>}},
author = {{Nordström, Jakob and Razborov, Alexander}},
booktitle = {{Automata, Languages and Programming : 38th International Colloquium, ICALP 2011, Proceedings}},
isbn = {{9783642220050}},
issn = {{1611-3349}},
language = {{eng}},
number = {{PART 1}},
pages = {{642--653}},
publisher = {{Springer}},
series = {{Lecture Notes in Computer Science}},
title = {{On minimal unsatisfiability and time-space trade-offs for k-DNF resolution}},
url = {{http://dx.doi.org/10.1007/978-3-642-22006-7_54}},
doi = {{10.1007/978-3-642-22006-7_54}},
volume = {{6755}},
year = {{2011}},
}