Search Results

Documents authored by Schidler, André

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}
}
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 About DROPS Imprint Privacy Contact