Trade-offs between time and memory in a tighter model of CDCL SAT solvers
(2016) 19th International Conference on Theory and Applications of Satisfiability Testing, SAT 2016 In Lecture Notes in Computer Science 9710. p.160-176- Abstract
A long line of research has studied the power of conflict- driven clause learning (CDCL) and how it compares to the resolution proof system in which it searches for proofs. It has been shown that CDCL can polynomially simulate resolution even with an adversarially chosen learning scheme as long as it is asserting. However, the simulation only works under the assumption that no learned clauses are ever forgot- ten, and the polynomial blow-up is significant. Moreover, the simulation requires very frequent restarts, whereas the power of CDCL with less frequent or entirely without restarts remains poorly understood. With a view towards obtaining results with tighter relations between CDCL and resolution, we introduce a more fine-grained... (More)
A long line of research has studied the power of conflict- driven clause learning (CDCL) and how it compares to the resolution proof system in which it searches for proofs. It has been shown that CDCL can polynomially simulate resolution even with an adversarially chosen learning scheme as long as it is asserting. However, the simulation only works under the assumption that no learned clauses are ever forgot- ten, and the polynomial blow-up is significant. Moreover, the simulation requires very frequent restarts, whereas the power of CDCL with less frequent or entirely without restarts remains poorly understood. With a view towards obtaining results with tighter relations between CDCL and resolution, we introduce a more fine-grained model of CDCL that cap- tures not only time but also memory usage and number of restarts. We show how previously established strong size-space trade-offs for resolution can be transformed into equally strong trade-offs between time and memory usage for CDCL, where the upper bounds hold for CDCL with- out any restarts using the standard 1UIP clause learning scheme, and the (in some cases tightly matching) lower bounds hold for arbitrarily frequent restarts and arbitrary clause learning schemes.
(Less)
- author
- Elffers, Jan LU ; Johannsen, Jan ; Lauria, Massimo ; Magnard, Thomas ; Nordström, Jakob LU and Vinyals, Marc
- publishing date
- 2016
- type
- Chapter in Book/Report/Conference proceeding
- publication status
- published
- subject
- host publication
- Theory and Applications of Satisfiability Testing – SAT 2016 : 19th International Conference, Proceedings - 19th International Conference, Proceedings
- series title
- Lecture Notes in Computer Science
- editor
- Le Berre, Daniel and Creignou, Nadia
- volume
- 9710
- pages
- 17 pages
- publisher
- Springer
- conference name
- 19th International Conference on Theory and Applications of Satisfiability Testing, SAT 2016
- conference location
- Bordeaux, France
- conference dates
- 2016-07-05 - 2016-07-08
- external identifiers
-
- scopus:84977484096
- ISSN
- 0302-9743
- 1611-3349
- ISBN
- 9783319409696
- DOI
- 10.1007/978-3-319-40970-2_11
- language
- English
- LU publication?
- no
- id
- eb128c8f-066f-455f-b7ce-5ceff20466ad
- date added to LUP
- 2020-12-18 22:22:01
- date last changed
- 2024-02-01 13:18:02
@inproceedings{eb128c8f-066f-455f-b7ce-5ceff20466ad,
abstract = {{<p>A long line of research has studied the power of conflict- driven clause learning (CDCL) and how it compares to the resolution proof system in which it searches for proofs. It has been shown that CDCL can polynomially simulate resolution even with an adversarially chosen learning scheme as long as it is asserting. However, the simulation only works under the assumption that no learned clauses are ever forgot- ten, and the polynomial blow-up is significant. Moreover, the simulation requires very frequent restarts, whereas the power of CDCL with less frequent or entirely without restarts remains poorly understood. With a view towards obtaining results with tighter relations between CDCL and resolution, we introduce a more fine-grained model of CDCL that cap- tures not only time but also memory usage and number of restarts. We show how previously established strong size-space trade-offs for resolution can be transformed into equally strong trade-offs between time and memory usage for CDCL, where the upper bounds hold for CDCL with- out any restarts using the standard 1UIP clause learning scheme, and the (in some cases tightly matching) lower bounds hold for arbitrarily frequent restarts and arbitrary clause learning schemes.</p>}},
author = {{Elffers, Jan and Johannsen, Jan and Lauria, Massimo and Magnard, Thomas and Nordström, Jakob and Vinyals, Marc}},
booktitle = {{Theory and Applications of Satisfiability Testing – SAT 2016 : 19th International Conference, Proceedings}},
editor = {{Le Berre, Daniel and Creignou, Nadia}},
isbn = {{9783319409696}},
issn = {{0302-9743}},
language = {{eng}},
pages = {{160--176}},
publisher = {{Springer}},
series = {{Lecture Notes in Computer Science}},
title = {{Trade-offs between time and memory in a tighter model of CDCL SAT solvers}},
url = {{http://dx.doi.org/10.1007/978-3-319-40970-2_11}},
doi = {{10.1007/978-3-319-40970-2_11}},
volume = {{9710}},
year = {{2016}},
}