30 Search Results for "Berkholz, Christoph"

Document
DOI: 10.4230/LIPIcs.ICDT.2026.11
Factorised Representations of Join Queries: Tight Bounds and a New Dichotomy

Authors: Christoph Berkholz and Harry Vinall-Smeeth

Published in: LIPIcs, Volume 365, 29th International Conference on Database Theory (ICDT 2026)

Abstract
A common theme in factorised databases and knowledge compilation is the representation of solution sets in a useful yet succinct data structure. In this paper, we study the representation of the result of join queries (or, equivalently, the set of homomorphisms between two relational structures). We focus on the very general format of {∪,×}-circuits - also known as d-representations or DNNF circuits - and aim to find the limits of this approach. In prior work, it has been shown that there always exists a {∪,×}-circuit of size N^O(subw) representing the query result, where N is the size of the database and subw the submodular width of the query. If the arity of all relations is bounded by a constant, then subw is linear in the treewidth tw of the query. In this setting, the authors of this paper proved a lower bound of N^Ω(tw^ε) on the circuit size (ICALP 2023), where ε > 0 depends on the excluded grid theorem. Our first main contribution is to improve this lower bound to N^Ω(tw), which is tight up to a constant factor in the exponent. Our second contribution is a N^Ω(subw^{1/4}) lower bound on the circuit size for join queries over relations of unbounded arity. Both lower bounds are unconditional lower bounds on the circuit size for well-chosen database instances. Their proofs use a combination of structural (hyper)graph theory with communication complexity in a simple yet novel way. While the second lower bound is asymptotically equivalent to Marx’s conditional bound on the decision complexity (JACM 2013), our N^Θ(tw) bound in the bounded arity setting is tight, while the best conditional bound on the decision complexity is N^Ω(tw/log tw). Note that removing this logarithmic factor in the decision setting is a major open problem.
Cite as

Christoph Berkholz and Harry Vinall-Smeeth. Factorised Representations of Join Queries: Tight Bounds and a New Dichotomy. In 29th International Conference on Database Theory (ICDT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 365, pp. 11:1-11:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{berkholz_et_al:LIPIcs.ICDT.2026.11,
  author =	{Berkholz, Christoph and Vinall-Smeeth, Harry},
  title =	{{Factorised Representations of Join Queries: Tight Bounds and a New Dichotomy}},
  booktitle =	{29th International Conference on Database Theory (ICDT 2026)},
  pages =	{11:1--11:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-413-0},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{365},
  editor =	{ten Cate, Balder and Funk, Maurice},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICDT.2026.11},
  URN =		{urn:nbn:de:0030-drops-256255},
  doi =		{10.4230/LIPIcs.ICDT.2026.11},
  annote =	{Keywords: join queries, homomorphisms, factorised databases, succinct representation, knowledge compilation, lower bounds}
}
Document
DOI: 10.4230/LIPIcs.STACS.2026.22
Modular Counting over 3-Element and Conservative Domains

Authors: Andrei A. Bulatov and Amirhossein Kazeminia

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

Abstract
In the Constraint Satisfaction Problem (CSP for short) the goal is to decide the existence of a homomorphism from a given relational structure {G} to a given relational structure {H}. If the structure {H} is fixed and {G} is the only input, the problem is denoted CSP({H}). In its counting version, #CSP({H}), the task is to find the number of such homomorphisms. The CSP and #CSP have been used to model a wide variety of combinatorial problems and have received a tremendous amount of attention from researchers from multiple disciplines. In this paper we consider the modular version of the counting CSPs, that is, problems of the form #_pCSP({H}) of counting the number of homomorphisms to {H} modulo a fixed prime number p. Modular counting has been intensively studied during the last decade, although mainly in the case of graph homomorphisms. Here we continue the program of systematic research of modular counting of homomorphisms to general relational structures. The main results of the paper include a new way of reducing modular counting problems to smaller domains and a study of the complexity of such problems over 3-element domains and over conservative domains, that is, relational structures that allow to express (in a certain exact way) every possible unary predicate.
Cite as

Andrei A. Bulatov and Amirhossein Kazeminia. Modular Counting over 3-Element and Conservative Domains. In 43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 364, pp. 22:1-22:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{bulatov_et_al:LIPIcs.STACS.2026.22,
  author =	{Bulatov, Andrei A. and Kazeminia, Amirhossein},
  title =	{{Modular Counting over 3-Element and Conservative Domains}},
  booktitle =	{43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026)},
  pages =	{22:1--22:20},
  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.22},
  URN =		{urn:nbn:de:0030-drops-255114},
  doi =		{10.4230/LIPIcs.STACS.2026.22},
  annote =	{Keywords: Constraint Satisfaction Problem, Modular Counting}
}
Document
DOI: 10.4230/LIPIcs.CSL.2026.35
Boolean Basis and Succinctness of Modal Logic via Hella-Vilander Games

Authors: Sebastian Pfau

Published in: LIPIcs, Volume 363, 34th EACSL Annual Conference on Computer Science Logic (CSL 2026)

Abstract
The Hella-Vilander game for modal logic is a model comparison game that captures the formula size necessary to separate sets of pointed Kripke structures. We introduce the ℳ-ON game as a modification of this game. Our game captures the necessary number of modal operators, i.e., ◇ and □ instead of formula size. We use our game to show that the bi-implication ↔, sometimes also called equivalence, enables us to write modal logic formula with significantly fewer modal operators. With this we show, that with bi-implications we can also write significantly shorter modal logic formulas. This result holds even if only special classes of Kripke structures are considered. To be more precise we show that there is an exponential succinctness gap between modal logic and its extension with bi-implication on the class of structures with a transitive and reflexive accessibility relation, as well as on the class of structures with a symmetrical and reflexive accessibility relation. Lastly we show that for the class of structures with a transitive and symmetrical accessibility relation this succinctness gap disappears.
Cite as

Sebastian Pfau. Boolean Basis and Succinctness of Modal Logic via Hella-Vilander Games. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 35:1-35:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{pfau:LIPIcs.CSL.2026.35,
  author =	{Pfau, Sebastian},
  title =	{{Boolean Basis and Succinctness of Modal Logic via Hella-Vilander Games}},
  booktitle =	{34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
  pages =	{35:1--35:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-411-6},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{363},
  editor =	{Guerrini, Stefano and K\"{o}nig, Barbara},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.35},
  URN =		{urn:nbn:de:0030-drops-254600},
  doi =		{10.4230/LIPIcs.CSL.2026.35},
  annote =	{Keywords: succinctness, modal logic, model comparison games}
}
Document
DOI: 10.4230/LIPIcs.ITCS.2026.81
Supercritical Tradeoff Between Size and Depth for Resolution over Parities

Authors: Dmitry Itsykson and Alexander Knop

Published in: LIPIcs, Volume 362, 17th Innovations in Theoretical Computer Science Conference (ITCS 2026)

Abstract
Alekseev and Itsykson (STOC 2025) proved the existence of an unsatisfiable CNF formula such that any resolution over parities (Res(⊕)) refutation must either have exponential size (in the formula size) or superlinear depth (in the number of variables). In this paper, we extend this result by constructing a formula with the same hardness properties, but which additionally admits a resolution refutation of quasi-polynomial size. This establishes a supercritical tradeoff between size and depth for resolution over parities. The proof builds on the framework of Alekseev and Itsykson and relies on a lifting argument applied to the supercritical tradeoff between width and depth in resolution, proposed by Buss and Thapen (IPL 2026).
Cite as

Dmitry Itsykson and Alexander Knop. Supercritical Tradeoff Between Size and Depth for Resolution over Parities. In 17th Innovations in Theoretical Computer Science Conference (ITCS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 362, pp. 81:1-81:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{itsykson_et_al:LIPIcs.ITCS.2026.81,
  author =	{Itsykson, Dmitry and Knop, Alexander},
  title =	{{Supercritical Tradeoff Between Size and Depth for Resolution over Parities}},
  booktitle =	{17th Innovations in Theoretical Computer Science Conference (ITCS 2026)},
  pages =	{81:1--81:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-410-9},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{362},
  editor =	{Saraf, Shubhangi},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITCS.2026.81},
  URN =		{urn:nbn:de:0030-drops-253680},
  doi =		{10.4230/LIPIcs.ITCS.2026.81},
  annote =	{Keywords: lifting theorems, resolution depth, resolution over parities, resolution width, supercritical tradeoff}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2025.88
Color Refinement for Relational Structures

Authors: Benjamin Scheidt and Nicole Schweikardt

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

Abstract
Color Refinement, also known as Naive Vertex Classification, is a classical method to distinguish graphs by iteratively computing a coloring of their vertices. While it is traditionally used as an imperfect way to test for isomorphism, the algorithm has permeated many other, seemingly unrelated, areas of computer science. The method is algorithmically simple, and it has a well-understood distinguishing power: it has been logically characterized by Immerman and Lander (1990) and Cai, Fürer, Immerman (1992), who showed that it distinguishes precisely those graphs that can be distinguished by a sentence of first-order logic with counting quantifiers and only two variables. A combinatorial characterization was given by Dvořák (2010), who showed that it distinguishes precisely those graphs that differ in the number of homomorphisms from some tree. In this paper, we introduce Relational Color Refinement (RCR, for short), a generalization of the Color Refinement method from graphs to arbitrary relational structures, whose distinguishing power admits the equivalent combinatorial and logical characterizations as Color Refinement has on graphs: we show that RCR distinguishes precisely those structures that differ in the number of homomorphisms from an acyclic connected relational structure. Further, we show that RCR distinguishes precisely those structures that are distinguished by a sentence of the guarded fragment of first-order logic with counting quantifiers. Additionally, we show that for every fixed finite relational signature, RCR can be implemented to run on structures of that signature in time O(N⋅log N), where N denotes the number of tuples present in the structure.
Cite as

Benjamin Scheidt and Nicole Schweikardt. Color Refinement for Relational Structures. In 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 345, pp. 88:1-88:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{scheidt_et_al:LIPIcs.MFCS.2025.88,
  author =	{Scheidt, Benjamin and Schweikardt, Nicole},
  title =	{{Color Refinement for Relational Structures}},
  booktitle =	{50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)},
  pages =	{88:1--88: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.88},
  URN =		{urn:nbn:de:0030-drops-241958},
  doi =		{10.4230/LIPIcs.MFCS.2025.88},
  annote =	{Keywords: color refinement, counting logics, homomorphism counts, homomorphism indistinguishability, guarded logics, pebble games, relational structures, alpha-acyclicity, join-trees}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2025.40
Symmetric Proofs in the Ideal Proof System

Authors: Anuj Dawar, Erich Grädel, Leon Kullmann, and Benedikt Pago

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

Abstract
We consider the Ideal Proof System (IPS) introduced by Grochow and Pitassi and pose the question of which tautologies admit symmetric proofs, and of what complexity. The symmetry requirement in proofs is inspired by recent work establishing lower bounds in other symmetric models of computation. We link the existence of symmetric IPS proofs to the expressive power of logics such as fixed-point logic with counting and Choiceless Polynomial Time, specifically regarding the graph isomorphism problem. We identify relationships and tradeoffs between the symmetry of proofs and other parameters of IPS proofs such as size, degree and linearity. We study these on a number of standard families of tautologies from proof complexity and finite model theory such as the pigeonhole principle, the subset sum problem and the Cai-Fürer-Immerman graphs, exhibiting non-trivial upper bounds on the size of symmetric IPS proofs.
Cite as

Anuj Dawar, Erich Grädel, Leon Kullmann, and Benedikt Pago. Symmetric Proofs in the Ideal Proof System. In 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 345, pp. 40:1-40:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{dawar_et_al:LIPIcs.MFCS.2025.40,
  author =	{Dawar, Anuj and Gr\"{a}del, Erich and Kullmann, Leon and Pago, Benedikt},
  title =	{{Symmetric Proofs in the Ideal Proof System}},
  booktitle =	{50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)},
  pages =	{40:1--40: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.40},
  URN =		{urn:nbn:de:0030-drops-241477},
  doi =		{10.4230/LIPIcs.MFCS.2025.40},
  annote =	{Keywords: proof complexity, algebraic complexity, descriptive complexity, symmetric circuits, graph isomorphism}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2025.18
Supercritical Size-Width Tree-Like Resolution Trade-Offs for Graph Isomorphism

Authors: Christoph Berkholz, Moritz Lichter, and Harry Vinall-Smeeth

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

Abstract
We study the refutation complexity of graph isomorphism in the tree-like resolution calculus. Torán and Wörz [Jacobo Torán and Florian Wörz, 2023] showed that there is a resolution refutation of narrow width k for two graphs if and only if they can be distinguished in (k+1)-variable first-order logic (FO^{k+1}). While DAG-like narrow width k resolution refutations have size at most n^k, tree-like refutations may be much larger. We show that there are graphs of order n, whose isomorphism can be refuted in narrow width k but only in tree-like size 2^{Ω(n^{k/2})}. This is a supercritical trade-off where bounding one parameter (the narrow width) causes the other parameter (the size) to grow above its worst case. The size lower bound is super-exponential in the formula size and improves a related supercritical trade-off by Razborov [Alexander A. Razborov, 2016]. To prove our result, we develop a new variant of the k-pebble EF-game for FO^k to reason about tree-like refutation size in a similar way as the Prover-Delayer games in proof complexity. We analyze this game on the compressed CFI graphs introduced by Grohe, Lichter, Neuen, and Schweitzer [Martin Grohe et al., 2023]. Using a recent improved robust compressed CFI construction of de Rezende, Fleming, Janett, Nordström, and Pang [Susanna F. de Rezende et al., 2024], we obtain a similar bound for width k (instead of the stronger but less common narrow width) and make the result more robust.
Cite as

Christoph Berkholz, Moritz Lichter, and Harry Vinall-Smeeth. Supercritical Size-Width Tree-Like Resolution Trade-Offs for Graph Isomorphism. In 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 345, pp. 18:1-18:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{berkholz_et_al:LIPIcs.MFCS.2025.18,
  author =	{Berkholz, Christoph and Lichter, Moritz and Vinall-Smeeth, Harry},
  title =	{{Supercritical Size-Width Tree-Like Resolution Trade-Offs for Graph Isomorphism}},
  booktitle =	{50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)},
  pages =	{18:1--18: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.18},
  URN =		{urn:nbn:de:0030-drops-241253},
  doi =		{10.4230/LIPIcs.MFCS.2025.18},
  annote =	{Keywords: Proof complexity, Resolution, Width, Tree-like size, Supercritical trade-off, Lower bound, Finite model theory, CFI graphs}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2025.69
FO-Query Enumeration over SLP-Compressed Structures of Bounded Degree

Authors: Markus Lohrey, Sebastian Maneth, and Markus L. Schmid

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

Abstract
Enumerating the result set of a first-order query over a relational structure of bounded degree can be done with linear preprocessing and constant delay. In this work, we extend this result towards the compressed perspective where the structure is given in a potentially highly compressed form by a straight-line program (SLP). Our main result is an algorithm that enumerates the result set of a first-order query over a structure of bounded degree that is represented by an SLP satisfying the so-called apex condition. For a fixed formula, the enumeration algorithm has constant delay and needs a preprocessing time that is linear in the size of the SLP.
Cite as

Markus Lohrey, Sebastian Maneth, and Markus L. Schmid. FO-Query Enumeration over SLP-Compressed Structures of Bounded Degree. In 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 345, pp. 69:1-69:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{lohrey_et_al:LIPIcs.MFCS.2025.69,
  author =	{Lohrey, Markus and Maneth, Sebastian and Schmid, Markus L.},
  title =	{{FO-Query Enumeration over SLP-Compressed Structures of Bounded Degree}},
  booktitle =	{50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)},
  pages =	{69:1--69: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.69},
  URN =		{urn:nbn:de:0030-drops-241760},
  doi =		{10.4230/LIPIcs.MFCS.2025.69},
  annote =	{Keywords: Enumeration algorithms, FO-logic, query evaluation over compressed data}
}
Document
DOI: 10.4230/LIPIcs.CCC.2025.24
Super-Critical Trade-Offs in Resolution over Parities via Lifting

Authors: Arkadev Chattopadhyay and Pavel Dvořák

Published in: LIPIcs, Volume 339, 40th Computational Complexity Conference (CCC 2025)

Abstract
Razborov [Alexander A. Razborov, 2016] exhibited the following surprisingly strong trade-off phenomenon in propositional proof complexity: for a parameter k = k(n), there exists k-CNF formulas over n variables, having resolution refutations of O(k) width, but every tree-like refutation of width n^{1-ε}/k needs size exp(n^Ω(k)). We extend this result to tree-like Resolution over parities, commonly denoted by Res(⊕), with parameters essentially unchanged. To obtain our result, we extend the lifting theorem of Chattopadhyay, Mande, Sanyal and Sherif [Arkadev Chattopadhyay et al., 2023] to handle tree-like affine DAGs. We introduce additional ideas from linear algebra to handle forget nodes along long paths.
Cite as

Arkadev Chattopadhyay and Pavel Dvořák. Super-Critical Trade-Offs in Resolution over Parities via Lifting. In 40th Computational Complexity Conference (CCC 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 339, pp. 24:1-24:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{chattopadhyay_et_al:LIPIcs.CCC.2025.24,
  author =	{Chattopadhyay, Arkadev and Dvo\v{r}\'{a}k, Pavel},
  title =	{{Super-Critical Trade-Offs in Resolution over Parities via Lifting}},
  booktitle =	{40th Computational Complexity Conference (CCC 2025)},
  pages =	{24:1--24:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-379-9},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{339},
  editor =	{Srinivasan, Srikanth},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2025.24},
  URN =		{urn:nbn:de:0030-drops-237186},
  doi =		{10.4230/LIPIcs.CCC.2025.24},
  annote =	{Keywords: Proof complexity, Lifting, Resolution over parities}
}
Document
DOI: 10.4230/LIPIcs.CCC.2025.8
Amortized Closure and Its Applications in Lifting for Resolution over Parities

Authors: Klim Efremenko and Dmitry Itsykson

Published in: LIPIcs, Volume 339, 40th Computational Complexity Conference (CCC 2025)

Abstract
The notion of closure of a set of linear forms, first introduced by Efremenko, Garlik, and Itsykson [Klim Efremenko et al., 2024], has proven instrumental in proving lower bounds on the sizes of regular and bounded-depth Res(⊕) refutations [Klim Efremenko et al., 2024; Yaroslav Alekseev and Dmitry Itsykson, 2025]. In this work, we present amortized closure, an enhancement that retains the properties of original closure [Klim Efremenko et al., 2024] but offers tighter control on its growth. Specifically, adding a new linear form increases the amortized closure by at most one. We explore two applications that highlight the power of this new concept. Utilizing our newly defined amortized closure, we extend and provide a succinct and elegant proof of the recent lifting theorem by Chattopadhyay and Dvorak [Arkadev Chattopadhyay and Pavel Dvorak, 2025]. Namely we show that for an unsatisfiable CNF formula φ and a 1-stifling gadget g: {0,1}^𝓁 → {0,1}, if the lifted formula φ∘g has a tree-like Res(⊕) refutation of size 2^d and width w, then φ has a resolution refutation of depth d and width w. The original theorem by Chattopadhyay and Dvorak [Arkadev Chattopadhyay and Pavel Dvorak, 2025] applies only to the more restrictive class of strongly stifling gadgets. As a more significant application of amortized closure, we show improved lower bounds for bounded-depth Res(⊕), extending the depth beyond that of Alekseev and Itsykson [Yaroslav Alekseev and Dmitry Itsykson, 2025]. Our result establishes an exponential lower bound for depth-Ω(n log n) Res(⊕) refutations of lifted Tseitin formulas, a notable improvement over the existing depth-Ω(n log log n) Res(⊕) lower bound.
Cite as

Klim Efremenko and Dmitry Itsykson. Amortized Closure and Its Applications in Lifting for Resolution over Parities. In 40th Computational Complexity Conference (CCC 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 339, pp. 8:1-8:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{efremenko_et_al:LIPIcs.CCC.2025.8,
  author =	{Efremenko, Klim and Itsykson, Dmitry},
  title =	{{Amortized Closure and Its Applications in Lifting for Resolution over Parities}},
  booktitle =	{40th Computational Complexity Conference (CCC 2025)},
  pages =	{8:1--8:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-379-9},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{339},
  editor =	{Srinivasan, Srikanth},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2025.8},
  URN =		{urn:nbn:de:0030-drops-237023},
  doi =		{10.4230/LIPIcs.CCC.2025.8},
  annote =	{Keywords: lifting, resolution over parities, closure of linear forms, lower bounds, width, depth, size vs depth tradeoff}
}
Document
Track A: Algorithms, Complexity and Games
DOI: 10.4230/LIPIcs.ICALP.2025.78
The Role of Regularity in (Hyper-)Clique Detection and Implications for Optimizing Boolean CSPs

Authors: Nick Fischer, Marvin Künnemann, Mirza Redžić, and Julian Stieß

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

Abstract
Is detecting a k-clique in k-partite regular (hyper-)graphs as hard as in the general case? Intuition suggests yes, but proving this - especially for hypergraphs - poses notable challenges. Concretely, we consider a strong notion of regularity in h-uniform hypergraphs, where we essentially require that any subset of at most h-1 is incident to a uniform number of hyperedges. Such notions are studied intensively in the combinatorial block design literature. We show that any f(k)n^{g(k)}-time algorithm for detecting k-cliques in such graphs transfers to an f'(k)n^{g(k)}-time algorithm for the general case, establishing a fine-grained equivalence between the h-uniform hyperclique hypothesis and its natural regular analogue. Equipped with this regularization result, we then fully resolve the fine-grained complexity of optimizing Boolean constraint satisfaction problems over assignments with k non-zeros. Our characterization depends on the maximum degree d of a constraint function. Specifically, if d ≤ 1, we obtain a linear-time solvable problem, if d = 2, the time complexity is essentially equivalent to k-clique detection, and if d ≥ 3 the problem requires exhaustive-search time under the 3-uniform hyperclique hypothesis. To obtain our hardness results, the regularization result plays a crucial role, enabling a very convenient approach when applied carefully. We believe that our regularization result will find further applications in the future.
Cite as

Nick Fischer, Marvin Künnemann, Mirza Redžić, and Julian Stieß. The Role of Regularity in (Hyper-)Clique Detection and Implications for Optimizing Boolean CSPs. In 52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 334, pp. 78:1-78:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{fischer_et_al:LIPIcs.ICALP.2025.78,
  author =	{Fischer, Nick and K\"{u}nnemann, Marvin and Red\v{z}i\'{c}, Mirza and Stie{\ss}, Julian},
  title =	{{The Role of Regularity in (Hyper-)Clique Detection and Implications for Optimizing Boolean CSPs}},
  booktitle =	{52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025)},
  pages =	{78:1--78:18},
  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.78},
  URN =		{urn:nbn:de:0030-drops-234559},
  doi =		{10.4230/LIPIcs.ICALP.2025.78},
  annote =	{Keywords: fine-grained complexity theory, clique detections in hypergraphs, constraint satisfaction, parameterized algorithms}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2025.166
Limitations of Affine Integer Relaxations for Solving Constraint Satisfaction Problems

Authors: Moritz Lichter and Benedikt Pago

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

Abstract
We show that various recent algorithms for finite-domain constraint satisfaction problems (CSP), which are based on solving their affine integer relaxations, do not solve all tractable and not even all Maltsev CSPs. This rules them out as candidates for a universal polynomial-time CSP algorithm. The algorithms are ℤ-affine k-consistency, BLP+AIP, BA^{k}, and CLAP. We thereby answer a question by Brakensiek, Guruswami, Wrochna, and Živný [Joshua Brakensiek et al., 2020] whether a constant level of BA^{k}solves all tractable CSPs in the negative: Indeed, not even a sublinear level k suffices. We also refute a conjecture by Dalmau and Opršal [Víctor Dalmau and Jakub Opršal, 2024] (LICS 2024) that every CSP is either solved by ℤ-affine k-consistency or admits a Datalog reduction from 3-colorability. For the cohomological k-consistency algorithm, that is also based on affine relaxations, we show that it correctly solves our counterexample but fails on an NP-complete template.
Cite as

Moritz Lichter and Benedikt Pago. Limitations of Affine Integer Relaxations for Solving Constraint Satisfaction Problems. In 52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 334, pp. 166:1-166:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{lichter_et_al:LIPIcs.ICALP.2025.166,
  author =	{Lichter, Moritz and Pago, Benedikt},
  title =	{{Limitations of Affine Integer Relaxations for Solving Constraint Satisfaction Problems}},
  booktitle =	{52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025)},
  pages =	{166:1--166: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.166},
  URN =		{urn:nbn:de:0030-drops-235431},
  doi =		{10.4230/LIPIcs.ICALP.2025.166},
  annote =	{Keywords: constraint satisfaction, affine relaxation, promise CSPs, \mathbb{Z}-affine k-consistency, cohomological k-consistency algorithm, Tseitin, graph isomorphism}
}
Document
Track A: Algorithms, Complexity and Games
DOI: 10.4230/LIPIcs.ICALP.2025.34
On the Degree Automatability of Sum-Of-Squares Proofs

Authors: Alex Bortolotti, Monaldo Mastrolilli, and Luis Felipe Vargas

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

Abstract
The Sum-of-Squares (SoS) hierarchy, also known as Lasserre hierarchy, has emerged as a promising tool in optimization. However, it remains unclear whether fixed-degree SoS proofs can be automated [O'Donnell (2017)]. Indeed, there are examples of polynomial systems with bounded coefficients that admit low-degree SoS proofs, but these proofs necessarily involve numbers with an exponential number of bits, implying that low-degree SoS proofs cannot always be found efficiently. A sufficient condition derived from the Nullstellensatz proof system [Raghavendra and Weitz (2017)] identifies cases where bit complexity issues can be circumvented. One of the main problems left open by Raghavendra and Weitz is proving any result for refutations, as their condition applies only to polynomial systems with a large set of solutions. In this work, we broaden the class of polynomial systems for which degree-d SoS proofs can be automated. To achieve this, we develop a new criterion and we demonstrate how our criterion applies to polynomial systems beyond the scope of Raghavendra and Weitz’s result. In particular, we establish a separation for instances arising from Constraint Satisfaction Problems (CSPs). Moreover, our result extends to refutations, establishing that polynomial-time refutation is possible for broad classes of polynomial time solvable constraint problems, highlighting a first advancement in this area.
Cite as

Alex Bortolotti, Monaldo Mastrolilli, and Luis Felipe Vargas. On the Degree Automatability of Sum-Of-Squares Proofs. In 52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 334, pp. 34:1-34:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{bortolotti_et_al:LIPIcs.ICALP.2025.34,
  author =	{Bortolotti, Alex and Mastrolilli, Monaldo and Vargas, Luis Felipe},
  title =	{{On the Degree Automatability of Sum-Of-Squares Proofs}},
  booktitle =	{52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025)},
  pages =	{34:1--34:19},
  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.34},
  URN =		{urn:nbn:de:0030-drops-234110},
  doi =		{10.4230/LIPIcs.ICALP.2025.34},
  annote =	{Keywords: Sum of squares, Polynomial calculus, Polynomial ideal membership, Polymorphisms, Gr\"{o}bner basis theory, Constraint satisfaction problems, Proof complexity}
}
Document
DOI: 10.4230/LIPIcs.SoCG.2025.25
Approximating Klee’s Measure Problem and a Lower Bound for Union Volume Estimation

Authors: Karl Bringmann, Kasper Green Larsen, André Nusser, Eva Rotenberg, and Yanheng Wang

Published in: LIPIcs, Volume 332, 41st International Symposium on Computational Geometry (SoCG 2025)

Abstract
Union volume estimation is a classical algorithmic problem. Given a family of objects O₁,…,O_n ⊂ ℝ^d, we want to approximate the volume of their union. In the special case where all objects are boxes (also called hyperrectangles) this is known as Klee’s measure problem. The state-of-the-art (1+ε)-approximation algorithm [Karp, Luby, Madras '89] for union volume estimation as well as Klee’s measure problem in constant dimension d uses a total of O(n/ε²) queries of three types: (i) determine the volume of O_i; (ii) sample a point uniformly at random from O_i; and (iii) ask whether a given point is contained in O_i. First, we show that if an algorithm learns about the objects only through these types of queries, then Ω(n/ε²) queries are necessary. In this sense, the complexity of [Karp, Luby, Madras '89] is optimal. Our lower bound holds even if the objects are equiponderous axis-aligned polygons in ℝ², if the containment query allows arbitrary (not necessarily sampled) points, and if the algorithm can spend arbitrary time and space examining the query responses. Second, we provide a more efficient approximation algorithm for Klee’s measure problem, which improves the running time from O(n/ε²) to O((n+1/ε²) ⋅ log^{O(d)} (n)). We circumvent our lower bound by exploiting the geometry of boxes in various ways: (1) We sort the boxes into classes of similar shapes after inspecting their corner coordinates. (2) With orthogonal range searching, we show how to sample points from the union of boxes in each class, and how to merge samples from different classes. (3) We bound the amount of wasted work by arguing that most pairs of classes have a small intersection.
Cite as

Karl Bringmann, Kasper Green Larsen, André Nusser, Eva Rotenberg, and Yanheng Wang. Approximating Klee’s Measure Problem and a Lower Bound for Union Volume Estimation. In 41st International Symposium on Computational Geometry (SoCG 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 332, pp. 25:1-25:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{bringmann_et_al:LIPIcs.SoCG.2025.25,
  author =	{Bringmann, Karl and Larsen, Kasper Green and Nusser, Andr\'{e} and Rotenberg, Eva and Wang, Yanheng},
  title =	{{Approximating Klee’s Measure Problem and a Lower Bound for Union Volume Estimation}},
  booktitle =	{41st International Symposium on Computational Geometry (SoCG 2025)},
  pages =	{25:1--25:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-370-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{332},
  editor =	{Aichholzer, Oswin and Wang, Haitao},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SoCG.2025.25},
  URN =		{urn:nbn:de:0030-drops-231778},
  doi =		{10.4230/LIPIcs.SoCG.2025.25},
  annote =	{Keywords: approximation, volume of union, union of objects, query complexity}
}
Document
DOI: 10.4230/LIPIcs.ICDT.2025.20
A Formal Language Perspective on Factorized Representations

Authors: Benny Kimelfeld, Wim Martens, and Matthias Niewerth

Published in: LIPIcs, Volume 328, 28th International Conference on Database Theory (ICDT 2025)

Abstract
Factorized representations (FRs) are a well-known tool to succinctly represent results of join queries and have been originally defined using the named database perspective. We define FRs in the unnamed database perspective and use them to establish several new connections. First, unnamed FRs can be exponentially more succinct than named FRs, but this difference can be alleviated by imposing a disjointness condition on columns. Conversely, named FRs can also be exponentially more succinct than unnamed FRs. Second, unnamed FRs are the same as (i.e., isomorphic to) context-free grammars for languages in which each word has the same length. This tight connection allows us to transfer a wide range of results on context-free grammars to database factorization; of which we offer a selection in the paper. Third, when we generalize unnamed FRs to arbitrary sets of tuples, they become a generalization of path multiset representations, a formalism that was recently introduced to succinctly represent sets of paths in the context of graph database query evaluation.
Cite as

Benny Kimelfeld, Wim Martens, and Matthias Niewerth. A Formal Language Perspective on Factorized Representations. In 28th International Conference on Database Theory (ICDT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 328, pp. 20:1-20:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{kimelfeld_et_al:LIPIcs.ICDT.2025.20,
  author =	{Kimelfeld, Benny and Martens, Wim and Niewerth, Matthias},
  title =	{{A Formal Language Perspective on Factorized Representations}},
  booktitle =	{28th International Conference on Database Theory (ICDT 2025)},
  pages =	{20:1--20:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-364-5},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{328},
  editor =	{Roy, Sudeepa and Kara, Ahmet},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICDT.2025.20},
  URN =		{urn:nbn:de:0030-drops-229614},
  doi =		{10.4230/LIPIcs.ICDT.2025.20},
  annote =	{Keywords: Databases, relational databases, graph databases, factorized databases, regular path queries, compact representations}
}
  • Refine by Type
  • 30 Document/PDF
  • 19 Document/HTML

  • Refine by Publication Year
  • 4 2026
  • 15 2025
  • 2 2024
  • 1 2023
  • 1 2022
  • Show More...

  • Refine by Author
  • 13 Berkholz, Christoph
  • 4 Schweikardt, Nicole
  • 3 Vinall-Smeeth, Harry
  • 2 Itsykson, Dmitry
  • 2 Keppeler, Jens
  • Show More...

  • Refine by Series/Journal
  • 29 LIPIcs
  • 1 DagRep

  • Refine by Classification
  • 5 Theory of computation → Complexity theory and logic
  • 5 Theory of computation → Finite Model Theory
  • 5 Theory of computation → Proof complexity
  • 4 Theory of computation → Database theory
  • 4 Theory of computation → Problems, reductions and completeness
  • Show More...

  • Refine by Keyword
  • 4 Proof complexity
  • 3 constraint satisfaction
  • 2 counting problem
  • 2 descriptive complexity
  • 2 graph isomorphism
  • 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