45 Search Results for "Held, Stephan"

Document
DOI: 10.4230/LIPIcs.ESA.2025.29
The Tape Reconfiguration Problem and Its Consequences for Dominating Set Reconfiguration

Authors: Nicolas Bousquet, Quentin Deschamps, Arnaud Mary, Amer E. Mouawad, and Théo Pierron

Published in: LIPIcs, Volume 351, 33rd Annual European Symposium on Algorithms (ESA 2025)

Abstract
A dominating set of a graph G = (V,E) is a set of vertices D ⊆ V whose closed neighborhood is V, i.e., N[D] = V. We view a dominating set as a collection of tokens placed on the vertices of D. In the token sliding variant of the Dominating Set Reconfiguration problem (TS-DSR), we seek to transform a source dominating set into a target dominating set in G by sliding tokens along edges, and while maintaining a dominating set all along the transformation. TS-DSR is known to be PSPACE-complete even restricted to graphs of pathwidth w, for some non-explicit constant w and to be XL-complete parameterized by the size k of the solution. The first contribution of this article consists in using a novel approach to provide the first explicit constant for which the TS-DSR problem is PSPACE-complete, a question that was left open in the literature. From a parameterized complexity perspective, the token jumping variant of DSR, i.e., where tokens can jump to arbitrary vertices, is known to be FPT when parameterized by the size of the dominating sets on nowhere dense classes of graphs. But, in contrast, no non-trivial result was known about TS-DSR. We prove that DSR is actually much harder in the sliding model since it is XL-complete when restricted to bounded pathwidth graphs and even when parameterized by k plus the feedback vertex set number of the graph. This gives, for the first time, a difference of behavior between the complexity under token sliding and token jumping for some problem on graphs of bounded treewidth. All our results are obtained using a brand new method, based on the hardness of the so-called Tape Reconfiguration problem, a problem we believe to be of independent interest. We complement these hardness results with a positive result showing that DSR (parameterized by k) in the sliding model is FPT on planar graphs, also answering an open problem from the literature.
Cite as

Nicolas Bousquet, Quentin Deschamps, Arnaud Mary, Amer E. Mouawad, and Théo Pierron. The Tape Reconfiguration Problem and Its Consequences for Dominating Set Reconfiguration. In 33rd Annual European Symposium on Algorithms (ESA 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 351, pp. 29:1-29:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{bousquet_et_al:LIPIcs.ESA.2025.29,
  author =	{Bousquet, Nicolas and Deschamps, Quentin and Mary, Arnaud and Mouawad, Amer E. and Pierron, Th\'{e}o},
  title =	{{The Tape Reconfiguration Problem and Its Consequences for Dominating Set Reconfiguration}},
  booktitle =	{33rd Annual European Symposium on Algorithms (ESA 2025)},
  pages =	{29:1--29:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-395-9},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{351},
  editor =	{Benoit, Anne and Kaplan, Haim and Wild, Sebastian and Herman, Grzegorz},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ESA.2025.29},
  URN =		{urn:nbn:de:0030-drops-244974},
  doi =		{10.4230/LIPIcs.ESA.2025.29},
  annote =	{Keywords: combinatorial reconfiguration, parameterized complexity, structural graph parameters, treewidth, dominating set}
}
Document
DOI: 10.4230/LIPIcs.ESA.2025.67
Compact Representation of Semilinear and Terrain-Like Graphs

Authors: Jean Cardinal and Yelena Yuditsky

Published in: LIPIcs, Volume 351, 33rd Annual European Symposium on Algorithms (ESA 2025)

Abstract
We consider the existence and construction of biclique covers of graphs, consisting of coverings of their edge sets by complete bipartite graphs. The size of such a cover is the sum of the sizes of the bicliques. Small-size biclique covers of graphs are ubiquitous in computational geometry, and have been shown to be useful compact representations of graphs. We give a brief survey of classical and recent results on biclique covers and their applications, and give new families of graphs having biclique covers of near-linear size. In particular, we show that semilinear graphs, whose edges are defined by linear relations in bounded dimensional space, always have biclique covers of size O(npolylog n). This generalizes many previously known results on special classes of graphs including interval graphs, permutation graphs, and graphs of bounded boxicity, but also new classes such as intersection graphs of L-shapes in the plane. It also directly implies the bounds for Zarankiewicz’s problem derived by Basit, Chernikov, Starchenko, Tao, and Tran (Forum Math. Sigma, 2021). We also consider capped graphs, also known as terrain-like graphs, defined as ordered graphs forbidding a certain ordered pattern on four vertices. Terrain-like graphs contain the induced subgraphs of terrain visibility graphs. We give an elementary proof that these graphs admit biclique partitions of size O(nlog³ n). This provides a simple combinatorial analogue of a classical result from Agarwal, Alon, Aronov, and Suri on polygon visibility graphs (Discrete Comput. Geom. 1994). Finally, we prove that there exists families of unit disk graphs on n vertices that do not admit biclique coverings of size o(n^{4/3}), showing that we are unlikely to improve on Szemerédi-Trotter type incidence bounds for higher-degree semialgebraic graphs.
Cite as

Jean Cardinal and Yelena Yuditsky. Compact Representation of Semilinear and Terrain-Like Graphs. In 33rd Annual European Symposium on Algorithms (ESA 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 351, pp. 67:1-67:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{cardinal_et_al:LIPIcs.ESA.2025.67,
  author =	{Cardinal, Jean and Yuditsky, Yelena},
  title =	{{Compact Representation of Semilinear and Terrain-Like Graphs}},
  booktitle =	{33rd Annual European Symposium on Algorithms (ESA 2025)},
  pages =	{67:1--67:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-395-9},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{351},
  editor =	{Benoit, Anne and Kaplan, Haim and Wild, Sebastian and Herman, Grzegorz},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ESA.2025.67},
  URN =		{urn:nbn:de:0030-drops-245359},
  doi =		{10.4230/LIPIcs.ESA.2025.67},
  annote =	{Keywords: Biclique covers, intersection graphs, visibility graphs, Zarankiewicz’s problem}
}
Document
DOI: 10.4230/LIPIcs.ITP.2025.26
Improving the SMT Proof Reconstruction Pipeline in Isabelle/HOL

Authors: Hanna Lachnitt, Mathias Fleury, Haniel Barbosa, Jibiana Jakpor, Bruno Andreotti, Andrew Reynolds, Hans-Jörg Schurr, Clark Barrett, and Cesare Tinelli

Published in: LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025)

Abstract
Sledgehammer is a tool that increases the level of automation in the Isabelle/HOL proof assistant by asking external automatic theorem provers (ATPs), including SMT solvers, to prove the current goal. When the external ATP succeeds it must provide enough evidence that the goal holds for Isabelle to be able to reprove it internally based on that evidence. In particular, Isabelle can do this by replaying fine-grained proof certificates from proof-producing SMT solvers as long as they are expressed in the Alethe format, which until now was supported only by the veriT SMT solver. We report on our experience adding proof reconstruction support for the cvc5 SMT solver in Isabelle by extending cvc5 to produce proofs in the Alethe format and then adapting Isabelle to reconstruct those proofs. We discuss several difficulties and pitfalls we encountered and describe a set of tools and techniques we developed to improve the process. A notable outcome of this effort is that Isabelle can now be used as an independent proof checker for SMT problems written in the SMT-LIB standard. We evaluate cvc5’s integration on a set of SMT-LIB benchmarks originating from Isabelle as well as on a set of Isabelle proofs. Our results confirm that this integration complements and improves Sledgehammer’s capabilities.
Cite as

Hanna Lachnitt, Mathias Fleury, Haniel Barbosa, Jibiana Jakpor, Bruno Andreotti, Andrew Reynolds, Hans-Jörg Schurr, Clark Barrett, and Cesare Tinelli. Improving the SMT Proof Reconstruction Pipeline in Isabelle/HOL. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 26:1-26:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{lachnitt_et_al:LIPIcs.ITP.2025.26,
  author =	{Lachnitt, Hanna and Fleury, Mathias and Barbosa, Haniel and Jakpor, Jibiana and Andreotti, Bruno and Reynolds, Andrew and Schurr, Hans-J\"{o}rg and Barrett, Clark and Tinelli, Cesare},
  title =	{{Improving the SMT Proof Reconstruction Pipeline in Isabelle/HOL}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{26:1--26:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-396-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{352},
  editor =	{Forster, Yannick and Keller, Chantal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.26},
  URN =		{urn:nbn:de:0030-drops-246243},
  doi =		{10.4230/LIPIcs.ITP.2025.26},
  annote =	{Keywords: interactive theorem proving, proof assistants, Isabelle/HOL, SMT, certification, proof certificates, proof reconstruction, proof automation}
}
Document
Short Paper
DOI: 10.4230/LIPIcs.ITP.2025.38
Sledgehammering Without ATPs (Short Paper)

Authors: Martin Desharnais and Jasmin Blanchette

Published in: LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025)

Abstract
We describe an alternative architecture for "hammers," inspired by Magnushammer, in which proofs are found by the proof assistant’s built-in automation instead of by external automatic theorem provers (ATPs). We implemented this approach in Isabelle’s Sledgehammer and evaluated it. The new ATP-free approach nicely complements the traditional Sledgehammer. The two approaches in combination solve more goals than the traditional ATP-based approach alone.
Cite as

Martin Desharnais and Jasmin Blanchette. Sledgehammering Without ATPs (Short Paper). In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 38:1-38:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{desharnais_et_al:LIPIcs.ITP.2025.38,
  author =	{Desharnais, Martin and Blanchette, Jasmin},
  title =	{{Sledgehammering Without ATPs}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{38:1--38:8},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-396-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{352},
  editor =	{Forster, Yannick and Keller, Chantal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.38},
  URN =		{urn:nbn:de:0030-drops-246366},
  doi =		{10.4230/LIPIcs.ITP.2025.38},
  annote =	{Keywords: Interactive theorem proving, proof assistants, proof automation}
}
Document
DOI: 10.4230/OASIcs.SpaceCHI.2025.27
Assessing the Use of Mixed Reality as a Valid Tool for Human-Robot Interaction Studies in the Context of Space Exploration

Authors: Enrico Guerra, Sebastian Thomas Büttner, Alper Beşer, and Michael Prilla

Published in: OASIcs, Volume 130, Advancing Human-Computer Interaction for Space Exploration (SpaceCHI 2025)

Abstract
Mixed Reality (MR) is a technology with strong potential for advancing research in Human-Robot Interaction (HRI) for space exploration. Apart from the efficiency and high flexibility MR can offer, we argue that its benefits for HRI research in space contexts lies particularly in its ability to aid human-in-the-loop development, offer realistic hybrid simulations, and foster broader participation in HRI research in the space exploration context. However, we believe that this is only plausible if MR-based simulations can yield comparable results to fully physical approaches in human-centred studies. In this position paper, we highlight several arguments in favour of MR as a tool for space HRI research, while emphasising the importance of the open question regarding its scientific validity. We believe MR could become a central tool for preparing for future human-robotic space exploration missions and significantly diversify research in this domain.
Cite as

Enrico Guerra, Sebastian Thomas Büttner, Alper Beşer, and Michael Prilla. Assessing the Use of Mixed Reality as a Valid Tool for Human-Robot Interaction Studies in the Context of Space Exploration. In Advancing Human-Computer Interaction for Space Exploration (SpaceCHI 2025). Open Access Series in Informatics (OASIcs), Volume 130, pp. 27:1-27:11, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{guerra_et_al:OASIcs.SpaceCHI.2025.27,
  author =	{Guerra, Enrico and B\"{u}ttner, Sebastian Thomas and Be\c{s}er, Alper and Prilla, Michael},
  title =	{{Assessing the Use of Mixed Reality as a Valid Tool for Human-Robot Interaction Studies in the Context of Space Exploration}},
  booktitle =	{Advancing Human-Computer Interaction for Space Exploration (SpaceCHI 2025)},
  pages =	{27:1--27:11},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-384-3},
  ISSN =	{2190-6807},
  year =	{2025},
  volume =	{130},
  editor =	{Bensch, Leonie and Nilsson, Tommy and Nisser, Martin and Pataranutaporn, Pat and Schmidt, Albrecht and Sumini, Valentina},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.SpaceCHI.2025.27},
  URN =		{urn:nbn:de:0030-drops-240175},
  doi =		{10.4230/OASIcs.SpaceCHI.2025.27},
  annote =	{Keywords: Mixed Reality, Augmented Reality, Human-Robot Interaction, Space Exploration, Validity}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2025.51
Word Structures and Their Automatic Presentations

Authors: Xiaoyang Gong, Bakh Khoussainov, and Yuyang Zhuge

Published in: LIPIcs, Volume 345, 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)

Abstract
We study automatic presentations of the structures (ℕ; S), (ℕ; E_S), (ℕ; ≤), and their expansions by a unary predicate U. Here S is the successor function, E_S is the undirected version of S, and ≤ is the natural order. We call these structures word structures. Our goal is three-fold. First, we study the isomorphism problem for automatic word structures by focusing on the following three problems. The first problem asks to design an algorithm that, given an automatic structure A, decides if A is isomorphic to (ℕ; S). The second asks to design an algorithm that, given two automatic presentations of (ℕ; S, U₁) and (ℕ; S, U₂), where U₁ and U₂ are unary predicates, decides if these structures are isomorphic. The third problem investigates if there is an algorithm that, given two automatic presentations of (ℕ; ≤, U₁) and (ℕ; ≤, U₂), decides whether U₁ ∩ U₂ ≠ ∅. We show that these problems are undecidable. Next, we study intrinsic regularity of the function S in the structure Path_ω = (ℕ; E_S). We build an automatic presentation of Path_ω in which S is not regular. This implies that S is not intrinsically regular in Path_ω. For U ⊆ ℕ, let d_U be the function that computes the distances between the consecutive elements of U. We build automatic presentations of (ℕ; ≤, U) where d_U can realise logarithmic, radical, intermediate, and exponential functions.
Cite as

Xiaoyang Gong, Bakh Khoussainov, and Yuyang Zhuge. Word Structures and Their Automatic Presentations. In 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 345, pp. 51:1-51:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{gong_et_al:LIPIcs.MFCS.2025.51,
  author =	{Gong, Xiaoyang and Khoussainov, Bakh and Zhuge, Yuyang},
  title =	{{Word Structures and Their Automatic Presentations}},
  booktitle =	{50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)},
  pages =	{51:1--51:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-388-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{345},
  editor =	{Gawrychowski, Pawe{\l} and Mazowiecki, Filip and Skrzypczak, Micha{\l}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2025.51},
  URN =		{urn:nbn:de:0030-drops-241581},
  doi =		{10.4230/LIPIcs.MFCS.2025.51},
  annote =	{Keywords: Automatic structures, the isomorphism problem, decidability, undecidability, regular relations}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2025.46
Guarding Offices with Maximum Dispersion

Authors: Sándor P. Fekete, Kai Kobbe, Dominik Krupke, Joseph S. B. Mitchell, Christian Rieck, and Christian Scheffer

Published in: LIPIcs, Volume 345, 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)

Abstract
We investigate the Dispersive Art Gallery Problem with vertex guards and rectangular visibility (r-visibility) for a class of orthogonal polygons that reflect the properties of real-world floor plans: these office-like polygons consist of rectangular rooms and corridors. In the dispersive variant of the Art Gallery Problem, the objective is not to minimize the number of guards but to maximize the minimum geodesic L₁-distance between any two guards, called the dispersion distance. Our main contributions are as follows. We prove that determining whether a vertex guard set can achieve a dispersion distance of 4 in office-like polygons is NP-complete, where vertices of the polygon are restricted to integer coordinates. Additionally, we present a simple worst-case optimal algorithm that guarantees a dispersion distance of 3 in polynomial time. Our complexity result extends to polyominoes, resolving an open question posed by Rieck and Scheffer [Christian Rieck and Christian Scheffer, 2024]. When vertex coordinates are allowed to be rational, we establish analogous results, proving that achieving a dispersion distance of 2+ε is NP-hard for any ε > 0, while the classic Art Gallery Problem remains solvable in polynomial time for this class of polygons. Furthermore, we give a straightforward polynomial-time algorithm that computes worst-case optimal solutions with a dispersion distance 2. On the other hand, for the more restricted class of hole-free independent office-like polygons, we propose a dynamic programming approach that computes optimal solutions. Moreover, we demonstrate that the problem is practically tractable for arbitrary orthogonal polygons. To this end, we compare solvers based on SAT, CP, and MIP formulations. Notably, SAT solvers efficiently compute optimal solutions for randomly generated instances with up to 1600 vertices in under 15s.
Cite as

Sándor P. Fekete, Kai Kobbe, Dominik Krupke, Joseph S. B. Mitchell, Christian Rieck, and Christian Scheffer. Guarding Offices with Maximum Dispersion. In 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 345, pp. 46:1-46:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{fekete_et_al:LIPIcs.MFCS.2025.46,
  author =	{Fekete, S\'{a}ndor P. and Kobbe, Kai and Krupke, Dominik and Mitchell, Joseph S. B. and Rieck, Christian and Scheffer, Christian},
  title =	{{Guarding Offices with Maximum Dispersion}},
  booktitle =	{50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)},
  pages =	{46:1--46:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-388-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{345},
  editor =	{Gawrychowski, Pawe{\l} and Mazowiecki, Filip and Skrzypczak, Micha{\l}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2025.46},
  URN =		{urn:nbn:de:0030-drops-241530},
  doi =		{10.4230/LIPIcs.MFCS.2025.46},
  annote =	{Keywords: Dispersive Art Gallery Problem, vertex guards, office-like polygons, orthogonal polygons, polyominoes, NP-completeness, worst-case optimality, dynamic programming, SAT solver}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2025.24
Temporal Valued Constraint Satisfaction Problems

Authors: Manuel Bodirsky, Édouard Bonnet, and Žaneta Semanišinová

Published in: LIPIcs, Volume 345, 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)

Abstract
We study the computational complexity of the valued constraint satisfaction problem (VCSP) for every valued structure over ℚ that is preserved by all order-preserving bijections. Such VCSPs will be called temporal, in analogy to the (classical) constraint satisfaction problem: a relational structure is preserved by all order-preserving bijections if and only if all its relations have a first-order definition in (ℚ; <), and the CSPs for such structures are called temporal CSPs. Many optimization problems that have been studied intensively in the literature can be phrased as a temporal VCSP. We prove that a temporal VCSP is in P, or NP-complete. Our analysis uses the concept of fractional polymorphisms. This is the first dichotomy result for VCSPs over infinite domains which is complete in the sense that it treats all valued structures that contain a given automorphism group.
Cite as

Manuel Bodirsky, Édouard Bonnet, and Žaneta Semanišinová. Temporal Valued Constraint Satisfaction Problems. In 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 345, pp. 24:1-24:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{bodirsky_et_al:LIPIcs.MFCS.2025.24,
  author =	{Bodirsky, Manuel and Bonnet, \'{E}douard and Semani\v{s}inov\'{a}, \v{Z}aneta},
  title =	{{Temporal Valued Constraint Satisfaction Problems}},
  booktitle =	{50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)},
  pages =	{24:1--24:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-388-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{345},
  editor =	{Gawrychowski, Pawe{\l} and Mazowiecki, Filip and Skrzypczak, Micha{\l}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2025.24},
  URN =		{urn:nbn:de:0030-drops-241311},
  doi =		{10.4230/LIPIcs.MFCS.2025.24},
  annote =	{Keywords: Constraint Satisfaction Problems, valued CSPs, temporal CSPs, fractional polymorphisms, complexity dichotomy, min CSPs}
}
Document
DOI: 10.4230/LIPIcs.DNA.31.1
Algorithmic Hardness of the Partition Function for Nucleic Acid Strands

Authors: Gwendal Ducloz, Ahmed Shalaby, and Damien Woods

Published in: LIPIcs, Volume 347, 31st International Conference on DNA Computing and Molecular Programming (DNA 31) (2025)

Abstract
To understand and engineer biological and artificial nucleic acid systems, algorithms are employed for prediction of secondary structures at thermodynamic equilibrium. Dynamic programming algorithms are used to compute the most favoured, or Minimum Free Energy (MFE), structure, and the Partition Function (PF) - a tool for assigning a probability to any structure. However, in some situations, such as when there are large numbers of strands, or pseudoknotted systems, NP-hardness results show that such algorithms are unlikely, but only for MFE. Curiously, algorithmic hardness results were not shown for PF, leaving two open questions on the complexity of PF for multiple strands and single strands with pseudoknots. The challenge is that while the MFE problem cares only about one, or a few structures, PF is a summation over the entire secondary structure space, giving theorists the vibe that computing PF should not only be as hard as MFE, but should be even harder. We answer both questions. First, we show that computing PF is #P-hard for systems with an unbounded number of strands, answering a question of Condon Hajiaghayi, and Thachuk [DNA27]. Second, for even a single strand, but allowing pseudoknots, we find that PF is #P-hard. Our proof relies on a novel magnification trick that leads to a tightly-woven set of reductions between five key thermodynamic problems: MFE, PF, their decision versions, and #SSEL that counts structures of a given energy. Our reductions show these five problems are fundamentally related for any energy model amenable to magnification. That general classification clarifies the mathematical landscape of nucleic acid energy models and yields several open questions.
Cite as

Gwendal Ducloz, Ahmed Shalaby, and Damien Woods. Algorithmic Hardness of the Partition Function for Nucleic Acid Strands. In 31st International Conference on DNA Computing and Molecular Programming (DNA 31). Leibniz International Proceedings in Informatics (LIPIcs), Volume 347, pp. 1:1-1:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{ducloz_et_al:LIPIcs.DNA.31.1,
  author =	{Ducloz, Gwendal and Shalaby, Ahmed and Woods, Damien},
  title =	{{Algorithmic Hardness of the Partition Function for Nucleic Acid Strands}},
  booktitle =	{31st International Conference on DNA Computing and Molecular Programming (DNA 31)},
  pages =	{1:1--1:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-399-7},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{347},
  editor =	{Schaeffer, Josie and Zhang, Fei},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.DNA.31.1},
  URN =		{urn:nbn:de:0030-drops-238504},
  doi =		{10.4230/LIPIcs.DNA.31.1},
  annote =	{Keywords: Partition function, minimum free energy, nucleic acid, DNA, RNA, secondary structure, computational complexity, #P-hardness}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2025.12
The Non-Cooperative Rational Synthesis Problem for SPEs and ω-Regular Objectives

Authors: Véronique Bruyère, Jean-François Raskin, Alexis Reynouard, and Marie Van Den Bogaard

Published in: LIPIcs, Volume 348, 36th International Conference on Concurrency Theory (CONCUR 2025)

Abstract
This paper studies the rational synthesis problem for multi-player games played on graphs when rational players are following subgame perfect equilibria. In these games, one player, the system, declares his strategy upfront, and the other players, composing the environment, then rationally respond by playing strategies forming a subgame perfect equilibrium. We study the complexity of the rational synthesis problem when the players have ω-regular objectives encoded as parity objectives. Our algorithm is based on an encoding into a three-player game with imperfect information, showing that the problem is in 2ExpTime. When the number of environment players is fixed, the problem is in ExpTime and is NP- and coNP-hard. Moreover, for a fixed number of players and reachability objectives, we get a polynomial algorithm.
Cite as

Véronique Bruyère, Jean-François Raskin, Alexis Reynouard, and Marie Van Den Bogaard. The Non-Cooperative Rational Synthesis Problem for SPEs and ω-Regular Objectives. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 12:1-12:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{bruyere_et_al:LIPIcs.CONCUR.2025.12,
  author =	{Bruy\`{e}re, V\'{e}ronique and Raskin, Jean-Fran\c{c}ois and Reynouard, Alexis and Van Den Bogaard, Marie},
  title =	{{The Non-Cooperative Rational Synthesis Problem for SPEs and \omega-Regular Objectives}},
  booktitle =	{36th International Conference on Concurrency Theory (CONCUR 2025)},
  pages =	{12:1--12:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-389-8},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{348},
  editor =	{Bouyer, Patricia and van de Pol, Jaco},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.12},
  URN =		{urn:nbn:de:0030-drops-239622},
  doi =		{10.4230/LIPIcs.CONCUR.2025.12},
  annote =	{Keywords: non-zero-sum games, subgame perfect equilibria, rational synthesis}
}
Document
DOI: 10.4230/LIPIcs.CP.2025.12
An Expansion-Based Approach for Quantified Integer Programming

Authors: Michael Hartisch and Leroy Chew

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

Abstract
Quantified Integer Programming (QIP) bridges multiple domains by extending Quantified Boolean Formulas (QBF) to incorporate general integer variables and linear constraints while also generalizing Integer Programming through variable quantification. As a special case of Quantified Constraint Satisfaction Problems (QCSP), QIP provides a versatile framework for addressing complex decision-making scenarios. Additionally, the inclusion of a linear objective function enables QIP to effectively model multistage robust discrete linear optimization problems, making it a powerful tool for tackling uncertainty in optimization. While two primary solution paradigms exist for QBF - search-based and expansion-based approaches - only search-based methods have been explored for QIP and QCSP. We introduce an expansion-based approach for QIP using Counterexample-Guided Abstraction Refinement (CEGAR), adapting techniques from QBF. We extend this methodology to tackle multistage robust discrete optimization problems with linear constraints and further embed it in an optimization framework, enhancing its applicability. Our experimental results highlight the advantages of this approach, demonstrating superior performance over existing search-based solvers for QIP in specific instances. Furthermore, the ability to model problems using linear constraints enables notable performance gains over state-of-the-art expansion-based solvers for QBF.
Cite as

Michael Hartisch and Leroy Chew. An Expansion-Based Approach for Quantified Integer Programming. In 31st International Conference on Principles and Practice of Constraint Programming (CP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 340, pp. 12:1-12:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{hartisch_et_al:LIPIcs.CP.2025.12,
  author =	{Hartisch, Michael and Chew, Leroy},
  title =	{{An Expansion-Based Approach for Quantified Integer Programming}},
  booktitle =	{31st International Conference on Principles and Practice of Constraint Programming (CP 2025)},
  pages =	{12:1--12:26},
  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.12},
  URN =		{urn:nbn:de:0030-drops-238736},
  doi =		{10.4230/LIPIcs.CP.2025.12},
  annote =	{Keywords: Quantified Integer Programming, Quantified Constraint Satisfaction, Robust Discrete Optimization, Expansion, CEGAR}
}
Document
DOI: 10.4230/LIPIcs.CP.2025.15
Symmetric Core Learning for Pseudo-Boolean Optimization by Implicit Hitting Sets

Authors: Hannes Ihalainen, Jeremias Berg, Matti Järvisalo, and Bart Bogaerts

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

Abstract
We propose symmetric core learning (SCL) as a novel approach to making the implicit hitting set approach (IHS) to constraint optimization more symmetry-aware. SCL has the potential of significantly reducing the number of iterations and, in particular, the number of calls to an NP decision solver for extracting individual unsatisfiable cores. As the technique is focused on generating symmetric cores to the hitting set component of IHS, SCL is generally applicable in IHS-style search for essentially any constraint optimization paradigm. In this work, we focus in particular on integrating SCL to IHS for pseudo-Boolean optimization (PBO), as earlier proposed static symmetry breaking through lex-leader constraints generated before search turns out to often degrade the performance of the IHS approach to PBO. In contrast, we show that SCL can improve the runtime performance of a state-of-the-art IHS approach to PBO and generally does not impose significant overhead in terms of runtime performance.
Cite as

Hannes Ihalainen, Jeremias Berg, Matti Järvisalo, and Bart Bogaerts. Symmetric Core Learning for Pseudo-Boolean Optimization by Implicit Hitting Sets. In 31st International Conference on Principles and Practice of Constraint Programming (CP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 340, pp. 15:1-15:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{ihalainen_et_al:LIPIcs.CP.2025.15,
  author =	{Ihalainen, Hannes and Berg, Jeremias and J\"{a}rvisalo, Matti and Bogaerts, Bart},
  title =	{{Symmetric Core Learning for Pseudo-Boolean Optimization by Implicit Hitting Sets}},
  booktitle =	{31st International Conference on Principles and Practice of Constraint Programming (CP 2025)},
  pages =	{15:1--15:26},
  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.15},
  URN =		{urn:nbn:de:0030-drops-238767},
  doi =		{10.4230/LIPIcs.CP.2025.15},
  annote =	{Keywords: Implicit hitting sets, symmetries, unsatisfiable cores, pseudo-Boolean optimization}
}
Document
DOI: 10.4230/LIPIcs.SAT.2025.11
Better Extension Variables in DQBF via Independence

Authors: Leroy Chew and Tomáš Peitl

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

Abstract
We show that extension variables in (D)QBF can be generalised by conditioning on universal assignments. The benefit of this is that the dependency sets of such conditioned extension variables can be made smaller to allow easier refutations. This simple modification instantly solves many challenges in p-simulating the QBF expansion rule, which cannot be p-simulated in proof systems that have strategy extraction [Leroy Chew and Judith Clymo, 2020]. Simulating expansion is even more crucial in DQBF, where other methods are incomplete. In this paper we provide an overview of the strength of this new independent extension rule. We find that a new version of Extended Frege called IndExtFrege + ∀red can p-simulate a multitude of difficult QBF and DQBF techniques, even techniques that are difficult to approach with eFrege + ∀red. We show five p-simulations, that IndExtFrege + ∀red p-simulates QRAT, DQBF-IR-calc, IR(𝒟^rrs)-calc, Fork-Resolution and DQRAT which together underpin most DQBF solving and preprocessing techniques. The p-simulations work despite these systems using complicated rules and our new extension rule being relatively simple. Moreover, unlike recent p-simulations by eFrege + ∀red we can simulate the proof rules line by line, which allows us to mix QBF rules more easily with other inference steps.
Cite as

Leroy Chew and Tomáš Peitl. Better Extension Variables in DQBF via Independence. In 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 341, pp. 11:1-11:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{chew_et_al:LIPIcs.SAT.2025.11,
  author =	{Chew, Leroy and Peitl, Tom\'{a}\v{s}},
  title =	{{Better Extension Variables in DQBF via Independence}},
  booktitle =	{28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)},
  pages =	{11:1--11:24},
  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.11},
  URN =		{urn:nbn:de:0030-drops-237453},
  doi =		{10.4230/LIPIcs.SAT.2025.11},
  annote =	{Keywords: DQBF, QBF, Proof Systems, Dependency Schemes, RAT, Extended Frege, Skolem functions}
}
Document
DOI: 10.4230/LIPIcs.SAT.2025.7
Redundancy Rules for MaxSAT

Authors: Ilario Bonacina, Maria Luisa Bonet, Sam Buss, and Massimo Lauria

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

Abstract
The concept of redundancy in SAT leads to more expressive and powerful proof search techniques, e.g., able to express various inprocessing techniques, and originates interesting hierarchies of proof systems [Heule et.al'20, Buss-Thapen'19]. Redundancy has also been integrated in MaxSAT [Ihalainen et.al'22, Berg et.al'23, Bonacina et.al'24]. In this paper, we define a structured hierarchy of redundancy proof systems for MaxSAT, with the goal of studying its proof complexity. We obtain MaxSAT variants of proof systems such as SPR, PR, SR, and others, previously defined for SAT. All our rules are polynomially checkable, unlike [Ihalainen et.al'22]. Moreover, they are simpler and weaker than [Berg et.al'23], and possibly amenable to lower bounds. This work also complements the approach of [Bonacina et.al'24]. Their proof systems use different rule sets for soft and hard clauses, while here we propose a system using only hard clauses and blocking variables. This is easier to integrate with current solvers and proof checkers. We discuss the strength of the systems introduced, we show some limitations of them, and we give a short cost-SR proof that any assignment for the weak pigeonhole principle PHP^m_n falsifies at least m-n clauses.
Cite as

Ilario Bonacina, Maria Luisa Bonet, Sam Buss, and Massimo Lauria. Redundancy Rules for MaxSAT. In 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 341, pp. 7:1-7:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{bonacina_et_al:LIPIcs.SAT.2025.7,
  author =	{Bonacina, Ilario and Bonet, Maria Luisa and Buss, Sam and Lauria, Massimo},
  title =	{{Redundancy Rules for MaxSAT}},
  booktitle =	{28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)},
  pages =	{7:1--7:17},
  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.7},
  URN =		{urn:nbn:de:0030-drops-237411},
  doi =		{10.4230/LIPIcs.SAT.2025.7},
  annote =	{Keywords: MaxSAT, Redundancy Rules, Pigeonhole Principle}
}
Document
DOI: 10.4230/LIPIcs.SAT.2025.22
Enumerating All Boolean Matches

Authors: Alexander Nadel and Yogev Shalmon

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

Abstract
Boolean matching, a fundamental problem in circuit design, determines whether two Boolean circuits are equivalent under input/output permutations and negations. While most works focus on finding a single match or proving its absence, the problem of enumerating all matches remains largely unexplored, with BooM being a notable exception. Motivated by timing challenges in Intel’s library mapping flow, we introduce EBat - an open-source tool for enumerating all matches between single-output circuits. Built from scratch, EBat reuses BooM’s SAT encoding and introduces novel high-level algorithms and performance-critical subroutines to efficiently identify and block multiple mismatches and matches simultaneously. Experiments demonstrate that EBat substantially outperforms BooM’s baseline algorithm, solving 3 to 4 times more benchmarks within a given time limit. EBat has been productized as part of Intel’s library mapping flow, effectively addressing the timing challenges.
Cite as

Alexander Nadel and Yogev Shalmon. Enumerating All Boolean Matches. In 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 341, pp. 22:1-22:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{nadel_et_al:LIPIcs.SAT.2025.22,
  author =	{Nadel, Alexander and Shalmon, Yogev},
  title =	{{Enumerating All Boolean Matches}},
  booktitle =	{28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)},
  pages =	{22:1--22: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.22},
  URN =		{urn:nbn:de:0030-drops-237568},
  doi =		{10.4230/LIPIcs.SAT.2025.22},
  annote =	{Keywords: Boolean Matching, All-Boolean-Matching, Enumeration, SAT, Generalization}
}
  • Refine by Type
  • 45 Document/PDF
  • 28 Document/HTML

  • Refine by Publication Year
  • 25 2025
  • 5 2023
  • 3 2022
  • 2 2017
  • 1 2016
  • Show More...

  • Refine by Author
  • 2 Chew, Leroy
  • 2 Dahlke, Stephan
  • 2 Diehl, Stephan
  • 2 Dumbrava, Stefania
  • 2 Lissandrini, Matteo
  • Show More...

  • Refine by Series/Journal
  • 26 LIPIcs
  • 1 OASIcs
  • 5 LITES
  • 5 TGDK
  • 1 DagRep
  • Show More...

  • Refine by Classification
  • 3 Theory of computation → Constraint and logic programming
  • 3 Theory of computation → Fixed parameter tractability
  • 3 Theory of computation → Logic
  • 2 Applied computing → Psychology
  • 2 Information systems → Graph-based database models
  • Show More...

  • Refine by Keyword
  • 4 parameterized complexity
  • 2 DNA
  • 2 RNA
  • 2 SAT
  • 2 SMT
  • 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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact