kth.sePublications
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • 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
Structure features for SAT instances classification
KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS. Spanish National Research Council, Spain.
2017 (English)In: Journal of Applied Logic, ISSN 1570-8683, E-ISSN 1570-8691, Vol. 23, p. 27-39Article in journal (Refereed) 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.

Place, publisher, year, edition, pages
Elsevier, 2017. Vol. 23, p. 27-39
Keywords [en]
SAT solving, Complex networks, Classifiers, Portfolio
National Category
Bioinformatics (Computational Biology)
Identifiers
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
Note

QC 20170821

Available from: 2017-08-21 Created: 2017-08-21 Last updated: 2024-03-15Bibliographically approved

Open Access in DiVA

No full text in DiVA

Other links

Publisher's full textScopus

Authority records

Giraldez-Cru, Jesus

Search in DiVA

By author/editor
Giraldez-Cru, Jesus
By organisation
Theoretical Computer Science, TCS
In the same journal
Journal of Applied Logic
Bioinformatics (Computational Biology)

Search outside of DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetric score

doi
urn-nbn
Total: 609 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • 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