Search Results

Documents authored by Gründel, Marlene


Document
The Descriptive Complexity of Relation Modification Problems

Authors: Florian Chudigiewitsch, Marlene Gründel, Christian Komusiewicz, Nils Morawietz, and Till Tantau

Published in: LIPIcs, Volume 386, 51st International Symposium on Mathematical Foundations of Computer Science (MFCS 2026)


Abstract
A relation modification problem gets a logical structure and a natural number k as input and asks whether k modifications of the structure suffice to make it satisfy a predefined property. We provide a complete classification of the classical and parameterized complexity of relation modification problems - the latter w. r. t. the modification budget k - based on the descriptive complexity of the respective target property. We consider different types of logical structures on which modifications are performed: Whereas monadic structures and undirected graphs without self-loops each yield their own complexity landscapes, we find that modifying undirected graphs with self-loops, directed graphs, or arbitrary logical structures is equally hard w. r. t. quantifier patterns. Moreover, we observe that all classes of problems considered in this paper are subject to a strong dichotomy in the sense that they are either very easy to solve (that is, they lie in para-AC^{0↑} or TC^0) or intractable (that is, they contain W[2]-hard or NP-hard problems).

Cite as

Florian Chudigiewitsch, Marlene Gründel, Christian Komusiewicz, Nils Morawietz, and Till Tantau. The Descriptive Complexity of Relation Modification Problems. In 51st International Symposium on Mathematical Foundations of Computer Science (MFCS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 386, pp. 93:1-93:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)


Copy BibTex To Clipboard

@InProceedings{chudigiewitsch_et_al:LIPIcs.MFCS.2026.93,
  author =	{Chudigiewitsch, Florian and Gr\"{u}ndel, Marlene and Komusiewicz, Christian and Morawietz, Nils and Tantau, Till},
  title =	{{The Descriptive Complexity of Relation Modification Problems}},
  booktitle =	{51st International Symposium on Mathematical Foundations of Computer Science (MFCS 2026)},
  pages =	{93:1--93:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-442-0},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{386},
  editor =	{Kouck\'{y}, Michal and Petrișan, Daniela},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2026.93},
  URN =		{urn:nbn:de:0030-drops-274752},
  doi =		{10.4230/LIPIcs.MFCS.2026.93},
  annote =	{Keywords: graph problems, descriptive complexity, edge modification, parameterized complexity, circuit complexity}
}
Document
Bilateral Treewidth for QBF: Where Strategies and Resolution Meet

Authors: Robert Ganian and Marlene Gründel

Published in: LIPIcs, Volume 377, 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)


Abstract
Treewidth is a well-studied decompositional parameter to measure the tree-likeness of a graph. While the propositional satisfiability problem (Sat) is known to be tractable when parameterized by the treewidth of the underlying primal graph, the evaluation of quantified Boolean formulas (QBFs) remains PSPACE-complete even on formulas of constant treewidth. Intuitively, this is because ordinary treewidth does not take into account the prefix of the QBF: it neither distinguishes between existential and universal variables, nor accounts for the order in which they are quantified. In the past, several weaker variants of treewidth have been devised to incorporate prefix-sensitive information. To establish tractability for QBFs under these notions, prior work has employed either strategy- or resolution-based techniques, thereby dividing the parameterized complexity landscape of QBF into two regimes that are incomparable in strength. We establish fixed-parameter tractability with respect to bilateral treewidth, a novel and strictly more powerful decompositional parameter that combines these rivaling approaches by simultaneously allowing for branching on strategies and performing Q-resolution. As in previous works in this direction, our algorithm assumes that a suitable tree decomposition is provided on the input.

Cite as

Robert Ganian and Marlene Gründel. Bilateral Treewidth for QBF: Where Strategies and Resolution Meet. In 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 377, pp. 16:1-16:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)


Copy BibTex To Clipboard

@InProceedings{ganian_et_al:LIPIcs.SAT.2026.16,
  author =	{Ganian, Robert and Gr\"{u}ndel, Marlene},
  title =	{{Bilateral Treewidth for QBF: Where Strategies and Resolution Meet}},
  booktitle =	{29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)},
  pages =	{16:1--16:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-431-4},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{377},
  editor =	{Ignatiev, Alexey and Szeider, Stefan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2026.16},
  URN =		{urn:nbn:de:0030-drops-263227},
  doi =		{10.4230/LIPIcs.SAT.2026.16},
  annote =	{Keywords: QBF, Treewidth, Fixed Parameter Tractability, Dependency Schemes}
}

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