Endre søk
RefereraExporteraLink to record
Permanent link

Direct link
Referera
Referensformat
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annet format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annet språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf
On the community structure of bounded model checking SAT problems
KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS.
2017 (engelsk)Inngår i: 20th International Conference on Theory and Applications of Satisfiability Testing, SAT 2017, Springer, 2017, Vol. 10491, s. 65-82Konferansepaper (Fagfellevurdert)
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.

sted, utgiver, år, opplag, sider
Springer, 2017. Vol. 10491, s. 65-82
Serie
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), ISSN 0302-9743 ; 10491
HSV kategori
Identifikatorer
URN: urn:nbn:se:kth:diva-214648DOI: 10.1007/978-3-319-66263-3_5ISI: 000455337600005Scopus ID: 2-s2.0-85028729996ISBN: 9783319662626 (tryckt)OAI: oai:DiVA.org:kth-214648DiVA, id: diva2:1142526
Konferanse
20th International Conference on Theory and Applications of Satisfiability Testing, SAT 2017, Melbourne, Australia, 28 August 2017 through 1 September 2017
Forskningsfinansiär
EU, European Research CouncilEU, FP7, Seventh Framework Programme, FP7/2007-2013
Merknad

QC 20170919

Tilgjengelig fra: 2017-09-19 Laget: 2017-09-19 Sist oppdatert: 2019-10-17bibliografisk kontrollert

Open Access i DiVA

Fulltekst mangler i DiVA

Andre lenker

Forlagets fulltekstScopus

Søk i DiVA

Av forfatter/redaktør
Giráldez-Cru, Jesús
Av organisasjonen

Søk utenfor DiVA

GoogleGoogle Scholar

doi
isbn
urn-nbn

Altmetric

doi
isbn
urn-nbn
Totalt: 17 treff
RefereraExporteraLink to record
Permanent link

Direct link
Referera
Referensformat
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annet format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annet språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf