Ändra sökning
RefereraExporteraLänk till posten
Permanent länk

Direktlänk
Referera
Referensformat
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat 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 (Engelska)Ingår i: 20th International Conference on Theory and Applications of Satisfiability Testing, SAT 2017, Springer, 2017, Vol. 10491, s. 65-82Konferensbidrag (Refereegranskat)
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.

Ort, förlag, år, upplaga, sidor
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
Nationell ämneskategori
Datavetenskap (datalogi)
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
Konferens
20th International Conference on Theory and Applications of Satisfiability Testing, SAT 2017, Melbourne, Australia, 28 August 2017 through 1 September 2017
Forskningsfinansiär
EU, Europeiska forskningsrådetEU, FP7, Sjunde ramprogrammet, FP7/2007-2013
Anmärkning

QC 20170919

Tillgänglig från: 2017-09-19 Skapad: 2017-09-19 Senast uppdaterad: 2019-10-17Bibliografiskt granskad

Open Access i DiVA

Fulltext saknas i DiVA

Övriga länkar

Förlagets fulltextScopus

Sök vidare i DiVA

Av författaren/redaktören
Giráldez-Cru, Jesús
Av organisationen
Teoretisk datalogi, TCS
Datavetenskap (datalogi)

Sök vidare utanför DiVA

GoogleGoogle Scholar

doi
isbn
urn-nbn

Altmetricpoäng

doi
isbn
urn-nbn
Totalt: 17 träffar
RefereraExporteraLänk till posten
Permanent länk

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