Search Results

Documents authored by Schidler, André

Artifact
Software
DOI: 10.4230/artifacts.24025
Kissat Clause Reduction Version

Authors: Bernhard Gstrein, Florian Pollitt, André Schidler, Mathias Fleury, and Armin Biere

Abstract
Cite as

Bernhard Gstrein, Florian Pollitt, André Schidler, Mathias Fleury, Armin Biere. Kissat Clause Reduction Version (Software, Source Code). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@misc{github,
   title = {{Kissat Clause Reduction Version}}, 
   author = {Gstrein, Bernhard and Pollitt, Florian and Schidler, Andr\'{e} and Fleury, Mathias and Biere, Armin},
   note = {Software, swhId: \href{https://archive.softwareheritage.org/swh:1:dir:b6a189824ab8c4ceab3f1a2f31c349423724cc19;origin=https://github.com/texmex76/kissat-cr;visit=swh:1:snp:5683baa56ab6acbc85aca46b16845fd3f6da4cf6;anchor=swh:1:rev:84d0d475780fa7e507cd7c9749e4c77465c35bfa}{\texttt{swh:1:dir:b6a189824ab8c4ceab3f1a2f31c349423724cc19}} (visited on 2025-08-07)},
   url = {https://github.com/texmex76/kissat-cr},
   doi = {10.4230/artifacts.24025},
}
Document
DOI: 10.4230/LIPIcs.SAT.2025.14
Learn to Unlearn

Authors: Bernhard Gstrein, Florian Pollitt, André Schidler, Mathias Fleury, and Armin Biere

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

Abstract
Clause learning is a significant milestone in the development of SAT solving. However, keeping all learned clauses without discrimination gradually slows down the solver. Thus, selectively removing some learned clauses during routine database reduction is essential. In this paper, we reexamine and test several long-standing ideas for clause removal in the modern solver Kissat. Our experiments show that retaining all clauses alters performance in all instances. For satisfiable instances, periodically removing all learned clauses surprisingly yields near state-of-the-art performance. For unsatisfiable instances, it is vital to always keep some learned clauses. Building on the influential Glucose paper, we find that it is crucial to always retain the clauses most likely to help, regardless of whether they are ranked by size or LBD in practice. Another key factor is whether a clause was used recently during conflict resolution steps. Eagerly keeping used clauses improves all unlearning strategies.
Cite as

Bernhard Gstrein, Florian Pollitt, André Schidler, Mathias Fleury, and Armin Biere. Learn to Unlearn. In 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 341, pp. 14:1-14:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{gstrein_et_al:LIPIcs.SAT.2025.14,
  author =	{Gstrein, Bernhard and Pollitt, Florian and Schidler, Andr\'{e} and Fleury, Mathias and Biere, Armin},
  title =	{{Learn to Unlearn}},
  booktitle =	{28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)},
  pages =	{14:1--14:12},
  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.14},
  URN =		{urn:nbn:de:0030-drops-237480},
  doi =		{10.4230/LIPIcs.SAT.2025.14},
  annote =	{Keywords: Satisfiability solving, learned clause recycling, LBD}
}
Document
DOI: 10.4230/LIPIcs.SAT.2025.26
Analyzing Reformulation Performance in Core-Guided MaxSAT Solving

Authors: André Schidler and Stefan Szeider

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

Abstract
Core-guided algorithms like OLL are among the best methods for solving the Maximum Satisfiability problem (MaxSAT). Although some performance characteristics of OLL have been studied, a comprehensive experimental analysis of its reformulation behavior is still missing. In this paper, we present a large-scale study on how different reformulations of a MaxSAT instance produced by OLL affect solver performance. By representing these reformulations as a directed acyclic graph (DAG), we isolate the impact of structural features - such as the size and interconnectivity of unsatisfiable cores - on solver runtime. Our extensive experimental evaluation of over 600k solver runs reveals clear correlations between DAG properties and performance outcomes. These results suggest a new avenue for designing heuristics that steer the solver toward more tractable reformulations. All OLL DAGs and performance data from our experiments are publicly available to foster further research.
Cite as

André Schidler and Stefan Szeider. Analyzing Reformulation Performance in Core-Guided MaxSAT Solving. In 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 341, pp. 26:1-26:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{schidler_et_al:LIPIcs.SAT.2025.26,
  author =	{Schidler, Andr\'{e} and Szeider, Stefan},
  title =	{{Analyzing Reformulation Performance in Core-Guided MaxSAT Solving}},
  booktitle =	{28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)},
  pages =	{26:1--26:18},
  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.26},
  URN =		{urn:nbn:de:0030-drops-237605},
  doi =		{10.4230/LIPIcs.SAT.2025.26},
  annote =	{Keywords: maximum satisfiability, OLL, core-guided}
}
Document
DOI: 10.4230/LIPIcs.CP.2024.26
Structure-Guided Local Improvement for Maximum Satisfiability

Authors: André Schidler and Stefan Szeider

Published in: LIPIcs, Volume 307, 30th International Conference on Principles and Practice of Constraint Programming (CP 2024)

Abstract
The enhanced performance of today’s MaxSAT solvers has elevated their appeal for many large-scale applications, notably in software analysis and computer-aided design. Our research delves into refining anytime MaxSAT solving by repeatedly identifying and solving with an exact solver smaller subinstances that are chosen based on the graphical structure of the instance. We investigate various strategies to pinpoint these subinstances. This structure-guided selection of subinstances provides an exact solver with a high potential for improving the current solution. Our exhaustive experimental analyses contrast our methodology as instantiated in our tool MaxSLIM with previous studies and benchmark it against leading-edge MaxSAT solvers.
Cite as

André Schidler and Stefan Szeider. Structure-Guided Local Improvement for Maximum Satisfiability. In 30th International Conference on Principles and Practice of Constraint Programming (CP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 307, pp. 26:1-26:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{schidler_et_al:LIPIcs.CP.2024.26,
  author =	{Schidler, Andr\'{e} and Szeider, Stefan},
  title =	{{Structure-Guided Local Improvement for Maximum Satisfiability}},
  booktitle =	{30th International Conference on Principles and Practice of Constraint Programming (CP 2024)},
  pages =	{26:1--26:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-336-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{307},
  editor =	{Shaw, Paul},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2024.26},
  URN =		{urn:nbn:de:0030-drops-207112},
  doi =		{10.4230/LIPIcs.CP.2024.26},
  annote =	{Keywords: maximum satisfiability, large neighborhood search (LNS), SAT-based local improvement (SLIM), incomplete MaxSAT, graphical structure, metaheuristic}
}
Document
DOI: 10.4230/DagRep.13.6.106
SAT Encodings and Beyond (Dagstuhl Seminar 23261)

Authors: Marijn J. H. Heule, Inês Lynce, Stefan Szeider, and Andre Schidler

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

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 23261 "SAT Encodings and Beyond." The seminar facilitated an intense examination and discussion of current results and challenges related to encodings for SAT and related solving paradigms. The seminar featured presentations and group work that provided theoretical, practical, and industrial viewpoints. The goal was to foster more profound insights and advancements in encoding techniques, which are pivotal in enhancing solvers' efficiency.
Cite as

Marijn J. H. Heule, Inês Lynce, Stefan Szeider, and Andre Schidler. SAT Encodings and Beyond (Dagstuhl Seminar 23261). In Dagstuhl Reports, Volume 13, Issue 6, pp. 106-122, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@Article{heule_et_al:DagRep.13.6.106,
  author =	{Heule, Marijn J. H. and Lynce, In\^{e}s and Szeider, Stefan and Schidler, Andre},
  title =	{{SAT Encodings and Beyond (Dagstuhl Seminar 23261)}},
  pages =	{106--122},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2024},
  volume =	{13},
  number =	{6},
  editor =	{Heule, Marijn J. H. and Lynce, In\^{e}s and Szeider, Stefan and Schidler, Andre},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.13.6.106},
  URN =		{urn:nbn:de:0030-drops-196409},
  doi =		{10.4230/DagRep.13.6.106},
  annote =	{Keywords: constraint propagation, lower and upper bounds, problem formulation, propositional satisfiability, symmetry breaking}
}
Document
PACE Solver Description
DOI: 10.4230/LIPIcs.IPEC.2022.32
PACE Solver Description: DAGer - Cutting out Cycles with MaxSAT

Authors: Rafael Kiesel and André Schidler

Published in: LIPIcs, Volume 249, 17th International Symposium on Parameterized and Exact Computation (IPEC 2022)

Abstract
We describe the solver DAGer for the Directed Feedback Vertex Set (DFVS) problem, as it was submitted to the exact track of the 2022 PACE Challenge. Our approach first applies a wide range of preprocessing techniques involving both well-known data reductions for DFVS as well as non-trivial adaptations from the vertex cover problem. For the actual solving, we found that using a MaxSAT solver with incremental constraints achieves a good performance.
Cite as

Rafael Kiesel and André Schidler. PACE Solver Description: DAGer - Cutting out Cycles with MaxSAT. In 17th International Symposium on Parameterized and Exact Computation (IPEC 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 249, pp. 32:1-32:4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{kiesel_et_al:LIPIcs.IPEC.2022.32,
  author =	{Kiesel, Rafael and Schidler, Andr\'{e}},
  title =	{{PACE Solver Description: DAGer - Cutting out Cycles with MaxSAT}},
  booktitle =	{17th International Symposium on Parameterized and Exact Computation (IPEC 2022)},
  pages =	{32:1--32:4},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-260-0},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{249},
  editor =	{Dell, Holger and Nederlof, Jesper},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.IPEC.2022.32},
  URN =		{urn:nbn:de:0030-drops-173885},
  doi =		{10.4230/LIPIcs.IPEC.2022.32},
  annote =	{Keywords: Directed Feeback Vertex Set, Data Reductions, Incremental MaxSAT}
}
Document
DOI: 10.4230/LIPIcs.SAT.2022.15
Weighted Model Counting with Twin-Width

Authors: Robert Ganian, Filip Pokrývka, André Schidler, Kirill Simonov, and Stefan Szeider

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

Abstract
Bonnet et al. (FOCS 2020) introduced the graph invariant twin-width and showed that many NP-hard problems are tractable for graphs of bounded twin-width, generalizing similar results for other width measures, including treewidth and clique-width. In this paper, we investigate the use of twin-width for solving the propositional satisfiability problem (SAT) and propositional model counting. We particularly focus on Bounded-ones Weighted Model Counting (BWMC), which takes as input a CNF formula F along with a bound k and asks for the weighted sum of all models with at most k positive literals. BWMC generalizes not only SAT but also (weighted) model counting. We develop the notion of "signed" twin-width of CNF formulas and establish that BWMC is fixed-parameter tractable when parameterized by the certified signed twin-width of F plus k. We show that this result is tight: it is neither possible to drop the bound k nor use the vanilla twin-width instead if one wishes to retain fixed-parameter tractability, even for the easier problem SAT. Our theoretical results are complemented with an empirical evaluation and comparison of signed twin-width on various classes of CNF formulas.
Cite as

Robert Ganian, Filip Pokrývka, André Schidler, Kirill Simonov, and Stefan Szeider. Weighted Model Counting with Twin-Width. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 15:1-15:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{ganian_et_al:LIPIcs.SAT.2022.15,
  author =	{Ganian, Robert and Pokr\'{y}vka, Filip and Schidler, Andr\'{e} and Simonov, Kirill and Szeider, Stefan},
  title =	{{Weighted Model Counting with Twin-Width}},
  booktitle =	{25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
  pages =	{15:1--15:17},
  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.15},
  URN =		{urn:nbn:de:0030-drops-166896},
  doi =		{10.4230/LIPIcs.SAT.2022.15},
  annote =	{Keywords: Weighted model counting, twin-width, parameterized complexity, SAT}
}
Document
CG Challenge
DOI: 10.4230/LIPIcs.SoCG.2022.74
SAT-Based Local Search for Plane Subgraph Partitions (CG Challenge)

Authors: André Schidler

Published in: LIPIcs, Volume 224, 38th International Symposium on Computational Geometry (SoCG 2022)

Abstract
The Partition into Plane Subgraphs Problem (PPS) asks to partition the edges of a geometric graph with straight line segments into as few classes as possible, such that the line segments within a class do not cross. We discuss our approach GC-SLIM: a local search method that views PPS as a graph coloring problem and tackles it with a new and unique combination of propositional satisfiability (SAT) and tabu search, achieving the fourth place in the 2022 CG:SHOP Challenge.
Cite as

André Schidler. SAT-Based Local Search for Plane Subgraph Partitions (CG Challenge). In 38th International Symposium on Computational Geometry (SoCG 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 224, pp. 74:1-74:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{schidler:LIPIcs.SoCG.2022.74,
  author =	{Schidler, Andr\'{e}},
  title =	{{SAT-Based Local Search for Plane Subgraph Partitions}},
  booktitle =	{38th International Symposium on Computational Geometry (SoCG 2022)},
  pages =	{74:1--74:8},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-227-3},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{224},
  editor =	{Goaoc, Xavier and Kerber, Michael},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SoCG.2022.74},
  URN =		{urn:nbn:de:0030-drops-160829},
  doi =		{10.4230/LIPIcs.SoCG.2022.74},
  annote =	{Keywords: graph coloring, plane subgraphs, SAT, logic, SLIM, local improvement, large neighborhood search}
}
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact