Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Trade-offs between time and memory in a tighter model of CDCL SAT solvers
KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
Show others and affiliations
2016 (English)In: 19th International Conference on Theory and Applications of Satisfiability Testing, SAT 2016, Springer, 2016, 160-176 p.Conference paper, Published paper (Refereed)
Abstract [en]

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.

Place, publisher, year, edition, pages
Springer, 2016. 160-176 p.
Keyword [en]
Commerce, Formal logic, Clause learning, Fine grained, Learning schemes, Lower bounds, Memory usage, Resolution proofs, SAT solvers, Upper Bound, Economic and social effects
National Category
Computer Science
Identifiers
URN: urn:nbn:se:kth:diva-195488DOI: 10.1007/978-3-319-40970-2_11ISI: 000387430600011Scopus ID: 2-s2.0-84977484096ISBN: 9783319409696 (print)OAI: oai:DiVA.org:kth-195488DiVA: diva2:1047764
Conference
5 July 2016 through 8 July 2016
Note

QC 20161118

Available from: 2016-11-18 Created: 2016-11-03 Last updated: 2017-05-09Bibliographically approved
In thesis
1. Space in Proof Complexity
Open this publication in new window or tab >>Space in Proof Complexity
2017 (English)Doctoral thesis, comprehensive summary (Other academic)
Abstract [en]

ropositional proof complexity is the study of the resources that are needed to prove formulas in propositional logic. In this thesis we are concerned with the size and space of proofs, and in particular with the latter.

Different approaches to reasoning are captured by corresponding proof systems. The simplest and most well studied proof system is resolution, and we try to get our understanding of other proof systems closer to that of resolution.

In resolution we can prove a space lower bound just by showing that any proof must have a large clause. We prove a similar relation between resolution width and polynomial calculus space that lets us derive space lower bounds, and we use it to separate degree and space.

For cutting planes we show length-space trade-offs. This is, there are formulas that have a proof in small space and a proof in small length, but there is no proof that can optimize both measures at the same time.

We introduce a new measure of space, cumulative space, that accounts for the space used throughout a proof rather than only its maximum. This is exploratory work, but we can also prove new results for the usual space measure.

We define a new proof system that aims to capture the power of current SAT solvers, and we show a landscape of length-space trade-offs comparable to those in resolution.

To prove these results we build and use tools from other areas of computational complexity. One area is pebble games, very simple computational models that are useful for modelling space. In addition to results with applications to proof complexity, we show that pebble game cost is PSPACE-hard to approximate.

Another area is communication complexity, the study of the amount of communication that is needed to solve a problem when its description is shared by multiple parties. We prove a simulation theorem that relates the query complexity of a function with the communication complexity of a composed function.

Place, publisher, year, edition, pages
Stockholm: KTH Royal Institute of Technology, 2017. 318 p.
Series
TRITA-CSC-A, ISSN 1653-5723 ; 2017:15
Keyword
proof complexity, resolution, polynomial calculus, cutting planes, space complexity, computational complexity, pebble games, communication complexity, CDCL
National Category
Computer Science
Research subject
Computer Science
Identifiers
urn:nbn:se:kth:diva-206571 (URN)978-91-7729-422-1 (ISBN)
Public defence
2017-06-09, E2, Lindstedtsvägen, 3, Stockholm, 14:00 (English)
Opponent
Supervisors
Funder
EU, FP7, Seventh Framework Programme, 279611
Note

QC 20170509

Available from: 2017-05-10 Created: 2017-05-09 Last updated: 2017-05-10Bibliographically approved

Open Access in DiVA

No full text

Other links

Publisher's full textScopus

Search in DiVA

By author/editor
Elffers, JanNordström, JakobVinyals, Marc
By organisation
Theoretical Computer Science, TCS
Computer Science

Search outside of DiVA

GoogleGoogle Scholar

Altmetric score

Total: 1639 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf