34 Search Results for "Vollmer, Michael"

Document
DOI: 10.4230/LIPIcs.STACS.2026.63
Generalised Quantifiers Based on Rabin-Mostowski Index

Authors: Denis Kuperberg, Damian Niwiński, Paweł Parys, and Michał Skrzypczak

Published in: LIPIcs, Volume 364, 43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026)

Abstract
In this work we introduce new generalised quantifiers which allow us to express the Rabin-Mostowski index of automata. Our main results study expressive power and decidability of the monadic second-order (MSO) logic extended with these quantifiers. We study these problems in the realm of both ω-words and infinite trees. As it turns out, the pictures in these two cases are very different. In the case of ω-words the new quantifiers can be effectively expressed in pure MSO logic. In contrast, in the case of infinite trees, addition of these quantifiers leads to an undecidable formalism. To realise index-quantifier elimination, we consider the extension of MSO by game quantifiers. As a tool, we provide a specific quantifier-elimination procedure for them. Moreover, we introduce a novel construction of transducers realising strategies in ω-regular games with monadic parameters.
Cite as

Denis Kuperberg, Damian Niwiński, Paweł Parys, and Michał Skrzypczak. Generalised Quantifiers Based on Rabin-Mostowski Index. In 43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 364, pp. 63:1-63:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{kuperberg_et_al:LIPIcs.STACS.2026.63,
  author =	{Kuperberg, Denis and Niwi\'{n}ski, Damian and Parys, Pawe{\l} and Skrzypczak, Micha{\l}},
  title =	{{Generalised Quantifiers Based on Rabin-Mostowski Index}},
  booktitle =	{43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026)},
  pages =	{63:1--63:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-412-3},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{364},
  editor =	{Mahajan, Meena and Manea, Florin and McIver, Annabelle and Thắng, Nguy\~{ê}n Kim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2026.63},
  URN =		{urn:nbn:de:0030-drops-255526},
  doi =		{10.4230/LIPIcs.STACS.2026.63},
  annote =	{Keywords: monadic quantifiers, decidability, quantifier elimination, parity automata, game quantifier, Rabin-Mostowski index}
}
Document
DOI: 10.4230/LIPIcs.STACS.2026.41
On the Complexity of Computing Strahler Numbers

Authors: Moses Ganardi and Markus Lohrey

Published in: LIPIcs, Volume 364, 43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026)

Abstract
It is shown that the problem of computing the Strahler number of a binary tree given as a term is complete for the circuit complexity class uniform NC¹. For several variants, where the binary tree is given by a pointer structure or in a succinct form by a directed acyclic graph or a tree straight-line program, the complexity of computing the Strahler number is determined as well. The problem, whether a given context-free grammar in Chomsky normal form produces a derivation tree (resp., an acyclic derivation tree), whose Strahler number is at least a given number k is shown to be P-complete (resp., PSPACE-complete).
Cite as

Moses Ganardi and Markus Lohrey. On the Complexity of Computing Strahler Numbers. In 43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 364, pp. 41:1-41:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{ganardi_et_al:LIPIcs.STACS.2026.41,
  author =	{Ganardi, Moses and Lohrey, Markus},
  title =	{{On the Complexity of Computing Strahler Numbers}},
  booktitle =	{43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026)},
  pages =	{41:1--41:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-412-3},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{364},
  editor =	{Mahajan, Meena and Manea, Florin and McIver, Annabelle and Thắng, Nguy\~{ê}n Kim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2026.41},
  URN =		{urn:nbn:de:0030-drops-255301},
  doi =		{10.4230/LIPIcs.STACS.2026.41},
  annote =	{Keywords: Strahler number, circuit complexity classes, context-free grammars}
}
Document
DOI: 10.4230/LIPIcs.IPEC.2025.23
Enumeration Kernels for Vertex Cover and Feedback Vertex Set

Authors: Marin Bougeret, Guilherme C. M. Gomes, Vinicius F. dos Santos, and Ignasi Sau

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

Abstract
Enumerative kernelization is a recent and promising area sitting at the intersection of parameterized complexity and enumeration algorithms. Its study began with the paper of Creignou et al. [Theory Comput. Syst., 2017], and development in the area has started to accelerate with the work of Golovach et al. [J. Comput. Syst. Sci., 2022]. The latter introduced polynomial-delay enumeration kernels and applied them in the study of structural parameterizations of the Matching Cut problem and some variants. Few other results, mostly on Longest Path and some generalizations of Matching Cut, have also been developed. However, little success has been seen in enumeration versions of Vertex Cover and Feedback Vertex Set, some of the most studied problems in kernelization. In this paper, we address this shortcoming. Our first result is a polynomial-delay enumeration kernel with 2k vertices for Enum Vertex Cover, where we wish to list all solutions with at most k vertices. This is obtained by developing a non-trivial lifting algorithm for the classical crown decomposition reduction rule, and directly improves upon the kernel with 𝒪(k²) vertices derived from the work of Creignou et al. Our other result is a polynomial-delay enumeration kernel with 𝒪(k³) vertices and edges for Enum Feedback Vertex Set; the proof is inspired by some ideas of Thomassé [TALG, 2010], but with a weaker bound on the kernel size due to difficulties in applying the q-expansion technique.
Cite as

Marin Bougeret, Guilherme C. M. Gomes, Vinicius F. dos Santos, and Ignasi Sau. Enumeration Kernels for Vertex Cover and Feedback Vertex Set. In 20th International Symposium on Parameterized and Exact Computation (IPEC 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 358, pp. 23:1-23:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{bougeret_et_al:LIPIcs.IPEC.2025.23,
  author =	{Bougeret, Marin and C. M. Gomes, Guilherme and dos Santos, Vinicius F. and Sau, Ignasi},
  title =	{{Enumeration Kernels for Vertex Cover and Feedback Vertex Set}},
  booktitle =	{20th International Symposium on Parameterized and Exact Computation (IPEC 2025)},
  pages =	{23:1--23:18},
  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.23},
  URN =		{urn:nbn:de:0030-drops-251552},
  doi =		{10.4230/LIPIcs.IPEC.2025.23},
  annote =	{Keywords: Kernelization, Enumeration, Vertex cover, Crown decomposition, Feedback vertex set}
}
Document
DOI: 10.4230/LIPIcs.IPEC.2025.27
Uniformity Within Parameterized Circuit Classes

Authors: Steef Hegeman, Jan Martens, and Alfons Laarman

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

Abstract
We study uniformity conditions for parameterized Boolean circuit families. Uniformity conditions require that the infinitely many circuits in a circuit family are in some sense easy to construct from one shared description. For shallow circuit families, logtime-uniformity is often desired but quite technical to prove. Despite that, proving it is often left as an exercise for the reader - even for recently introduced classes in parameterized circuit complexity, where uniformity conditions have not yet been explicitly studied. We formally define parameterized versions of linear-uniformity, logtime-uniformity, and FO-uniformity, and prove that these result in equivalent complexity classes when imposed on para-AC⁰ and para-AC^{0↑}. Overall, we provide a convenient way to verify uniformity for shallow parameterized circuit classes, and thereby substantiate claims of uniformity in the literature.
Cite as

Steef Hegeman, Jan Martens, and Alfons Laarman. Uniformity Within Parameterized Circuit Classes. In 20th International Symposium on Parameterized and Exact Computation (IPEC 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 358, pp. 27:1-27:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{hegeman_et_al:LIPIcs.IPEC.2025.27,
  author =	{Hegeman, Steef and Martens, Jan and Laarman, Alfons},
  title =	{{Uniformity Within Parameterized Circuit Classes}},
  booktitle =	{20th International Symposium on Parameterized and Exact Computation (IPEC 2025)},
  pages =	{27:1--27:16},
  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.27},
  URN =		{urn:nbn:de:0030-drops-251598},
  doi =		{10.4230/LIPIcs.IPEC.2025.27},
  annote =	{Keywords: Parameterized complexity, circuit complexity, uniformity, descriptive complexity}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.FSTTCS.2025.2
Unboundedness Problems for Formal Languages (Invited Talk)

Authors: Georg Zetzsche

Published in: LIPIcs, Volume 360, 45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025)

Abstract
Informally, unboundedness problems are decision problems that ask about the existence of infinitely many words (satisfying certain properties) in a formal language. For example: Is a given language infinite? Or: Does a given language have super-polynomial growth? These came into focus in recent years because of their connections to downward closure computation and separability problems. Although unboundedness problems may seem difficult at first, it turns out that there are techniques that are at the same time conceptually very simple, but also apply to a surprisingly wide variety of language classes. The talk will survey recent results (and techniques) concerning unboundedness problems.
Cite as

Georg Zetzsche. Unboundedness Problems for Formal Languages (Invited Talk). In 45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 360, pp. 2:1-2:10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{zetzsche:LIPIcs.FSTTCS.2025.2,
  author =	{Zetzsche, Georg},
  title =	{{Unboundedness Problems for Formal Languages}},
  booktitle =	{45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025)},
  pages =	{2:1--2:10},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-406-2},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{360},
  editor =	{Aiswarya, C. and Mehta, Ruta and Roy, Subhajit},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2025.2},
  URN =		{urn:nbn:de:0030-drops-250810},
  doi =		{10.4230/LIPIcs.FSTTCS.2025.2},
  annote =	{Keywords: Decidability, formal languages, unifying frameworks, downward closure, separability}
}
Document
DOI: 10.4230/LIPIcs.ISAAC.2025.25
Structural Parameterizations of Simultaneous Planarity

Authors: Thomas Depian, Simon D. Fink, Alexander Firbas, Robert Ganian, Matthias Pfretzschner, and Ignaz Rutter

Published in: LIPIcs, Volume 359, 36th International Symposium on Algorithms and Computation (ISAAC 2025)

Abstract
Given a set of graphs on the same vertex set, the problem Simultaneous Embedding With Fixed Edges (SEFE) asks, whether there exist planar drawings of all input graphs, such that every pair of drawings coincides on their shared subgraph. It is known that SEFE is NP-complete [Elisabeth Gassner et al., 2006], even in the so-called sunflower case, where all pairs of input graphs have the same shared graph G_∩ [Marcus Schaefer, 2012]. Fink, Pfretzschner, and Rutter [Simon D. Fink et al., 2023] recently initiated the study of the parameterized complexity of SEFE in the sunflower case, mainly focusing on structural parameters of G_∩. In this work, we shift the focus towards parameters of the union graph G_∪ that contains the edges of all input graphs. On the positive side, we establish fixed-parameter tractability for the problem with respect to the feedback edge set number of G_∪. We complement this result by showing that it, surprisingly, remains NP-complete even if G_∪ has constant vertex cover number. These results settle two open questions posed by Fink et al. [Simon D. Fink et al., 2023].
Cite as

Thomas Depian, Simon D. Fink, Alexander Firbas, Robert Ganian, Matthias Pfretzschner, and Ignaz Rutter. Structural Parameterizations of Simultaneous Planarity. In 36th International Symposium on Algorithms and Computation (ISAAC 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 359, pp. 25:1-25:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{depian_et_al:LIPIcs.ISAAC.2025.25,
  author =	{Depian, Thomas and Fink, Simon D. and Firbas, Alexander and Ganian, Robert and Pfretzschner, Matthias and Rutter, Ignaz},
  title =	{{Structural Parameterizations of Simultaneous Planarity}},
  booktitle =	{36th International Symposium on Algorithms and Computation (ISAAC 2025)},
  pages =	{25:1--25:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-408-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{359},
  editor =	{Chen, Ho-Lin and Hon, Wing-Kai and Tsai, Meng-Tsung},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ISAAC.2025.25},
  URN =		{urn:nbn:de:0030-drops-249332},
  doi =		{10.4230/LIPIcs.ISAAC.2025.25},
  annote =	{Keywords: SEFE, Simultaneous Planarity, Fixed-Parameter Tractability, NP-hardness}
}
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}
}
Artifact
Software
DOI: 10.4230/artifacts.23907
dcastrop/coq-hylomorphisms

Authors: David Castro Perez, Marco Paviotti, and Michael Vollmer

Abstract
Cite as

David Castro Perez, Marco Paviotti, Michael Vollmer. dcastrop/coq-hylomorphisms (Software, Source Code). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@misc{dagstuhl-artifact-23907,
   title = {{dcastrop/coq-hylomorphisms}}, 
   author = {Castro Perez, David and Paviotti, Marco and Vollmer, Michael},
   note = {Software, EP/Y00339X/1, EP/T014512/1, swhId: \href{https://archive.softwareheritage.org/swh:1:dir:72a5871702972010658c8b75970475a540abf44d;origin=https://github.com/dcastrop/coq-hylomorphisms;visit=swh:1:snp:3033a9703c61e14e58b51c7f66c784b9955e737f;anchor=swh:1:rev:305c425fdd165254bbf1bee47ed9d44d6b93fa3c}{\texttt{swh:1:dir:72a5871702972010658c8b75970475a540abf44d}} (visited on 2025-09-22)},
   url = {https://github.com/dcastrop/coq-hylomorphisms},
   doi = {10.4230/artifacts.23907},
}
Document
DOI: 10.4230/LIPIcs.ITP.2025.32
Program Optimisations via Hylomorphisms for Extraction of Executable Code

Authors: David Castro Perez, Marco Paviotti, and Michael Vollmer

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

Abstract
Generic programming with recursion schemes provides a powerful abstraction for structuring recursion and provides a rigorous reasoning principle for program optimisations which have been successfully applied to compilers for functional languages. Formalising recursion schemes in a type theory offers additional termination guarantees, but it often requires compromising on performance, requiring the assumption of additional axioms, and/or introducing unsafe casts into extracted code. This paper presents the first Rocq formalisation of hylomorphisms allowing for the mechanisation of all recognised recursive algorithms. The key contribution of this paper is that this formalisation is fully axiom-free, and it allows the extraction of safe, idiomatic functional code. We exemplify the framework by formalising a series of algorithms based on different recursive paradigms such as divide-and conquer, dynamic programming, and mutual recursion and demonstrate that the extracted functional code for the programs formalised in our framework is efficient, humanly readable, and runnable. Furthermore, we show the use of the machine-checked proofs of the laws of hylomorphisms to do program optimisations.
Cite as

David Castro Perez, Marco Paviotti, and Michael Vollmer. Program Optimisations via Hylomorphisms for Extraction of Executable Code. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 32:1-32:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{castroperez_et_al:LIPIcs.ITP.2025.32,
  author =	{Castro Perez, David and Paviotti, Marco and Vollmer, Michael},
  title =	{{Program Optimisations via Hylomorphisms for Extraction of Executable Code}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{32:1--32:20},
  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.32},
  URN =		{urn:nbn:de:0030-drops-246302},
  doi =		{10.4230/LIPIcs.ITP.2025.32},
  annote =	{Keywords: hylomorphisms, program calculation, divide and conquer, fusion}
}
Document
DOI: 10.4230/LIPIcs.TQC.2025.6
Quantum SAT Problems with Finite Sets of Projectors Are Complete for a Plethora of Classes

Authors: Ricardo Rivera Cardoso, Alex Meiburg, and Daniel Nagaj

Published in: LIPIcs, Volume 350, 20th Conference on the Theory of Quantum Computation, Communication and Cryptography (TQC 2025)

Abstract
Previously, all known variants of the Quantum Satisfiability (QSAT) problem - consisting of determining whether a k-local (k-body) Hamiltonian is frustration-free - could be classified as being either in 𝖯; or complete for NP, MA, or QMA₁. Here, we present new qubit variants of this problem that are complete for BQP₁, coRP, QCMA, PI(coRP,NP), PI(BQP₁,NP), PI(BQP₁,MA), SoPU(coRP,NP), SoPU(BQP₁,NP), and SoPU(BQP₁,MA). Our result implies that a complete classification of quantum constraint satisfaction problems (QCSPs), analogous to Schaefer’s dichotomy theorem for classical CSPs, must either include these 13 classes, or otherwise show that some are equal. Additionally, our result showcases two new types of QSAT problems that can be decided efficiently, as well as the first nontrivial BQP₁-complete problem. We first construct QSAT problems on qudits that are complete for BQP₁, coRP, and QCMA. These are made by restricting the finite set of Hamiltonians to consist of elements similar to H_{init}, H_{prop}, and H_{out}, seen in the circuit-to-Hamiltonian transformation. Usually, these are used to demonstrate hardness of QSAT and Local Hamiltonian problems, and so our proofs of hardness are simple. The difficulty lies in ensuring that all Hamiltonians generated with these three elements can be decided in their respective classes. For this, we build our Hamiltonian terms with high-dimensional data and clock qudits, ternary logic, and either monogamy of entanglement or specific clock encodings. We then show how to express these problems in terms of qubits, by proving that any QCSP can be reduced to a qubit problem while maintaining the same complexity - something not believed possible classically. The remaining six problems are obtained by considering "sums" and "products" of some of the QSAT problems mentioned here. Before this work, the QSAT problems generated in this way resulted in complete problems for PI and SoPU classes that were trivially equal to NP, MA, or QMA₁. We thus commence the study of these new and seemingly nontrivial classes. While [Meiburg, 2021] first sought to prove completeness for coRP, BQP₁, and QCMA, we note that those constructions are flawed. Here, we rework them, provide correct proofs, and obtain improvements on the required qudit dimensionality.
Cite as

Ricardo Rivera Cardoso, Alex Meiburg, and Daniel Nagaj. Quantum SAT Problems with Finite Sets of Projectors Are Complete for a Plethora of Classes. In 20th Conference on the Theory of Quantum Computation, Communication and Cryptography (TQC 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 350, pp. 6:1-6:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{riveracardoso_et_al:LIPIcs.TQC.2025.6,
  author =	{Rivera Cardoso, Ricardo and Meiburg, Alex and Nagaj, Daniel},
  title =	{{Quantum SAT Problems with Finite Sets of Projectors Are Complete for a Plethora of Classes}},
  booktitle =	{20th Conference on the Theory of Quantum Computation, Communication and Cryptography (TQC 2025)},
  pages =	{6:1--6:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-392-8},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{350},
  editor =	{Fefferman, Bill},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TQC.2025.6},
  URN =		{urn:nbn:de:0030-drops-240557},
  doi =		{10.4230/LIPIcs.TQC.2025.6},
  annote =	{Keywords: Quantum complexity theory, quantum satisfiability, circuit-to-Hamiltonian, pairwise union of classes, pairwise intersection of classes}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2025.6
Catalytic Computing and Register Programs Beyond Log-Depth

Authors: Yaroslav Alekseev, Yuval Filmus, Ian Mertz, Alexander Smal, and Antoine Vinciguerra

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

Abstract
In a seminal work, Buhrman et al. (STOC 2014) defined the class CSPACE(s,c) of problems solvable in space s with an additional catalytic tape of size c, which is a tape whose initial content must be restored at the end of the computation. They showed that uniform TC¹ circuits are computable in catalytic logspace, i.e., CL = CSPACE(O(log{n}), 2^{O(log{n})}), thus giving strong evidence that catalytic space gives L strict additional power. Their study focuses on an arithmetic model called register programs, which has been a focal point in development since then. Understanding CL remains a major open problem, as TC¹ remains the most powerful containment to date. In this work, we study the power of catalytic space and register programs to compute circuits of larger depth. Using register programs, we show that for every ε > 0, SAC² ⊆ CSPACE (O((log²n)/(log log n)), 2^{O(log^{1+ε} n)}) . On the other hand, we know that SAC² ⊆ TC² ⊆ CSPACE(O(log²{n}) , 2^{O(log{n})}). Our result thus shows an O(log log n) factor improvement on the free space needed to compute SAC², at the expense of a nearly-polynomial-sized catalytic tape. We also exhibit non-trivial register programs for matrix powering, which is a further step towards showing NC² ⊆ CL.
Cite as

Yaroslav Alekseev, Yuval Filmus, Ian Mertz, Alexander Smal, and Antoine Vinciguerra. Catalytic Computing and Register Programs Beyond Log-Depth. In 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 345, pp. 6:1-6:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{alekseev_et_al:LIPIcs.MFCS.2025.6,
  author =	{Alekseev, Yaroslav and Filmus, Yuval and Mertz, Ian and Smal, Alexander and Vinciguerra, Antoine},
  title =	{{Catalytic Computing and Register Programs Beyond Log-Depth}},
  booktitle =	{50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)},
  pages =	{6:1--6: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.6},
  URN =		{urn:nbn:de:0030-drops-241136},
  doi =		{10.4230/LIPIcs.MFCS.2025.6},
  annote =	{Keywords: catalytic computing, circuit classes, polynomial method}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2025.38
The Complexity of Separability for Semilinear Sets and Parikh Automata

Authors: Elias Rojas Collins, Chris Köcher, and Georg Zetzsche

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

Abstract
In a separability problem, we are given two sets K and L from a class 𝒞, and we want to decide whether there exists a set S from a class 𝒮 such that K ⊆ S and S ∩ L = ∅. In this case, we speak of separability of sets in 𝒞 by sets in 𝒮. We study two types of separability problems. First, we consider separability of semilinear sets (i.e. subsets of ℕ^d for some d) by sets definable by quantifier-free monadic Presburger formulas (or equivalently, the recognizable subsets of ℕ^d). Here, a formula is monadic if each atom uses at most one variable. Second, we consider separability of languages of Parikh automata by regular languages. A Parikh automaton is a machine with access to counters that can only be incremented, and have to meet a semilinear constraint at the end of the run. Both of these separability problems are known to be decidable with elementary complexity. Our main results are that both problems are coNP-complete. In the case of semilinear sets, coNP-completeness holds regardless of whether the input sets are specified by existential Presburger formulas, quantifier-free formulas, or semilinear representations. Our results imply that recognizable separability of rational subsets of Σ* × ℕ^d (shown decidable by Choffrut and Grigorieff) is coNP-complete as well. Another application is that regularity of deterministic Parikh automata (where the target set is specified using a quantifier-free Presburger formula) is coNP-complete as well.
Cite as

Elias Rojas Collins, Chris Köcher, and Georg Zetzsche. The Complexity of Separability for Semilinear Sets and Parikh Automata. In 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 345, pp. 38:1-38:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{collins_et_al:LIPIcs.MFCS.2025.38,
  author =	{Collins, Elias Rojas and K\"{o}cher, Chris and Zetzsche, Georg},
  title =	{{The Complexity of Separability for Semilinear Sets and Parikh Automata}},
  booktitle =	{50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)},
  pages =	{38:1--38:21},
  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.38},
  URN =		{urn:nbn:de:0030-drops-241457},
  doi =		{10.4230/LIPIcs.MFCS.2025.38},
  annote =	{Keywords: Vector Addition System, Separability, Regular Language}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2025.29
A Universal Uniform Approximation Theorem for Neural Networks

Authors: Olivier Bournez, Johanne Cohen, and Adrian Wurm

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

Abstract
We show the existence of a fixed recurrent network capable of approximating any computable function with arbitrary precision, provided that an encoding of the function is given in the initial input. While uniform approximation over a compact domain is a well-known property of neural networks, we go further by proving that our network ensures effective uniform approximation - simultaneously ensuring: - Uniform approximation in the sup-norm sense, guaranteeing precision across the compact domain {[0,1]^d}; - Uniformity in the sense of computability theory (also referred to as effectivity or universality), meaning the same network works for all computable functions. Our result is obtained constructively, using original arguments. Moreover, our construction bridges computation theory with neural network approximation, providing new insights into the fundamental connections between circuit complexity and function representation. Furthermore, this connection extends beyond computability to complexity theory. The obtained network is efficient: if a function is computable or approximable in polynomial time in the Turing machine model, then the network requires only a polynomial number of recurrences or iterations to achieve the same level of approximation, and conversely. Moreover, the recurrent network can be assumed to be very narrow, strengthening the link our results and existing models of very deep learning, where uniform approximation properties have already been established.
Cite as

Olivier Bournez, Johanne Cohen, and Adrian Wurm. A Universal Uniform Approximation Theorem for Neural Networks. In 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 345, pp. 29:1-29:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{bournez_et_al:LIPIcs.MFCS.2025.29,
  author =	{Bournez, Olivier and Cohen, Johanne and Wurm, Adrian},
  title =	{{A Universal Uniform Approximation Theorem for Neural Networks}},
  booktitle =	{50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)},
  pages =	{29:1--29:20},
  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.29},
  URN =		{urn:nbn:de:0030-drops-241365},
  doi =		{10.4230/LIPIcs.MFCS.2025.29},
  annote =	{Keywords: Models of computation, Complexity theory, Formal neural networks}
}
Document
Research
DOI: 10.4230/OASIcs.Grossi.19
Designing Output Sensitive Algorithms for Subgraph Enumeration

Authors: Alessio Conte, Kazuhiro Kurita, Andrea Marino, Giulia Punzi, Takeaki Uno, and Kunihiro Wasa

Published in: OASIcs, Volume 132, From Strings to Graphs, and Back Again: A Festschrift for Roberto Grossi's 60th Birthday (2025)

Abstract
The enumeration of all subgraphs respecting some structural property is a fundamental task in theoretical computer science, with practical applications in many branches of data mining and network analysis. It is often of interest to only consider solutions (subgraphs) that are maximal under inclusion, and to achieve output-sensitive complexity, i.e., bounding the running time with respect to the number of subgraphs produced. In this paper, we provide a survey of techniques for designing output-sensitive algorithms for subgraph enumeration, including partition-based approaches such as flashlight search, solution-graph traversal methods such as reverse search, and cost amortization strategies such as push-out amortization. We also briefly discuss classes of efficiency, hardness of enumeration, and variants such as approximate enumeration. The paper is meant as an accessible handbook for learning the basics of the field and as a practical reference for selecting state-of-the-art subgraph enumeration strategies fitting to one’s needs.
Cite as

Alessio Conte, Kazuhiro Kurita, Andrea Marino, Giulia Punzi, Takeaki Uno, and Kunihiro Wasa. Designing Output Sensitive Algorithms for Subgraph Enumeration. In From Strings to Graphs, and Back Again: A Festschrift for Roberto Grossi's 60th Birthday. Open Access Series in Informatics (OASIcs), Volume 132, pp. 19:1-19:40, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{conte_et_al:OASIcs.Grossi.19,
  author =	{Conte, Alessio and Kurita, Kazuhiro and Marino, Andrea and Punzi, Giulia and Uno, Takeaki and Wasa, Kunihiro},
  title =	{{Designing Output Sensitive Algorithms for Subgraph Enumeration}},
  booktitle =	{From Strings to Graphs, and Back Again: A Festschrift for Roberto Grossi's 60th Birthday},
  pages =	{19:1--19:40},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-391-1},
  ISSN =	{2190-6807},
  year =	{2025},
  volume =	{132},
  editor =	{Conte, Alessio and Marino, Andrea and Rosone, Giovanna and Vitter, Jeffrey Scott},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.Grossi.19},
  URN =		{urn:nbn:de:0030-drops-238180},
  doi =		{10.4230/OASIcs.Grossi.19},
  annote =	{Keywords: Graph algorithms, Graph enumeration, Output sensitive enumeration}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2025.162
Positive and Monotone Fragments of FO and LTL

Authors: Simon Iosti, Denis Kuperberg, and Quentin Moreau

Published in: LIPIcs, Volume 334, 52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025)

Abstract
We study the positive logic FO^+ on finite words, and its fragments, pursuing and refining the work initiated in [Denis Kuperberg, 2023]. First, we transpose notorious logic equivalences into positive first-order logic: FO^+ is equivalent to LTL^+, and its two-variable fragment FO^{2+} with (resp. without) successor available is equivalent to UTL^+ with (resp. without) the "next" operator X available. This shows that despite previous negative results, the class of FO^+-definable languages exhibits some form of robustness. We then exhibit an example of an FO-definable monotone language on one predicate, that is not FO^+-definable, refining the example from [Denis Kuperberg, 2023] with 3 predicates. Moreover, we show that such a counter-example cannot be FO²-definable. Finally, we provide a new example distinguishing the positive and monotone versions of FO² without quantifier alternation. This does not rely on a variant of the previously known counter-example, and witnesses a new phenomenon.
Cite as

Simon Iosti, Denis Kuperberg, and Quentin Moreau. Positive and Monotone Fragments of FO and LTL. In 52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 334, pp. 162:1-162:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{iosti_et_al:LIPIcs.ICALP.2025.162,
  author =	{Iosti, Simon and Kuperberg, Denis and Moreau, Quentin},
  title =	{{Positive and Monotone Fragments of FO and LTL}},
  booktitle =	{52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025)},
  pages =	{162:1--162:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-372-0},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{334},
  editor =	{Censor-Hillel, Keren and Grandoni, Fabrizio and Ouaknine, Jo\"{e}l and Puppis, Gabriele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2025.162},
  URN =		{urn:nbn:de:0030-drops-235398},
  doi =		{10.4230/LIPIcs.ICALP.2025.162},
  annote =	{Keywords: Positive logic, LTL, separation, first-order, monotone}
}
  • Refine by Type
  • 32 Document/PDF
  • 17 Document/HTML
  • 2 Artifact

  • Refine by Publication Year
  • 2 2026
  • 19 2025
  • 2 2024
  • 3 2023
  • 1 2019
  • Show More...

  • Refine by Author
  • 11 Vollmer, Michael
  • 3 Batty, Mark
  • 3 Koparkar, Chaitanya
  • 3 Kulkarni, Milind
  • 2 Castro Perez, David
  • Show More...

  • Refine by Series/Journal
  • 27 LIPIcs
  • 1 OASIcs
  • 2 DARTS
  • 2 DagSemProc

  • Refine by Classification
  • 4 Software and its engineering → Compilers
  • 4 Theory of computation → Circuit complexity
  • 3 Information systems → Data layout
  • 3 Mathematics of computing → Graph algorithms
  • 3 Theory of computation → Complexity classes
  • Show More...

  • Refine by Keyword
  • 4 Compilers
  • 2 CHERI
  • 2 Data layout optimization
  • 2 Dense data layout
  • 2 Memory Safety
  • 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