21 Search Results for "Hoos, Holger"

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}
}
Document
DOI: 10.4230/LIPIcs.IPEC.2025.32
The PACE 2025 Parameterized Algorithms and Computational Experiments Challenge: Dominating Set and Hitting Set

Authors: Mario Grobler and Sebastian Siebertz

Published in: LIPIcs, Volume 358, 20th International Symposium on Parameterized and Exact Computation (IPEC 2025)

Abstract
The 10th iteration of the of the Parameterized Algorithms and Computational Experiments challenge (PACE) 2025 was devoted to engineer algorithms solving the Dominating Set problem as well as the Hitting Set problem. In contrast to the last iterations, these problems are (under standard assumptions) not fixed-parameter tractable (fpt) in general. However, restricting the structure of the input (e.g. to planar graphs or degenerate graphs for Dominating Set, or to set systems with sets of bounded size for Hitting Set) renders these problems fpt. Following the spirit of the last iterations of the PACE challenge, there is an exact track and a heuristic track for each problem; each track coming with a benchmark set of 100 public instances and 100 private instances. Overall, the PACE 2025 had 71 participants from 25 teams, 13 countries, and 3 continents. In this report, we briefly describe the setup of the challenge, the selection of benchmark instances, as well as the ranking of the participating teams. We also briefly outline the approaches used in the submitted solvers.
Cite as

Mario Grobler and Sebastian Siebertz. The PACE 2025 Parameterized Algorithms and Computational Experiments Challenge: Dominating Set and Hitting Set. In 20th International Symposium on Parameterized and Exact Computation (IPEC 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 358, pp. 32:1-32:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{grobler_et_al:LIPIcs.IPEC.2025.32,
  author =	{Grobler, Mario and Siebertz, Sebastian},
  title =	{{The PACE 2025 Parameterized Algorithms and Computational Experiments Challenge: Dominating Set and Hitting Set}},
  booktitle =	{20th International Symposium on Parameterized and Exact Computation (IPEC 2025)},
  pages =	{32:1--32:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-407-9},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{358},
  editor =	{Agrawal, Akanksha and van Leeuwen, Erik Jan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.IPEC.2025.32},
  URN =		{urn:nbn:de:0030-drops-251644},
  doi =		{10.4230/LIPIcs.IPEC.2025.32},
  annote =	{Keywords: PACE 2025 Report, Dominating Set, Hitting Set, Algorithm Engineering, FPT, Heuristics}
}
Document
DOI: 10.4230/LIPIcs.WADS.2025.32
Fantastic Flips and Where to Find Them: A General Framework for Parameterized Local Search on Partitioning Problems

Authors: Niels Grüttemeier, Nils Morawietz, and Frank Sommer

Published in: LIPIcs, Volume 349, 19th International Symposium on Algorithms and Data Structures (WADS 2025)

Abstract
Parameterized local search combines classic local search heuristics with the paradigm of parameterized algorithmics. While most local search algorithms aim to improve given solutions by performing one single operation on a given solution, the parameterized approach aims to improve a solution by performing k simultaneous operations. Herein, k is a parameter called search radius for which the value can be chosen by a user. One major goal in the field of parameterized local search is to outline the trade-off between the size of k and the running time of the local search step. In this work, we introduce an abstract framework that generalizes natural parameterized local search approaches for a large class of partitioning problems: Given n items that are partitioned into b bins and a target function that evaluates the quality of the current partition, one asks whether it is possible to improve the solution by removing up to k items from their current bins and reassigning them to other bins. Among others, our framework applies for the local search versions of problems like Cluster Editing, Vector Bin Packing, and Nash Social Welfare. Motivated by a real-world application of the problem Vector Bin Packing, we introduce a parameter called number of types τ ≤ n and show that all problems fitting in our framework can be solved in τ^k ⋅ 2^𝒪(k) ⋅ |I|^𝒪(1) time, where |I| denotes the total input size. In case of Cluster Editing, the parameter τ generalizes the well-known parameter neighborhood diversity of the input graph. We complement these algorithms by showing that for all considered problems, an algorithm significantly improving over our algorithm with running time τ^k ⋅ 2^𝒪(k) ⋅ |I|^𝒪(1) would contradict the Exponential Time Hypothesis. Additionally, we show that even on very restricted instances, all considered problems are W[1]-hard when parameterized by the search radius k alone. In case of the local search version of Vector Bin Packing, we provide an even stronger W[1]-hardness result.
Cite as

Niels Grüttemeier, Nils Morawietz, and Frank Sommer. Fantastic Flips and Where to Find Them: A General Framework for Parameterized Local Search on Partitioning Problems. In 19th International Symposium on Algorithms and Data Structures (WADS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 349, pp. 32:1-32:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{gruttemeier_et_al:LIPIcs.WADS.2025.32,
  author =	{Gr\"{u}ttemeier, Niels and Morawietz, Nils and Sommer, Frank},
  title =	{{Fantastic Flips and Where to Find Them: A General Framework for Parameterized Local Search on Partitioning Problems}},
  booktitle =	{19th International Symposium on Algorithms and Data Structures (WADS 2025)},
  pages =	{32:1--32:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-398-0},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{349},
  editor =	{Morin, Pat and Oh, Eunjin},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.WADS.2025.32},
  URN =		{urn:nbn:de:0030-drops-242631},
  doi =		{10.4230/LIPIcs.WADS.2025.32},
  annote =	{Keywords: Flip-Neighborhood, Cluster Editing, Vector Bin Packing, Vertex Cover, NP-hard problem, Max c-Cut}
}
Document
DOI: 10.4230/LIPIcs.WABI.2025.13
Spark: Sparsified Hierarchical Energy Minimization of RNA Pseudoknots

Authors: Mateo Gray, Sebastian Will, and Hosna Jabbari

Published in: LIPIcs, Volume 344, 25th International Conference on Algorithms for Bioinformatics (WABI 2025)

Abstract
Motivation. Determining RNA structure is essential for understanding RNA function and interaction networks. Although experimental techniques yield high‑accuracy structures, they are costly and time‑consuming; thus, computational approaches - especially minimum‑free‑energy (MFE) prediction algorithms - are indispensable. Accurately predicting pseudoknots, however, remains challenging because their inclusion usually leads to prohibitive computational complexity. Recent work demonstrated that sparsification can improve the efficiency of complex pseudoknot prediction algorithms such as Knotty. This finding suggests similar gains are possible for already efficient algorithms like HFold, which targets a complementary class of hierarchically constrained pseudoknots. Results. We introduce Spark, an exact, fully sparsified algorithm for predicting pseudoknotted RNA structures. Like its non‑sparsified predecessor HFold, Spark searches for the minimum‑energy structure under the HotKots 2.0 energy model, a pseudoknot extension of the Turner model. Because the sparsification is non‑heuristic, Spark preserves the asymptotic time‑ and space‑complexity guarantees of HFold while greatly reducing the constant factors. We benchmarked the performance of Spark against HFold and, as a pseudoknot‑free baseline, RNAfold. Compared with HFold, Spark substantially lowers both run time and memory usage, while achieving run‑time figures close to those of RNAfold. Across all tested sequence lengths, Spark used the least memory and consistently ran faster than HFold. Conclusion. By extending non‑heuristic sparsification to hierarchical pseudoknot prediction, Spark delivers an exceptionally fast and memory‑efficient tool accurate prediction of pseudoknotted RNA structures, enabling routine analysis of long sequences. The algorithm broadens the practical scope of computational RNA biology and provides a solid foundation for future advances in structure‑based functional annotation. Availability. Spark’s implementation and detailed results are available at https://github.com/TheCOBRALab/Spark.
Cite as

Mateo Gray, Sebastian Will, and Hosna Jabbari. Spark: Sparsified Hierarchical Energy Minimization of RNA Pseudoknots. In 25th International Conference on Algorithms for Bioinformatics (WABI 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 344, pp. 13:1-13:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{gray_et_al:LIPIcs.WABI.2025.13,
  author =	{Gray, Mateo and Will, Sebastian and Jabbari, Hosna},
  title =	{{Spark: Sparsified Hierarchical Energy Minimization of RNA Pseudoknots}},
  booktitle =	{25th International Conference on Algorithms for Bioinformatics (WABI 2025)},
  pages =	{13:1--13:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-386-7},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{344},
  editor =	{Brejov\'{a}, Bro\v{n}a and Patro, Rob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.WABI.2025.13},
  URN =		{urn:nbn:de:0030-drops-239383},
  doi =		{10.4230/LIPIcs.WABI.2025.13},
  annote =	{Keywords: RNA, MFE, Secondary Structure Prediction, Pseudoknot, Sparsification, Space Complexity, Time Complexity}
}
Document
DOI: 10.4230/LIPIcs.CP.2025.24
The Work Task Variation Problem

Authors: Mikael Z. Lagerkvist and Magnus Rattfeldt

Published in: LIPIcs, Volume 340, 31st International Conference on Principles and Practice of Constraint Programming (CP 2025)

Abstract
This paper introduces the Work Task Variation (WTV) problem, a novel scheduling post-processing challenge focused on improving worker shift quality by rearranging tasks within their assigned time slots. The objective is to avoid excessively short or long durations of specific task types, creating smoother and more ergonomic work patterns. We present RosterLogic Variation, a constraint-based local search (CBLS) inspired solver originally developed at Optischedule and successfully deployed in real-world retail settings. This solver rapidly improves existing schedules using tailored invariants and heuristics. We also provide a complete MiniZinc model and a set of generated realistic publicly available benchmark instances. We compare our solver’s performance with that of modern CP solvers using the MiniZinc model. Contemporary state-of-the-art CP solvers are approaching the interactive performance of our CBLS solver for coarse planning, representing a significant advancement since the original design and implementation of our solver.
Cite as

Mikael Z. Lagerkvist and Magnus Rattfeldt. The Work Task Variation Problem. In 31st International Conference on Principles and Practice of Constraint Programming (CP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 340, pp. 24:1-24:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{lagerkvist_et_al:LIPIcs.CP.2025.24,
  author =	{Lagerkvist, Mikael Z. and Rattfeldt, Magnus},
  title =	{{The Work Task Variation Problem}},
  booktitle =	{31st International Conference on Principles and Practice of Constraint Programming (CP 2025)},
  pages =	{24:1--24:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-380-5},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{340},
  editor =	{de la Banda, Maria Garcia},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2025.24},
  URN =		{urn:nbn:de:0030-drops-238850},
  doi =		{10.4230/LIPIcs.CP.2025.24},
  annote =	{Keywords: Constraint-Based Local Search, Constraint Programming, Metaheuristics, Scheduling}
}
Document
DOI: 10.4230/LIPIcs.CP.2025.9
Constraint Models for Klondike

Authors: Nguyen Dang, Ian P. Gent, Peter Nightingale, Felix Ulrich-Oltean, and Jack Waller

Published in: LIPIcs, Volume 340, 31st International Conference on Principles and Practice of Constraint Programming (CP 2025)

Abstract
Klondike is the most famous single-player card game, and remains a challenging search problem even in the "thoughtful" variant where all card locations are known. We consider the full game of Klondike except for one restriction that the unusual move of "worrying back" is disallowed. This model is able to determine the winnability of all instances of the game and in practice does so in less than 2000 secs for 10,000 instances we tested, which no other known algorithm can achieve. On some instances, however, other techniques can produce answers more quickly. We use constraint modelling to produce schedules for running our constraint model in combination with other techniques. The combination outperforms any single solver across a range of time limits. Using this combination we are able to significantly improve the best estimate of winnability of Klondike without worrying back. Finally we show how we can use this work to also improve the estimate of winnability of the regular game of Klondike.
Cite as

Nguyen Dang, Ian P. Gent, Peter Nightingale, Felix Ulrich-Oltean, and Jack Waller. Constraint Models for Klondike. In 31st International Conference on Principles and Practice of Constraint Programming (CP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 340, pp. 9:1-9:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{dang_et_al:LIPIcs.CP.2025.9,
  author =	{Dang, Nguyen and Gent, Ian P. and Nightingale, Peter and Ulrich-Oltean, Felix and Waller, Jack},
  title =	{{Constraint Models for Klondike}},
  booktitle =	{31st International Conference on Principles and Practice of Constraint Programming (CP 2025)},
  pages =	{9:1--9:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-380-5},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{340},
  editor =	{de la Banda, Maria Garcia},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2025.9},
  URN =		{urn:nbn:de:0030-drops-238702},
  doi =		{10.4230/LIPIcs.CP.2025.9},
  annote =	{Keywords: AI Planning, Modelling, Constraint Programming, Solitaire and Patience Games}
}
Document
DOI: 10.4230/LIPIcs.CP.2025.31
Transformer-Based Feature Learning for Algorithm Selection in Combinatorial Optimisation

Authors: Alessio Pellegrino, Özgür Akgün, Nguyen Dang, Zeynep Kiziltan, and Ian Miguel

Published in: LIPIcs, Volume 340, 31st International Conference on Principles and Practice of Constraint Programming (CP 2025)

Abstract
Given a combinatorial optimisation problem, there are typically multiple ways of modelling it for presentation to an automated solver. Choosing the right combination of model and target solver can have a significant impact on the effectiveness of the solving process. The best combination of model and solver can also be instance-dependent: there may not exist a single combination that works best for all instances of the same problem. We consider the task of building machine learning models to automatically select the best combination for a problem instance. Critical to the learning process is to define instance features, which serve as input to the selection model. Our contribution is the automatic learning of instance features directly from the high-level representation of a problem instance using a transformer encoder. We evaluate the performance of our approach using the Essence modelling language via a case study of three problem classes.
Cite as

Alessio Pellegrino, Özgür Akgün, Nguyen Dang, Zeynep Kiziltan, and Ian Miguel. Transformer-Based Feature Learning for Algorithm Selection in Combinatorial Optimisation. In 31st International Conference on Principles and Practice of Constraint Programming (CP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 340, pp. 31:1-31:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{pellegrino_et_al:LIPIcs.CP.2025.31,
  author =	{Pellegrino, Alessio and Akg\"{u}n, \"{O}zg\"{u}r and Dang, Nguyen and Kiziltan, Zeynep and Miguel, Ian},
  title =	{{Transformer-Based Feature Learning for Algorithm Selection in Combinatorial Optimisation}},
  booktitle =	{31st International Conference on Principles and Practice of Constraint Programming (CP 2025)},
  pages =	{31:1--31:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-380-5},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{340},
  editor =	{de la Banda, Maria Garcia},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2025.31},
  URN =		{urn:nbn:de:0030-drops-238928},
  doi =		{10.4230/LIPIcs.CP.2025.31},
  annote =	{Keywords: Constraint modelling, algorithm selection, feature extraction, machine learning, transformer architecture}
}
Document
DOI: 10.4230/LIPIcs.CP.2025.34
DynamicSAT: Dynamic Configuration Tuning for SAT Solving

Authors: Zhengyuan Shi, Wentao Jiang, Xindi Zhang, Jin Luo, Yun Liang, Zhufei Chu, and Qiang Xu

Published in: LIPIcs, Volume 340, 31st International Conference on Principles and Practice of Constraint Programming (CP 2025)

Abstract
Boolean Satisfiability (SAT) problem serves as a foundation for solving numerous real-world challenges. As problem complexity increases, so does the demand for sophisticated SAT solvers, which incorporate a variety of heuristics tailored to optimize performance for specific problem instances. However, a major limitation persists: a configuration that performs well on one instance may lead to inefficiencies on others. While previous approaches to automatic algorithm configuration set parameters prior to runtime, they fail to adapt to the dynamic evolution of problem characteristics during the solving process. We introduce DynamicSAT, a novel SAT solver framework that dynamically tunes configuration parameters during solving process. By adjusting parameters on-the-fly, DynamicSAT adapts to changes arising from clause learning, elimination, and other transformations, thus improving efficiency and robustness across diverse SAT instances. We demonstrate that DynamicSAT achieves significant performance gains over the state-of-the-art solver on 2024 SAT Competition Benchmark.
Cite as

Zhengyuan Shi, Wentao Jiang, Xindi Zhang, Jin Luo, Yun Liang, Zhufei Chu, and Qiang Xu. DynamicSAT: Dynamic Configuration Tuning for SAT Solving. In 31st International Conference on Principles and Practice of Constraint Programming (CP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 340, pp. 34:1-34:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{shi_et_al:LIPIcs.CP.2025.34,
  author =	{Shi, Zhengyuan and Jiang, Wentao and Zhang, Xindi and Luo, Jin and Liang, Yun and Chu, Zhufei and Xu, Qiang},
  title =	{{DynamicSAT: Dynamic Configuration Tuning for SAT Solving}},
  booktitle =	{31st International Conference on Principles and Practice of Constraint Programming (CP 2025)},
  pages =	{34:1--34:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-380-5},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{340},
  editor =	{de la Banda, Maria Garcia},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2025.34},
  URN =		{urn:nbn:de:0030-drops-238952},
  doi =		{10.4230/LIPIcs.CP.2025.34},
  annote =	{Keywords: Boolean satisfiability problem, configuration tuning, multi-armed bandit}
}
Document
DOI: 10.4230/LIPIcs.SAT.2025.29
Reencoding Unique Literal Clauses

Authors: Aeacus Sheng, Joseph E. Reeves, and Marijn J. H. Heule

Published in: LIPIcs, Volume 341, 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)

Abstract
We present a lightweight reencoding technique that augments propositional formulas containing implicit or explicit exactly-one constraints with auxiliary variables derived from the order encoding. Our approach is based on the observation that many formulas contain clauses where each literal appears only in that clause, and that these unique literal clauses can be replaced by the corresponding sequential counter encoding of exactly-one constraints, which introduces the same variables as the order encoding. We implemented the reencoding in the state-of-the-art SAT solver CaDiCaL with support for proof logging and solution reconstruction. Experiments on SAT Competition benchmarks demonstrate that our technique enables solving dozens of additional formulas. We found that shuffling a formula before reencoding harms performance. To mitigate this issue, we introduce a method that sorts literals within clauses based on the formula structure before applying our reencoding. The same technique also predicts whether reencoding is likely to yield improvements.
Cite as

Aeacus Sheng, Joseph E. Reeves, and Marijn J. H. Heule. Reencoding Unique Literal Clauses. In 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 341, pp. 29:1-29:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{sheng_et_al:LIPIcs.SAT.2025.29,
  author =	{Sheng, Aeacus and Reeves, Joseph E. and Heule, Marijn J. H.},
  title =	{{Reencoding Unique Literal Clauses}},
  booktitle =	{28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)},
  pages =	{29:1--29:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-381-2},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{341},
  editor =	{Berg, Jeremias and Nordstr\"{o}m, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2025.29},
  URN =		{urn:nbn:de:0030-drops-237635},
  doi =		{10.4230/LIPIcs.SAT.2025.29},
  annote =	{Keywords: Satisfiability solving, auxiliary variables, graph coloring}
}
Document
DOI: 10.4230/LIPIcs.SAT.2025.25
QRP+Gen: A Framework for Checking Q-Resolution Proofs with Generalized Axioms

Authors: Mark Peyrer and Martina Seidl

Published in: LIPIcs, Volume 341, 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)

Abstract
Q-resolution is a proof system for quantified Boolean formulas (QBFs) that forms the foundation for search-based QBF solvers with clause and cube learning. To derive stronger clauses and cubes, Q-resolution was extended with so-called generalized axioms. The derivation of such generalized axioms relies on solving oracles that could be, for example, SAT solvers or even QBF solvers. While the correctness of results obtained with classical QCDCL-based solving can be efficiently certified by an independent checker, until now, proof generation had to be turned off to benefit from generalized axioms. Consequently, the results obtained with reasoning under generalized axioms could not be certified independently. To overcome this restriction, we present QRP+Gen, a novel framework to automatically generate and check Q-resolution proofs that contain generalized axioms. To this end, we extended the Q-resolution format QRP such that all necessary information is included to verify the correctness of generalized axioms. Our extension allows to integrate certificates produced by any oracle which can produce automatically checkable proofs. Furthermore, we developed a proof checker that orchestrates the proof checking of the core Q-resolution proof and the proofs produced by the oracles. As a case study, we equipped the search-based QBF solver DepQBF with proof-producing oracles for the SAT-based techniques trivial truth and trivial falsity.
Cite as

Mark Peyrer and Martina Seidl. QRP+Gen: A Framework for Checking Q-Resolution Proofs with Generalized Axioms. In 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 341, pp. 25:1-25:10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{peyrer_et_al:LIPIcs.SAT.2025.25,
  author =	{Peyrer, Mark and Seidl, Martina},
  title =	{{QRP+Gen: A Framework for Checking Q-Resolution Proofs with Generalized Axioms}},
  booktitle =	{28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)},
  pages =	{25:1--25:10},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-381-2},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{341},
  editor =	{Berg, Jeremias and Nordstr\"{o}m, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2025.25},
  URN =		{urn:nbn:de:0030-drops-237592},
  doi =		{10.4230/LIPIcs.SAT.2025.25},
  annote =	{Keywords: Automated Reasoning, Quantified Resolution Proof, Generalized Axioms}
}
Document
DOI: 10.4230/OASIcs.SLATE.2025.8
An Architecture for Composite Combinatorial Optimization Solvers

Authors: Khalil Chrit, Jean-François Baffier, Pedro Patinho, and Salvador Abreu

Published in: OASIcs, Volume 135, 14th Symposium on Languages, Applications and Technologies (SLATE 2025)

Abstract
In this paper, we introduce elements for MoSCO, a framework for building hybrid metaheuristic-based solvers from a collection of reusable base components. The framework is implemented in Julia and provides a modular architecture for composing solvers through a pipeline-based approach. The modular design of MoSCO supports the creation of reusable components and adaptable solver strategies for various Constraint Satisfaction Problems (CSPs) and Constraint Optimization Problems (COPs). We validate MoSCO’s utility through practical examples, demonstrating its effectiveness in reconstructing established metaheuristics and enabling the creation of novel solver configurations. This work lays the foundation for future developments in automated solver construction and parameter optimization.
Cite as

Khalil Chrit, Jean-François Baffier, Pedro Patinho, and Salvador Abreu. An Architecture for Composite Combinatorial Optimization Solvers. In 14th Symposium on Languages, Applications and Technologies (SLATE 2025). Open Access Series in Informatics (OASIcs), Volume 135, pp. 8:1-8:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{chrit_et_al:OASIcs.SLATE.2025.8,
  author =	{Chrit, Khalil and Baffier, Jean-Fran\c{c}ois and Patinho, Pedro and Abreu, Salvador},
  title =	{{An Architecture for Composite Combinatorial Optimization Solvers}},
  booktitle =	{14th Symposium on Languages, Applications and Technologies (SLATE 2025)},
  pages =	{8:1--8:16},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-387-4},
  ISSN =	{2190-6807},
  year =	{2025},
  volume =	{135},
  editor =	{Baptista, Jorge and Barateiro, Jos\'{e}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.SLATE.2025.8},
  URN =		{urn:nbn:de:0030-drops-236885},
  doi =		{10.4230/OASIcs.SLATE.2025.8},
  annote =	{Keywords: Hybrid Metaheuristics, DSL}
}
Document
DOI: 10.4230/LIPIcs.SAT.2024.27
Revisiting SATZilla Features in 2024

Authors: Hadar Shavit and Holger H. Hoos

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

Abstract
Boolean satisfiability (SAT) is an NP-complete problem with important applications, notably in hardware and software verification. Characterising a SAT instance by a set of features has shown great potential for various tasks, ranging from algorithm selection to benchmark generation. In this work, we revisit the widely used SATZilla features and introduce a new version of the tool used to compute them. In particular, we utilise a new preprocessor and SAT solvers, adjust the code to accommodate larger formulas, and determine better settings of the feature extraction time limits. We evaluate the extracted features on three downstream tasks: satisfiability prediction, running time prediction, and algorithm selection. We observe that our new tool is able to extract features from a broader range of instances than before. We show that the new version of the feature extractor produces features that achieve up to 26% lower RMSE for running time prediction, up to 3% higher accuracy for satisfiability prediction, and up to 15 times higher closed gap for algorithm selection on benchmarks from recent SAT competitions.
Cite as

Hadar Shavit and Holger H. Hoos. Revisiting SATZilla Features in 2024. In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, pp. 27:1-27:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{shavit_et_al:LIPIcs.SAT.2024.27,
  author =	{Shavit, Hadar and Hoos, Holger H.},
  title =	{{Revisiting SATZilla Features in 2024}},
  booktitle =	{27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)},
  pages =	{27:1--27:26},
  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.27},
  URN =		{urn:nbn:de:0030-drops-205496},
  doi =		{10.4230/LIPIcs.SAT.2024.27},
  annote =	{Keywords: Satisfiability, feature extraction, running time prediction, satisfiability prediction}
}
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/DagRep.13.11.72
Space and Artificial Intelligence (Dagstuhl Seminar 23461)

Authors: Sašo Džeroski, Holger H. Hoos, Bertrand Le Saux, Leendert van der Torre, and Ana Kostovska

Published in: Dagstuhl Reports, Volume 13, Issue 11 (2024)

Abstract
This report documents the program and the outcomes of the Dagstuhl Seminar 23461 "Space and Artificial Intelligence". The seminar was interdisciplinary, situated at the intersection of research on AI / computer science and space research. Since each of these is a very wide field on its own, we focussed on a selection of topics from each of the two and their intersections. On the artificial intelligence side, we focused on data-driven AI, which makes use of data in order to produce intelligent behaviour and notably includes machine learning approaches. We also considered knowledge-based AI, which is focussed on the explicit formalisation of human knowledge and its use for tasks such as reasoning, planning, and scheduling. On the space research side, we considered the two major branches of space operations (SO) and Earth observation (EO). The seminar brought together a diverse set of players, including researchers from academia, on one hand, and practitioners from space agencies (ESA, NASA) and industry, on the other hand. The seminar included plenary talks and parallel group discussions. Through the plenary talks, we obtained insight into the state-of-the-art in the different areas of AI research and space research, and especially in their intersections. Through the parallel group discussions, we identified obstacles and challenges to further progress and charted directions for further work.
Cite as

Sašo Džeroski, Holger H. Hoos, Bertrand Le Saux, Leendert van der Torre, and Ana Kostovska. Space and Artificial Intelligence (Dagstuhl Seminar 23461). In Dagstuhl Reports, Volume 13, Issue 11, pp. 72-102, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@Article{dzeroski_et_al:DagRep.13.11.72,
  author =	{D\v{z}eroski, Sa\v{s}o and Hoos, Holger H. and Le Saux, Bertrand and van der Torre, Leendert and Kostovska, Ana},
  title =	{{Space and Artificial Intelligence (Dagstuhl Seminar 23461)}},
  pages =	{72--102},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2024},
  volume =	{13},
  number =	{11},
  editor =	{D\v{z}eroski, Sa\v{s}o and Hoos, Holger H. and Le Saux, Bertrand and van der Torre, Leendert and Kostovska, Ana},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.13.11.72},
  URN =		{urn:nbn:de:0030-drops-198454},
  doi =		{10.4230/DagRep.13.11.72},
  annote =	{Keywords: Artificial Intelligence, Machine Learning, Data-based AI, Knowledge-based AI, Deep Learning, Foundation Models, Explainable Artificial Intelligence, Space Research, Space Operations, Earth Observation}
}
Document
Vision
DOI: 10.4230/TGDK.1.1.3
Knowledge Engineering Using Large Language Models

Authors: Bradley P. Allen, Lise Stork, and Paul Groth

Published in: TGDK, Volume 1, Issue 1 (2023): Special Issue on Trends in Graph Data and Knowledge. Transactions on Graph Data and Knowledge, Volume 1, Issue 1

Abstract
Knowledge engineering is a discipline that focuses on the creation and maintenance of processes that generate and apply knowledge. Traditionally, knowledge engineering approaches have focused on knowledge expressed in formal languages. The emergence of large language models and their capabilities to effectively work with natural language, in its broadest sense, raises questions about the foundations and practice of knowledge engineering. Here, we outline the potential role of LLMs in knowledge engineering, identifying two central directions: 1) creating hybrid neuro-symbolic knowledge systems; and 2) enabling knowledge engineering in natural language. Additionally, we formulate key open research questions to tackle these directions.
Cite as

Bradley P. Allen, Lise Stork, and Paul Groth. Knowledge Engineering Using Large Language Models. In Special Issue on Trends in Graph Data and Knowledge. Transactions on Graph Data and Knowledge (TGDK), Volume 1, Issue 1, pp. 3:1-3:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@Article{allen_et_al:TGDK.1.1.3,
  author =	{Allen, Bradley P. and Stork, Lise and Groth, Paul},
  title =	{{Knowledge Engineering Using Large Language Models}},
  journal =	{Transactions on Graph Data and Knowledge},
  pages =	{3:1--3:19},
  ISSN =	{2942-7517},
  year =	{2023},
  volume =	{1},
  number =	{1},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/TGDK.1.1.3},
  URN =		{urn:nbn:de:0030-drops-194777},
  doi =		{10.4230/TGDK.1.1.3},
  annote =	{Keywords: knowledge engineering, large language models}
}
  • Refine by Type
  • 21 Document/PDF
  • 13 Document/HTML

  • Refine by Publication Year
  • 1 2026
  • 10 2025
  • 3 2024
  • 2 2023
  • 1 2022
  • Show More...

  • Refine by Author
  • 6 Hoos, Holger H.
  • 3 Iser, Ashlin
  • 2 Anastacio, Marie
  • 2 Dang, Nguyen
  • 2 Matricon, Théo
  • Show More...

  • Refine by Series/Journal
  • 15 LIPIcs
  • 1 OASIcs
  • 2 TGDK
  • 3 DagRep

  • Refine by Classification
  • 4 Theory of computation → Constraint and logic programming
  • 3 Computing methodologies → Planning and scheduling
  • 3 Theory of computation → Automated reasoning
  • 2 Computing methodologies → Knowledge representation and reasoning
  • 2 Theory of computation → Design and analysis of algorithms
  • Show More...

  • Refine by Keyword
  • 3 machine learning
  • 2 Constraint Programming
  • 2 algorithm selection
  • 2 feature extraction
  • 1 AI
  • Show More...

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