License: 
Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.SAT.2022.2
URN: urn:nbn:de:0030-drops-166767
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2022/16676/
Bach, Jakob ;
Iser, Markus ;
Böhm, Klemens
A Comprehensive Study of k-Portfolios of Recent SAT Solvers
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.
BibTeX - Entry
@InProceedings{bach_et_al:LIPIcs.SAT.2022.2,
author = {Bach, Jakob and Iser, Markus and B\"{o}hm, Klemens},
title = {{A Comprehensive Study of k-Portfolios of Recent SAT Solvers}},
booktitle = {25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
pages = {2:1--2:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-242-6},
ISSN = {1868-8969},
year = {2022},
volume = {236},
editor = {Meel, Kuldeep S. and Strichman, Ofer},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2022/16676},
URN = {urn:nbn:de:0030-drops-166767},
doi = {10.4230/LIPIcs.SAT.2022.2},
annote = {Keywords: Propositional satisfiability, solver portfolios, runtime prediction, machine learning, integer programming}
}
