KIT | KIT-Bibliothek | Impressum | Datenschutz

A Comprehensive Study of k-Portfolios of Recent SAT Solvers

Bach, Jakob ORCID iD icon 1; Iser, Markus 2; Böhm, Klemens 1
1 Institut für Programmstrukturen und Datenorganisation (IPD), Karlsruher Institut für Technologie (KIT)
2 Institut für Informationssicherheit und Verlässlichkeit (KASTEL), Karlsruher Institut für Technologie (KIT)

Abstract:

Hard combinatorial problems such as propositional satisfiability are ubiquitous. The holy grail are solution methods that show good performance on all problem instances. However, new approaches emerge regularly, some of which are complementary to existing solvers in that they only run faster on some instances but not on many others. While portfolios, i.e., sets of solvers, have been touted as useful, putting together such portfolios also needs to be efficient. In particular, it remains an open question how well portfolios can exploit the complementarity of solvers. This paper features a comprehensive analysis of portfolios of recent SAT solvers, the ones from the SAT Competitions 2020 and 2021. We determine optimal portfolios with exact and approximate approaches and study the impact of portfolio size k on performance. We also investigate how effective off-the-shelf prediction models are for instance-specific solver recommendations. One result is that the portfolios found with an approximate approach are as good as the optimal solution in practice. We also observe that marginal returns decrease very quickly with larger k, and our prediction models do not give way to better performance beyond very small portfolio sizes.


Verlagsausgabe §
DOI: 10.5445/IR/1000149302
Veröffentlicht am 01.08.2022
Originalveröffentlichung
DOI: 10.4230/LIPIcs.SAT.2022.2
Scopus
Zitationen: 1
Cover der Publikation
Zugehörige Institution(en) am KIT Institut für Informationssicherheit und Verlässlichkeit (KASTEL)
Institut für Programmstrukturen und Datenorganisation (IPD)
Publikationstyp Proceedingsbeitrag
Publikationsdatum 28.07.2022
Sprache Englisch
Identifikator ISBN: 978-3-9597724-2-6
ISSN: 1868-8969
KITopen-ID: 1000149302
Erschienen in 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Hrsg.: Kuldeep S. Meel
Veranstaltung 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022), Haifa, Israel, 02.08.2022 – 05.08.2022
Verlag Schloss Dagstuhl - Leibniz-Zentrum für Informatik (LZI)
Seiten 2:1–2:18
Serie Leibniz International Proceedings in Informatics (LIPIcs) ; 236
Externe Relationen Abstract/Volltext
Schlagwörter Propositional satisfiability, solver portfolios, runtime prediction, machine learning, integer programming
Nachgewiesen in Scopus
Relationen in KITopen
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft
KITopen Landing Page