DROPS

Document

DOI: 10.4230/LIPIcs.SAT.2022.2

A Comprehensive Study of k-Portfolios of Recent SAT Solvers

Authors: Jakob Bach, Markus Iser, and Klemens Böhm

Published in: LIPIcs, Volume 236, 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)

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.

Cite as

Jakob Bach, Markus Iser, and Klemens Böhm. A Comprehensive Study of k-Portfolios of Recent SAT Solvers. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 2:1-2:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@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/entities/document/10.4230/LIPIcs.SAT.2022.2},
  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}
}

Document

DOI: 10.4230/DagSemProc.04391.21

Summary of the Results of the Break-out Session "Social Issues around the Semantic Web"

Authors: Karl Aberer, Klemens Böhm, and Fred Fonseca

Published in: Dagstuhl Seminar Proceedings, Volume 4391, Semantic Interoperability and Integration (2005)

Abstract

As part of the Dagstuhl Workshop on the Semantic Web, a break-out session focused on discussing social issues around the Semantic Web. This article is a concise summary of the main issues discussed, the controversies that have arisen, and of the open research questions that need to be addressed.

Cite as

Karl Aberer, Klemens Böhm, and Fred Fonseca. Summary of the Results of the Break-out Session "Social Issues around the Semantic Web". In Semantic Interoperability and Integration. Dagstuhl Seminar Proceedings, Volume 4391, pp. 1-4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2005)

Copy BibTex To Clipboard

@InProceedings{aberer_et_al:DagSemProc.04391.21,
  author =	{Aberer, Karl and B\"{o}hm, Klemens and Fonseca, Fred},
  title =	{{Summary of the Results of the Break-out Session "Social Issues around the Semantic Web"}},
  booktitle =	{Semantic Interoperability and Integration},
  pages =	{1--4},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2005},
  volume =	{4391},
  editor =	{Y. Kalfoglou and M. Schorlemmer and A. Sheth and S. Staab and M. Uschold},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.04391.21},
  URN =		{urn:nbn:de:0030-drops-337},
  doi =		{10.4230/DagSemProc.04391.21},
  annote =	{Keywords: semantic web , social issues}
}

Search Results

Documents authored by Böhm, Klemens

A Comprehensive Study of k-Portfolios of Recent SAT Solvers

Abstract

Cite as

Summary of the Results of the Break-out Session "Social Issues around the Semantic Web"

Abstract

Cite as

Thanks for your feedback!

Could not send message