4 Search Results for "Iser, Markus"

Document

DOI: 10.4230/LIPIcs.SEA.2024.26

Scalable Hard Instances for Independent Set Reconfiguration

Authors: Takehide Soh, Takumu Watanabe, Jun Kawahara, Akira Suzuki, and Takehiro Ito

Published in: LIPIcs, Volume 301, 22nd International Symposium on Experimental Algorithms (SEA 2024)

Abstract

The Token Jumping problem, also known as the independent set reconfiguration problem under the token jumping model, is defined as follows: Given a graph and two same-sized independent sets, determine whether one can be transformed into the other via a sequence of independent sets. Token Jumping has been extensively studied, mainly from the viewpoint of algorithmic theory, but its practical study has just begun. To develop a practically good solver, it is important to construct benchmark datasets that are scalable and hard. Here, "scalable" means the ability to change the scale of the instance while maintaining its characteristics by adjusting the given parameters; and "hard" means that the instance can become so difficult that it cannot be solved within a practical time frame by a solver. In this paper, we propose four types of instance series for Token Jumping. Our instance series is scalable in the sense that instance scales are controlled by the number of vertices. To establish their hardness, we focus on the numbers of transformation steps; our instance series requires exponential numbers of steps with respect to the number of vertices. Interestingly, three types of instance series are constructed by importing theories developed by algorithmic research. We experimentally evaluate the scalability and hardness of the proposed instance series, using the SAT solver and award-winning solvers of the international competition for Token Jumping.

Cite as

Takehide Soh, Takumu Watanabe, Jun Kawahara, Akira Suzuki, and Takehiro Ito. Scalable Hard Instances for Independent Set Reconfiguration. In 22nd International Symposium on Experimental Algorithms (SEA 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 301, pp. 26:1-26:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{soh_et_al:LIPIcs.SEA.2024.26,
  author =	{Soh, Takehide and Watanabe, Takumu and Kawahara, Jun and Suzuki, Akira and Ito, Takehiro},
  title =	{{Scalable Hard Instances for Independent Set Reconfiguration}},
  booktitle =	{22nd International Symposium on Experimental Algorithms (SEA 2024)},
  pages =	{26:1--26:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-325-6},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{301},
  editor =	{Liberti, Leo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SEA.2024.26},
  URN =		{urn:nbn:de:0030-drops-203913},
  doi =		{10.4230/LIPIcs.SEA.2024.26},
  annote =	{Keywords: Combinatorial reconfiguration, Benckmark dataset, Graph Algorithm, PSPACE-complete}
}

Document

DOI: 10.4230/LIPIcs.FSCD.2024.27

A Verified Algorithm for Deciding Pattern Completeness

Authors: René Thiemann and Akihisa Yamada

Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)

Abstract

Pattern completeness is the property that the left-hand sides of a functional program cover all cases w.r.t. pattern matching. In the context of term rewriting a related notion is quasi-reducibility, a prerequisite if one wants to perform ground confluence proofs by rewriting induction. In order to certify such confluence proofs, we develop a novel algorithm that decides pattern completeness and that can be used to ensure quasi-reducibility. One of the advantages of the proposed algorithm is its simple structure: it is similar to that of a regular matching algorithm and, unlike an existing decision procedure for quasi-reducibility, it avoids enumerating all terms up to a given depth. Despite the simple structure, proving the correctness of the algorithm is not immediate. Therefore we formalize the algorithm and verify its correctness using the proof assistant Isabelle/HOL. To this end, we not only verify some auxiliary algorithms, but also design an Isabelle library on sorted term rewriting. Moreover, we export the verified code in Haskell and experimentally evaluate its performance. We observe that our algorithm significantly outperforms existing algorithms, even including the pattern completeness check of the GHC Haskell compiler.

Cite as

René Thiemann and Akihisa Yamada. A Verified Algorithm for Deciding Pattern Completeness. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 27:1-27:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{thiemann_et_al:LIPIcs.FSCD.2024.27,
  author =	{Thiemann, Ren\'{e} and Yamada, Akihisa},
  title =	{{A Verified Algorithm for Deciding Pattern Completeness}},
  booktitle =	{9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)},
  pages =	{27:1--27:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-323-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{299},
  editor =	{Rehof, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.27},
  URN =		{urn:nbn:de:0030-drops-203566},
  doi =		{10.4230/LIPIcs.FSCD.2024.27},
  annote =	{Keywords: Isabelle/HOL, pattern matching, term rewriting}
}

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

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.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
1 Ito, Takehiro
Show More...

Refine by Classification
1 Computing methodologies → Discrete space search
1 Computing methodologies → Supervised learning
1 Theory of computation → Constraint and logic programming
1 Theory of computation → Higher order logic
1 Theory of computation → Integer programming
Show More...

Refine by Keyword
1 Benckmark dataset
1 Combinatorial reconfiguration
1 Graph Algorithm
1 Isabelle/HOL
1 Literal Stability
Show More...

Refine by Type
4 document

Refine by Publication Year
2 2024
1 2021
1 2022