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
On the community structure of bounded model checking SAT problems
KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
2017 (English)In: 20th International Conference on Theory and Applications of Satisfiability Testing, SAT 2017, Springer, 2017, Vol. 10491, p. 65-82Conference paper (Refereed)
Abstract [en]

Following the impressive progress made in the quest for efficient SAT solving in the last years, a number of researches has focused on explaining performances observed on typical application problems. However, until now, tentative explanations were only partial, essentially because the semantic of the original problem was lost in the translation to SAT. In this work, we study the behavior of so called “modern” SAT solvers under the prism of the first successful application of CDCL solvers, i.e., Bounded Model Checking. We trace the origin of each variable w.r.t. its unrolling depth, and show a surprising relationship between these time steps and the communities found in the CNF encoding. We also show how the VSIDS heuristic, the resolution engine, and the learning mechanism interact with the unrolling steps. Additionally, we show that the Literal Block Distance (LBD), used to identify good learnt clauses, is related to this measure. Our work shows that communities identify strong dependencies among the variables of different time steps, revealing a structure that arises when unrolling the problem, and which seems to be caught by the LBD measure.

Place, publisher, year, edition, pages
Springer, 2017. Vol. 10491, p. 65-82
Series
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), ISSN 0302-9743 ; 10491
National Category
Computer Sciences
Identifiers
URN: urn:nbn:se:kth:diva-214648DOI: 10.1007/978-3-319-66263-3_5Scopus ID: 2-s2.0-85028729996ISBN: 9783319662626 (print)OAI: oai:DiVA.org:kth-214648DiVA, id: diva2:1142526
Conference
20th International Conference on Theory and Applications of Satisfiability Testing, SAT 2017, Melbourne, Australia, 28 August 2017 through 1 September 2017
Funder
EU, European Research CouncilEU, FP7, Seventh Framework Programme, FP7/2007-2013
Note

QC 20170919

Available from: 2017-09-19 Created: 2017-09-19 Last updated: 2018-01-13Bibliographically approved

Open Access in DiVA

No full text in DiVA

Other links

Publisher's full textScopus

Search in DiVA

By author/editor
Giráldez-Cru, Jesús
By organisation
Theoretical Computer Science, TCS
Computer Sciences

Search outside of DiVA

GoogleGoogle Scholar

doi
isbn
urn-nbn

Altmetric score

doi
isbn
urn-nbn
Total: 12 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