2 Search Results for "Iser, Markus"

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-dev.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
Short Paper
DOI: 10.4230/LIPIcs.CP.2021.6
Unit Propagation with Stable Watches (Short Paper)

Authors: Markus Iser and Tomáš Balyo

Published in: LIPIcs, Volume 210, 27th International Conference on Principles and Practice of Constraint Programming (CP 2021)

Abstract
Unit propagation is the hottest path in CDCL SAT solvers, therefore the related data-structures, algorithms and implementation details are well studied and highly optimized. State-of-the-art implementations are based on reduced occurrence tracking with two watched literals per clause and one blocking literal per watcher in order to further reduce the number of clause accesses. In this paper, we show that using runtime statistics for watched literal selection can improve the performance of state-of-the-art SAT solvers. We present a method for efficiently keeping track of spans during which literals are satisfied and using this statistic to improve watcher selection. An implementation of our method in the SAT solver CaDiCaL can solve more instances of the SAT Competition 2019 and 2020 benchmark sets and is specifically strong on satisfiable cryptographic instances.
Cite as

Markus Iser and Tomáš Balyo. Unit Propagation with Stable Watches (Short Paper). In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 6:1-6:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{iser_et_al:LIPIcs.CP.2021.6,
  author =	{Iser, Markus and Balyo, Tom\'{a}\v{s}},
  title =	{{Unit Propagation with Stable Watches}},
  booktitle =	{27th International Conference on Principles and Practice of Constraint Programming (CP 2021)},
  pages =	{6:1--6:8},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-211-2},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{210},
  editor =	{Michel, Laurent D.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2021.6},
  URN =		{urn:nbn:de:0030-drops-152973},
  doi =		{10.4230/LIPIcs.CP.2021.6},
  annote =	{Keywords: Unit Propagation, Two-Watched Literals, Literal Stability}
}
  • Refine by Author
  • 2 Iser, Markus
  • 1 Bach, Jakob
  • 1 Balyo, Tomáš
  • 1 Böhm, Klemens

  • Refine by Classification
  • 1 Computing methodologies → Supervised learning
  • 1 Theory of computation → Constraint and logic programming
  • 1 Theory of computation → Integer programming
  • 1 Theory of computation → Logic and verification

  • Refine by Keyword
  • 1 Literal Stability
  • 1 Propositional satisfiability
  • 1 Two-Watched Literals
  • 1 Unit Propagation
  • 1 integer programming
  • Show More...

  • Refine by Type
  • 2 document

  • Refine by Publication Year
  • 1 2021
  • 1 2022

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact