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
Structure features for SAT instances classification
KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS. Spanish National Research Council, Spain.
2017 (engelsk)Inngår i: Journal of Applied Logic, ISSN 1570-8683, E-ISSN 1570-8691, Vol. 23, s. 27-39Artikkel i tidsskrift (Fagfellevurdert) Published
Abstract [en]

The success of portfolio approaches in SAT solving relies on the observation that different SAT solvers may dramatically change their performance depending on the class of SAT instances they are trying to solve. In these approaches, a set of features of the problem is used to build a prediction model, which classifies instances into classes, and computes the fastest algorithm to solve each of them. Therefore, the set of features used to build these classifiers plays a crucial role. Traditionally, portfolio SAT solvers include features about the structure of the problem and its hardness. Recently, there have been some attempts to better characterize the structure of industrial SAT instances. In this paper, we use some structure features of industrial SAT instances to build some classifiers of industrial SAT families of instances. Namely, they are the scale-free structure, the community structure and the self similar structure. First, we measure the effectiveness of these classifiers by comparing them to other sets of SAT features commonly used in portfolio SAT solving approaches. Then, we evaluate the performance of this set of structure features when used in a real portfolio SAT solver. Finally, we analyze the relevance of these features on the analyzed classifiers.

sted, utgiver, år, opplag, sider
Elsevier, 2017. Vol. 23, s. 27-39
Emneord [en]
SAT solving, Complex networks, Classifiers, Portfolio
HSV kategori
Identifikatorer
URN: urn:nbn:se:kth:diva-212327DOI: 10.1016/j.jal.2016.11.004ISI: 000406728700004Scopus ID: 2-s2.0-85006968223OAI: oai:DiVA.org:kth-212327DiVA, id: diva2:1134708
Merknad

QC 20170821

Tilgjengelig fra: 2017-08-21 Laget: 2017-08-21 Sist oppdatert: 2018-01-13bibliografisk kontrollert

Open Access i DiVA

Fulltekst mangler i DiVA

Andre lenker

Forlagets fulltekstScopus

Søk i DiVA

Av forfatter/redaktør
Giraldez-Cru, Jesus
Av organisasjonen
I samme tidsskrift
Journal of Applied Logic

Søk utenfor DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetric

doi
urn-nbn
Totalt: 492 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