Search Results

Documents authored by Iser, Ashlin

Artifact
Software
DOI: 10.4230/artifacts.26969
Global Benchmark Database

Authors: Ashlin Iser and Frederick Gehm

Abstract
Cite as

Ashlin Iser, Frederick Gehm. Global Benchmark Database (Software). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@misc{dagstuhl-artifact-26969,
   title = {{Global Benchmark Database}}, 
   author = {Iser, Ashlin and Gehm, Frederick},
   note = {Software, swhId: \href{https://archive.softwareheritage.org/swh:1:dir:2553a0109d95559020fb87331f2d49502d4c4c67;origin=https://github.com/udopia/gbdc;visit=swh:1:snp:f8ee95852dcfcfd38c0eec4340954c1002a4daa7;anchor=swh:1:rev:d03875b98d3062fec717c231975a4fb5e2ebe551}{\texttt{swh:1:dir:2553a0109d95559020fb87331f2d49502d4c4c67}} (visited on 2026-07-16)},
   url = {https://github.com/udopia/gbdc},
   doi = {10.4230/artifacts.26969},
}
Document
Tool Paper
DOI: 10.4230/LIPIcs.SAT.2026.35
Efficient Identification of Isomorphic SAT Instances (Tool Paper)

Authors: Ashlin Iser and Frederick Gehm

Published in: LIPIcs, Volume 377, 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)

Abstract
Many SAT benchmark datasets contain structurally identical instances arising from repeated shuffling, generators producing identical formulas under different seeds, or duplicate encodings from different tools. We present an efficient, open-source, isomorphism-invariant hashing algorithm for SAT instances, based on Weisfeiler-Leman (WL) label refinement. Each instance is represented as a bipartite clause-literal graph, and iterative label refinement computes a canonical signature, with instances having identical signatures treated as isomorphic. When integrated into our benchmark toolset Global Benchmark Database (GBD), the method substantially reduces false positives from naive degree-sequence hashing with minimal overhead.
Cite as

Ashlin Iser and Frederick Gehm. Efficient Identification of Isomorphic SAT Instances (Tool Paper). In 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 377, pp. 35:1-35:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{iser_et_al:LIPIcs.SAT.2026.35,
  author =	{Iser, Ashlin and Gehm, Frederick},
  title =	{{Efficient Identification of Isomorphic SAT Instances}},
  booktitle =	{29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)},
  pages =	{35:1--35:8},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-431-4},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{377},
  editor =	{Ignatiev, Alexey and Szeider, Stefan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2026.35},
  URN =		{urn:nbn:de:0030-drops-263418},
  doi =		{10.4230/LIPIcs.SAT.2026.35},
  annote =	{Keywords: Isomorphism, Benchmarking, Boolean Satisfiability}
}
Document
Tool Paper
DOI: 10.4230/LIPIcs.SAT.2026.36
Sustainable Benchmarking Tool (Tool Paper)

Authors: Ashlin Iser, Marie Anastacio, Théo Matricon, Laurent Simon, and Holger H. Hoos

Published in: LIPIcs, Volume 377, 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)

Abstract
Solvers for NP-hard problems from areas such as automated reasoning or optimisation are complex systems in which many different components interact. The performance of these solvers is the result of an intricate interplay between implementation details, algorithmic concepts and heuristics. This, alongside the complexity of the problem instances to be solved, makes it challenging to assess the effect of a single idea on the overall performance of a given solver. It is therefore not only crucial, but also challenging to evaluate the performance impact of new ideas. Existing reliable evaluation methods require large sets of diverse benchmark instances and considerable amounts of computing resources. This makes empirical evaluation a bottleneck for solver development, as it is time-consuming and energy-intensive, often requiring several CPU years of computation to evaluate the impact of a single idea. In recent years, this bottleneck has led to the development of data-driven approaches that can dynamically select a smaller number of instances that provide sufficient statistical evidence to evaluate the relative performance of a given set of solvers. However, these methods are typically not easily accessible. In this work, we present a tool that implements these methods and makes them readily accessible to solver developers, thus enabling them to obtain swifter feedback on their ideas.
Cite as

Ashlin Iser, Marie Anastacio, Théo Matricon, Laurent Simon, and Holger H. Hoos. Sustainable Benchmarking Tool (Tool Paper). In 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 377, pp. 36:1-36:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{iser_et_al:LIPIcs.SAT.2026.36,
  author =	{Iser, Ashlin and Anastacio, Marie and Matricon, Th\'{e}o and Simon, Laurent and Hoos, Holger H.},
  title =	{{Sustainable Benchmarking Tool}},
  booktitle =	{29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)},
  pages =	{36:1--36:12},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-431-4},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{377},
  editor =	{Ignatiev, Alexey and Szeider, Stefan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2026.36},
  URN =		{urn:nbn:de:0030-drops-263427},
  doi =		{10.4230/LIPIcs.SAT.2026.36},
  annote =	{Keywords: Sustainability, Empirical performance comparison, Benchmarking, Problem instance selection}
}
Artifact
Software
DOI: 10.4230/artifacts.22456
Global Benchmark Database

Authors: Ashlin Iser and Christoph Jabs

Abstract
Cite as

Ashlin Iser, Christoph Jabs. Global Benchmark Database (Software, GBD Source Code). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@misc{dagstuhl-artifact-22456,
   title = {{Global Benchmark Database}}, 
   author = {Iser, Ashlin and Jabs, Christoph},
   note = {Software, version 4.8.5., swhId: \href{https://archive.softwareheritage.org/swh:1:dir:37fb54c7420fd71b6c4930bcf7e78d5129325a6d;origin=https://github.com/Udopia/gbd;visit=swh:1:snp:2ac08f4b21c50b3e1afa06cdf1c124f23032a3ee;anchor=swh:1:rev:d046347f76eab17038205b3485b0dec83d90860f}{\texttt{swh:1:dir:37fb54c7420fd71b6c4930bcf7e78d5129325a6d}} (visited on 2026-01-26)},
   url = {https://github.com/Udopia/gbd},
   doi = {10.4230/artifacts.22456},
}
Artifact
Software
DOI: 10.4230/artifacts.22457
Global Benchmark Database (Extension Module)

Authors: Ashlin Iser and Christoph Jabs

Abstract
Cite as

Ashlin Iser, Christoph Jabs. Global Benchmark Database (Extension Module) (Software). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@misc{dagstuhl-artifact-22457,
   title = {{Global Benchmark Database (Extension Module)}}, 
   author = {Iser, Ashlin and Jabs, Christoph},
   note = {Software, version 1.0., swhId: \href{https://archive.softwareheritage.org/swh:1:dir:705258b1bd5c3415069fbd156759945a8ad725c0;origin=https://github.com/Udopia/gbdc;visit=swh:1:snp:23f6abd3b9d7389152ed319b2671f16df2071c42;anchor=swh:1:rev:7b6183a29cca2316e7b5b6801d9cc0c86b3ed404}{\texttt{swh:1:dir:705258b1bd5c3415069fbd156759945a8ad725c0}} (visited on 2026-01-26)},
   url = {https://github.com/Udopia/gbdc},
   doi = {10.4230/artifacts.22457},
}
Artifact
Software
DOI: 10.4230/artifacts.22458
GBD Evaluation Scripts

Authors: Ashlin Iser and Christoph Jabs

Abstract
Cite as

Ashlin Iser, Christoph Jabs. GBD Evaluation Scripts (Software). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@misc{dagstuhl-artifact-22458,
   title = {{GBD Evaluation Scripts}}, 
   author = {Iser, Ashlin and Jabs, Christoph},
   note = {Software, version 1.0., swhId: \href{https://archive.softwareheritage.org/swh:1:dir:159fae7ac54d9f678ee38ed882dae693cd5f14cf;origin=https://github.com/Udopia/gbdeval;visit=swh:1:snp:0ca8e899579d511367cf2981a5da9ff656f6577d;anchor=swh:1:rev:1db61d77d84d5e54ad5cedd66cd15f9334212875}{\texttt{swh:1:dir:159fae7ac54d9f678ee38ed882dae693cd5f14cf}} (visited on 2026-01-26)},
   url = {https://github.com/Udopia/gbdeval},
   doi = {10.4230/artifacts.22458},
}
Artifact
Dataset
DOI: 10.4230/artifacts.22459
GBD Data Repository

Authors: Ashlin Iser and Christoph Jabs

Abstract
Cite as

Ashlin Iser, Christoph Jabs. GBD Data Repository (Dataset). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@misc{dagstuhl-artifact-22459,
   title = {{GBD Data Repository}}, 
   author = {Iser, Ashlin and Jabs, Christoph},
   note = {Dataset, version 1.0., swhId: \href{https://archive.softwareheritage.org/swh:1:dir:1764eef19455a0bfdb6389a04a055977338304ff;origin=https://github.com/Udopia/gbd-data;visit=swh:1:snp:c94e9ddcf3108d147a440520e71697d5a7526095;anchor=swh:1:rev:609f64f7d8335d50aca9f4713afcce3e81bf09b2}{\texttt{swh:1:dir:1764eef19455a0bfdb6389a04a055977338304ff}} (visited on 2026-01-26)},
   url = {https://github.com/Udopia/gbd-data},
   doi = {10.4230/artifacts.22459},
}
Document
DOI: 10.4230/LIPIcs.SAT.2024.18
Global Benchmark Database

Authors: Ashlin Iser and Christoph Jabs

Published in: LIPIcs, Volume 305, 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)

Abstract
This paper presents Global Benchmark Database (GBD), a comprehensive suite of tools for provisioning and sustainably maintaining benchmark instances and their metadata. The availability of benchmark metadata is essential for many tasks in empirical research, e.g., for the data-driven compilation of benchmarks, the domain-specific analysis of runtime experiments, or the instance-specific selection of solvers. In this paper, we introduce the data model of GBD as well as its interfaces and provide examples of how to interact with them. We also demonstrate the integration of custom data sources and explain how to extend GBD with additional problem domains, instance formats and feature extractors.
Cite as

Ashlin Iser and Christoph Jabs. Global Benchmark Database. In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, pp. 18:1-18:10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{iser_et_al:LIPIcs.SAT.2024.18,
  author =	{Iser, Ashlin and Jabs, Christoph},
  title =	{{Global Benchmark Database}},
  booktitle =	{27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)},
  pages =	{18:1--18:10},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-334-8},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{305},
  editor =	{Chakraborty, Supratik and Jiang, Jie-Hong Roland},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2024.18},
  URN =		{urn:nbn:de:0030-drops-205405},
  doi =		{10.4230/LIPIcs.SAT.2024.18},
  annote =	{Keywords: Maintenance and Distribution of Benchmark Instances and their Features}
}
Document
DOI: 10.4230/LIPIcs.SAT.2022.2
A Comprehensive Study of k-Portfolios of Recent SAT Solvers

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

Authors: Ashlin 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

Ashlin 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, Ashlin 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.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}
}
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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