78 Search Results for "Kolaitis, Phokion"

Volume

Dagstuhl Follow-Ups, Volume 5

Data Exchange, Integration, and Streams

Editors: Phokion G. Kolaitis, Maurizio Lenzerini, and Nicole Schweikardt

Document
DOI: 10.4230/LIPIcs.ICDT.2026.16
Gamma Acyclicity, Annotated Relations, and Consistency Witness Functions

Authors: Albert Atserias and Phokion G. Kolaitis

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

Abstract
During the early days of relational database theory it was realized that "acyclic" database schemas possess a number of desirable properties. In fact, three different notions of "acyclicity" were identified and investigated during the 1980s, namely, α-acyclicity, β-acyclicity, and γ-acyclicity. Much more recently, the study of α-acyclicity was extended to annotated relations, where the annotations are values from some positive commutative monoid. The recent results about α-acyclic schemas and annotated relations give rise to results about β-acyclic schemas and annotated relations, since a schema is β-acyclic if and only if every sub-schema of it is α-acyclic. Here, we study γ-acyclic schemas and annotated relations. Our main finding is that the characterization of γ-acyclic schemas in terms of monotone sequential join expression extends to annotated relations, provided the annotations come from a positive commutative monoid that has the inner consistency property. Furthermore, the results reported here shed light on the role of the join of two standard relations. Specifically, our results reveal that the only relevant property of the join of two standard relations is that it is a witness to the consistency of the two relations, provided that these two relations are consistent. For the more abstract setting of annotated relations, this property of the standard join is captured by the notion of a consistency witness function, a notion which we systematically utilize in this work.
Cite as

Albert Atserias and Phokion G. Kolaitis. Gamma Acyclicity, Annotated Relations, and Consistency Witness Functions. In 29th International Conference on Database Theory (ICDT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 365, pp. 16:1-16:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{atserias_et_al:LIPIcs.ICDT.2026.16,
  author =	{Atserias, Albert and Kolaitis, Phokion G.},
  title =	{{Gamma Acyclicity, Annotated Relations, and Consistency Witness Functions}},
  booktitle =	{29th International Conference on Database Theory (ICDT 2026)},
  pages =	{16:1--16:18},
  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.16},
  URN =		{urn:nbn:de:0030-drops-256304},
  doi =		{10.4230/LIPIcs.ICDT.2026.16},
  annote =	{Keywords: annotated relations, gamma-acyclicity, consistency witness functions}
}
Document
DOI: 10.4230/LIPIcs.CSL.2026.10
Disjunctions of Two Dependence Atoms

Authors: Nicolas Fröhlich, Phokion G. Kolaitis, and Arne Meier

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

Abstract
Dependence logic is a formalism that augments the syntax of first-order logic with dependence atoms asserting that the value of a variable is determined by the values of some other variables, i.e., dependence atoms express functional dependencies in relational databases. On finite structures, dependence logic captures NP, hence there are sentences of dependence logic whose model-checking problem is NP-complete. In fact, it is known that there are disjunctions of three dependence atoms whose model-checking problem is NP-complete. Motivated from considerations in database theory, we study the model-checking problem for disjunctions of two unary dependence atoms and establish a trichotomy theorem, namely, for every such formula, one of the following is true for the model-checking problem: (i) it is NL-complete; (ii) it is L-complete; (iii) it is first-order definable (hence, in AC⁰). Furthermore, we classify the complexity of the model-checking problem for disjunctions of two arbitrary dependence atoms, and also characterize when such a disjunction is coherent, i.e., when it satisfies a certain small-model property. Along the way, we identify a new class of 2CNF-formulas whose satisfiability problem is L-complete.
Cite as

Nicolas Fröhlich, Phokion G. Kolaitis, and Arne Meier. Disjunctions of Two Dependence Atoms. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 10:1-10:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{frohlich_et_al:LIPIcs.CSL.2026.10,
  author =	{Fr\"{o}hlich, Nicolas and Kolaitis, Phokion G. and Meier, Arne},
  title =	{{Disjunctions of Two Dependence Atoms}},
  booktitle =	{34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
  pages =	{10:1--10:21},
  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.10},
  URN =		{urn:nbn:de:0030-drops-254343},
  doi =		{10.4230/LIPIcs.CSL.2026.10},
  annote =	{Keywords: Dependence logic, coherence, model-checking, complexity, functional dependencies}
}
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.CSL.2026.36
A Game for Counting Logic Formula Size and an Application to Linear Orders

Authors: Grégoire Fournier and György Turán

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

Abstract
Ehrenfeucht-Fraïssé (EF) games are a basic tool in finite model theory for proving definability lower bounds, with many applications in complexity theory and related areas. They have been applied to study various logics, giving insights on quantifier rank and other logical complexity measures. In this paper, we present an EF game to capture formula size in counting logic with a bounded number of variables. The game combines games introduced previously for counting logic quantifier rank due to Immerman and Lander, and for first-order formula size due to Adler and Immerman, and Hella and Väänänen. The game is used to prove an extension of a formula size lower bound of Grohe and Schweikardt for distinguishing linear orders, from 3-variable first-order logic to 3-variable counting logic.
Cite as

Grégoire Fournier and György Turán. A Game for Counting Logic Formula Size and an Application to Linear Orders. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 36:1-36:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{fournier_et_al:LIPIcs.CSL.2026.36,
  author =	{Fournier, Gr\'{e}goire and Tur\'{a}n, Gy\"{o}rgy},
  title =	{{A Game for Counting Logic Formula Size and an Application to Linear Orders}},
  booktitle =	{34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
  pages =	{36:1--36: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.36},
  URN =		{urn:nbn:de:0030-drops-254612},
  doi =		{10.4230/LIPIcs.CSL.2026.36},
  annote =	{Keywords: Finite Model Theory, Logical Aspects of Computational Complexity}
}
Document
DOI: 10.4230/LIPIcs.CSL.2026.7
Bridging Weighted First Order Model Counting and Graph Polynomials

Authors: Qipeng Kuang, Ondřej Kuželka, Yuanhong Wang, and Yuyi Wang

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

Abstract
The Weighted First-Order Model Counting Problem (WFOMC) asks to compute the weighted sum of models of a given first-order logic sentence over a given domain. It can be solved in time polynomial in the domain size for sentences from the two-variable fragment with counting quantifiers, known as C^2. This polynomial-time complexity is known to be retained when extending C^2 by one of the following axioms: linear order axiom, tree axiom, forest axiom, directed acyclic graph axiom or connectedness axiom. An interesting question remains as to which other axioms can be added to the first-order sentences in this way. We provide a new perspective on this problem by associating WFOMC with graph polynomials. Using WFOMC, we define Weak Connectedness Polynomial and Strong Connectedness Polynomials for first-order logic sentences. It turns out that these polynomials have the following interesting properties. First, they can be computed in polynomial time in the domain size for sentences from C^2. Second, we can use them to solve WFOMC with all of the existing axioms known to be tractable as well as with new ones such as bipartiteness, strong connectedness, having k connected components, etc. Third, the well-known Tutte polynomial can be recovered as a special case of the Weak Connectedness Polynomial, and the Strict and Non-Strict Directed Chromatic Polynomials can be recovered from the Strong Connectedness Polynomials.
Cite as

Qipeng Kuang, Ondřej Kuželka, Yuanhong Wang, and Yuyi Wang. Bridging Weighted First Order Model Counting and Graph Polynomials. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 7:1-7:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{kuang_et_al:LIPIcs.CSL.2026.7,
  author =	{Kuang, Qipeng and Ku\v{z}elka, Ond\v{r}ej and Wang, Yuanhong and Wang, Yuyi},
  title =	{{Bridging Weighted First Order Model Counting and Graph Polynomials}},
  booktitle =	{34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
  pages =	{7:1--7:23},
  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.7},
  URN =		{urn:nbn:de:0030-drops-254316},
  doi =		{10.4230/LIPIcs.CSL.2026.7},
  annote =	{Keywords: Weighted First-Order Model Counting, Axiom, Enumerative Combinatorics, Tutte Polynomial}
}
Document
DOI: 10.4230/LIPIcs.CSL.2026.6
Hereditary First-Order Logic: the Tractable Quantifier Prefix Classes

Authors: Manuel Bodirsky and Santiago Guzmán-Pro

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

Abstract
Many computational problems can be modelled as the class of all finite structures A that satisfy a fixed first-order sentence ϕ hereditarily, i.e., we require that every (induced) substructure of A satisfies ϕ. We call the corresponding computational problem the hereditary model checking problem for ϕ, and denote it by Her(ϕ). We present a complete description of the quantifier prefixes for ϕ such that Her(ϕ) is in P; we show that for every other quantifier prefix there exists a formula ϕ with this prefix such that Her(ϕ) is coNP-complete. Specifically, we show that if Q is of the form ∀*∃∀* or of the form ∀*∃*, then Her(ϕ) can be solved in polynomial time whenever the quantifier prefix of ϕ is Q. Otherwise, Q contains ∃∃∀ or ∃∀∃ as a subword, and in this case, there is a first-order formula ϕ whose quantifier prefix is Q and Her(ϕ) is coNP-complete. Moreover, we show that there is no algorithm that decides for a given first-order formula ϕ whether Her(ϕ) is in P (unless P=NP).
Cite as

Manuel Bodirsky and Santiago Guzmán-Pro. Hereditary First-Order Logic: the Tractable Quantifier Prefix Classes. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 6:1-6:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{bodirsky_et_al:LIPIcs.CSL.2026.6,
  author =	{Bodirsky, Manuel and Guzm\'{a}n-Pro, Santiago},
  title =	{{Hereditary First-Order Logic: the Tractable Quantifier Prefix Classes}},
  booktitle =	{34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
  pages =	{6:1--6:20},
  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.6},
  URN =		{urn:nbn:de:0030-drops-254308},
  doi =		{10.4230/LIPIcs.CSL.2026.6},
  annote =	{Keywords: Quantifier prefix, first-order Logic, Computational Complexity, Polynomial-time algorithm, coNP-completeness}
}
Document
DOI: 10.4230/LIPIcs.CSL.2026.41
Weakly-Sparse and Strongly Flip-Flat Classes of Graphs Are Uniformly Almost-Wide

Authors: Fatemeh Ghasemi, Julien Grange, Mamadou Moustapha Kanté, and Florent Madelaine

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

Abstract
In this work we take a step towards characterising strongly flip-flat classes of graphs. Strong flip-flatness appears to be the analogue of uniform almost-wideness in the setting of dense classes of graphs. We prove that strongly flip-flat classes of graphs that are weakly sparse are indeed uniformly almost-wide.
Cite as

Fatemeh Ghasemi, Julien Grange, Mamadou Moustapha Kanté, and Florent Madelaine. Weakly-Sparse and Strongly Flip-Flat Classes of Graphs Are Uniformly Almost-Wide. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 41:1-41:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{ghasemi_et_al:LIPIcs.CSL.2026.41,
  author =	{Ghasemi, Fatemeh and Grange, Julien and Kant\'{e}, Mamadou Moustapha and Madelaine, Florent},
  title =	{{Weakly-Sparse and Strongly Flip-Flat Classes of Graphs Are Uniformly Almost-Wide}},
  booktitle =	{34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
  pages =	{41:1--41:14},
  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.41},
  URN =		{urn:nbn:de:0030-drops-254668},
  doi =		{10.4230/LIPIcs.CSL.2026.41},
  annote =	{Keywords: Almost-wide, Flip-flatness}
}
Document
DOI: 10.4230/LIPIcs.ITCS.2026.99
AC⁰[p]-Frege Cannot Efficiently Prove That Constant-Depth Algebraic Circuit Lower Bounds Are Hard

Authors: Jiaqi Lu, Rahul Santhanam, and Iddo Tzameret

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

Abstract
We study whether lower bounds against constant-depth algebraic circuits computing the Permanent over finite fields (Limaye-Srinivasan-Tavenas [J. ACM, 2025] and Forbes [CCC'24]) are hard to prove in certain proof systems. We focus on a DNF formula that expresses that such lower bounds are hard for constant-depth algebraic proofs. Using an adaptation of the diagonalization framework of Santhanam and Tzameret (SIAM J. Comput., 2025), we show unconditionally that this family of DNF formulas does not admit polynomial-size propositional AC⁰[p]-Frege proofs, infinitely often. This rules out the possibility that the DNF family is easy, and establishes that its status is either that of a hard tautology for AC⁰[p]-Frege or else unprovable (i.e., not a tautology). While it remains open whether the DNFs in question are tautologies, we provide evidence in this direction. In particular, under the plausible assumption that certain (weak) properties of multilinear algebra - specifically, those involving tensor rank - do not admit short constant-depth algebraic proofs, the DNFs are tautologies. We also observe that several weaker variants of the DNF formula are provably tautologies, and we show that the question of whether the DNFs are tautologies connects to conjectures of Razborov (ICALP'96) and Krajíček (J. Symb. Log., 2004). Additionally, our result has the following special features: ii) Existential depth amplification: the DNF formula considered is parameterised by a constant depth d bounding the depth of the algebraic proofs. We show that there exists some fixed depth d such that if there are no small depth-d algebraic proofs of certain circuit lower bounds for the Permanent, then there are no such small algebraic proofs in any constant depth. iii) Necessity: We show that our result is a necessary step towards establishing lower bounds against constant-depth algebraic proofs, and more generally against any sufficiently strong proof system. In particular, showing there are no short proofs for our DNF formulas, obtained by replacing "constant-depth algebraic circuits" with any "reasonable" algebraic circuit class C, is necessary in order to prove any super-polynomial lower bounds against algebraic proofs operating with circuits from C.
Cite as

Jiaqi Lu, Rahul Santhanam, and Iddo Tzameret. AC⁰[p]-Frege Cannot Efficiently Prove That Constant-Depth Algebraic Circuit Lower Bounds Are Hard. In 17th Innovations in Theoretical Computer Science Conference (ITCS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 362, pp. 99:1-99:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{lu_et_al:LIPIcs.ITCS.2026.99,
  author =	{Lu, Jiaqi and Santhanam, Rahul and Tzameret, Iddo},
  title =	{{AC⁰\lbrackp\rbrack-Frege Cannot Efficiently Prove That Constant-Depth Algebraic Circuit Lower Bounds Are Hard}},
  booktitle =	{17th Innovations in Theoretical Computer Science Conference (ITCS 2026)},
  pages =	{99:1--99:25},
  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.99},
  URN =		{urn:nbn:de:0030-drops-253865},
  doi =		{10.4230/LIPIcs.ITCS.2026.99},
  annote =	{Keywords: Complexity, Lower bounds, Proof complexity, AC⁰\lbrackp\rbrack-Frege, Diagonalisation, Algebraic complexity}
}
Document
DOI: 10.4230/LIPIcs.IPEC.2025.25
Exact Algorithms and Hardness Result for the Boolean Connectivity Problem of k-Horn Formulas

Authors: Takashi Horiyama, Yuto Okura, Kazuhisa Seto, and Junichi Teruyama

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

Abstract
The Boolean connectivity problem asks whether the set of satisfying assignments of a given Boolean formula forms a connected subgraph in the n-dimensional hypercube. This problem is known to be coNP-complete, even when restricted to k-Horn formulas for k ≥ 3, as shown by Makino, Tamaki, and Yamamoto. In this paper, we further investigate the complexity of the Boolean connectivity problem for k-Horn formulas, referred to as Conn k-Horn. We first present an exact exponential-time algorithm for Conn k-Horn without any structural restrictions. Our algorithm builds on the deterministic PPZ algorithm proposed by Paturi, Pudlák, and Zane. It runs in O^*(2^{(1-1/2k)n}) time, achieving an exponential improvement over the previously known algorithm for the Boolean connectivity problem of k-CNF formulas, shown by Makino, Tamaki, and Yamamoto. We then examine both algorithmic and hardness results for Conn 3-Horn under bounded variable occurrences. On the algorithmic side, we propose a polynomial-time algorithm for Conn 3-Horn when each clause contains exactly three literals and each variable appears at most three times. This result generalizes to Conn k-Horn under the same structural constraints, in which each clause contains exactly k literals and each variable appears at most k times. On the hardness side, we prove that Conn 3-Horn remains coNP-complete even when restricted to instances in which each variable appears exactly four times.
Cite as

Takashi Horiyama, Yuto Okura, Kazuhisa Seto, and Junichi Teruyama. Exact Algorithms and Hardness Result for the Boolean Connectivity Problem of k-Horn Formulas. In 20th International Symposium on Parameterized and Exact Computation (IPEC 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 358, pp. 25:1-25:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{horiyama_et_al:LIPIcs.IPEC.2025.25,
  author =	{Horiyama, Takashi and Okura, Yuto and Seto, Kazuhisa and Teruyama, Junichi},
  title =	{{Exact Algorithms and Hardness Result for the Boolean Connectivity Problem of k-Horn Formulas}},
  booktitle =	{20th International Symposium on Parameterized and Exact Computation (IPEC 2025)},
  pages =	{25:1--25:15},
  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.25},
  URN =		{urn:nbn:de:0030-drops-251577},
  doi =		{10.4230/LIPIcs.IPEC.2025.25},
  annote =	{Keywords: k-Horn, Boolean connectivity, bounded variable occurrence, hardness, exact algorithm, satisfiability}
}
Document
Invited Paper
DOI: 10.4230/OASIcs.RW.2024/2025.5
Inconsistency-Tolerant Semantics Based on (Preferred) Repairs (Invited Paper)

Authors: Camille Bourgaux

Published in: OASIcs, Volume 138, Joint Proceedings of the 20th and 21st Reasoning Web Summer Schools (RW 2024 & RW 2025)

Abstract
Real-world datasets are plagued by data quality issues which may render the data inconsistent w.r.t. a set of constraints, be they given by database integrity constraints or ontologies. A prominent way to handle such inconsistent data is to use inconsistency-tolerant semantics to obtain meaningful answers to queries. Most of these semantics are based on some notion of repairs, which represent ways of restoring the data consistency. The most basic kind of repairs is that of subset repairs, which are maximal consistent subsets of the dataset. However, in many scenarios, one can define preferred repairs based on some preference information. These lecture notes present inconsistency-tolerant semantics, focusing on the repair-based ones, then review different kinds of preferred repairs that have been considered in the literature. We present in particular the relationships between different kinds of preferred repairs and other notions related to inconsistency handling, the computational complexity of reasoning with (preferred) repairs, and some implementations.
Cite as

Camille Bourgaux. Inconsistency-Tolerant Semantics Based on (Preferred) Repairs (Invited Paper). In Joint Proceedings of the 20th and 21st Reasoning Web Summer Schools (RW 2024 & RW 2025). Open Access Series in Informatics (OASIcs), Volume 138, pp. 5:1-5:67, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{bourgaux:OASIcs.RW.2024/2025.5,
  author =	{Bourgaux, Camille},
  title =	{{Inconsistency-Tolerant Semantics Based on (Preferred) Repairs}},
  booktitle =	{Joint Proceedings of the 20th and 21st Reasoning Web Summer Schools (RW 2024 \& RW 2025)},
  pages =	{5:1--5:67},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-405-5},
  ISSN =	{2190-6807},
  year =	{2025},
  volume =	{138},
  editor =	{Artale, Alessandro and Bienvenu, Meghyn and Garc{\'\i}a, Yazm{\'\i}n Ib\'{a}\~{n}ez and Murlak, Filip},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.RW.2024/2025.5},
  URN =		{urn:nbn:de:0030-drops-250504},
  doi =		{10.4230/OASIcs.RW.2024/2025.5},
  annote =	{Keywords: Knowledge bases, databases, inconsistency handling, repairs, preferences}
}
Document
Invited Paper
DOI: 10.4230/OASIcs.RW.2024/2025.7
Modern Datalog: Concepts, Methods, Applications (Invited Paper)

Authors: Markus Krötzsch

Published in: OASIcs, Volume 138, Joint Proceedings of the 20th and 21st Reasoning Web Summer Schools (RW 2024 & RW 2025)

Abstract
Pure Datalog is arguably the most fundamental rule language, elegant and simple, but also often too limited to be useful in practice. This has motivated the introduction of many new expressive features, ranging from datatypes and related functions, over aggregates and semi-ring generalisations, to existential quantifiers and complex terms. In spite of their variety, all these approaches remain true to the nature of Datalog as a direct, pattern-based way of computing on structured data. We therefore find that a modern notion of Datalog is emerging, distinctly different from other approaches of logic programming and with its own set of related methods and applications. In this course, we introduce Datalog and its most common extensions, and explain when and how these features can be used together (which is often, but not always, safe to do). We further look at modern Datalog systems and some of their primary use cases. Hands-on work with Datalog and its extensions is done with the free Datalog engine https://knowsys.github.io/nemo-doc/. The course is accessible to all audiences and does not assume specific prior knowledge.
Cite as

Markus Krötzsch. Modern Datalog: Concepts, Methods, Applications (Invited Paper). In Joint Proceedings of the 20th and 21st Reasoning Web Summer Schools (RW 2024 & RW 2025). Open Access Series in Informatics (OASIcs), Volume 138, pp. 7:1-7:41, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{krotzsch:OASIcs.RW.2024/2025.7,
  author =	{Kr\"{o}tzsch, Markus},
  title =	{{Modern Datalog: Concepts, Methods, Applications}},
  booktitle =	{Joint Proceedings of the 20th and 21st Reasoning Web Summer Schools (RW 2024 \& RW 2025)},
  pages =	{7:1--7:41},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-405-5},
  ISSN =	{2190-6807},
  year =	{2025},
  volume =	{138},
  editor =	{Artale, Alessandro and Bienvenu, Meghyn and Garc{\'\i}a, Yazm{\'\i}n Ib\'{a}\~{n}ez and Murlak, Filip},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.RW.2024/2025.7},
  URN =		{urn:nbn:de:0030-drops-250524},
  doi =		{10.4230/OASIcs.RW.2024/2025.7},
  annote =	{Keywords: Datalog, query language, knowlegde representation and reasoning, logic programming, Horn logic, SPARQL, datatypes and aggregation, lecture notes, tutorial}
}
Document
DOI: 10.4230/DagRep.15.2.89
Semirings in Databases, Automata, and Logic (Dagstuhl Seminar 25081)

Authors: Guillermo Badia, Manfred Droste, Phokion G. Kolaitis, Carles Noguera, Sophie Brinke, Lovro Mrkonjić, and Gaia Petreni

Published in: Dagstuhl Reports, Volume 15, Issue 2 (2025)

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 25081 "Semirings in Databases, Automata, and Logic", which was held from February 16 to 21, 2025. The seminar focused on semirings, a class of algebraic structures with many applications in computer science, particularly in databases and automata. Semirings are used in databases to annotate tuples in the input and output relations of queries (in particular, in the case of bag semantics, using the semiring of natural numbers) allowing to model several relevant aspects of databases. In automata theory, semirings allow to define weighted automata, which have applications in natural language processing, speech recognition, and image compression. Moreover, semirings are strongly related to the algebraic semantics of many-valued logics. The seminar brought together researchers from the communities mentioned above, and it developed a research agenda for studying semirings, guided by a collection of diverse applications. This led to several new collaborations between members from different communities, including joint work for publications.
Cite as

Guillermo Badia, Manfred Droste, Phokion G. Kolaitis, Carles Noguera, Sophie Brinke, Lovro Mrkonjić, and Gaia Petreni. Semirings in Databases, Automata, and Logic (Dagstuhl Seminar 25081). In Dagstuhl Reports, Volume 15, Issue 2, pp. 89-109, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@Article{badia_et_al:DagRep.15.2.89,
  author =	{Badia, Guillermo and Droste, Manfred and Kolaitis, Phokion G. and Noguera, Carles and Brinke, Sophie and Mrkonji\'{c}, Lovro and Petreni, Gaia},
  title =	{{Semirings in Databases, Automata, and Logic (Dagstuhl Seminar 25081)}},
  pages =	{89--109},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2025},
  volume =	{15},
  number =	{2},
  editor =	{Badia, Guillermo and Droste, Manfred and Kolaitis, Phokion G. and Noguera, Carles and Brinke, Sophie and Mrkonji\'{c}, Lovro and Petreni, Gaia},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.15.2.89},
  URN =		{urn:nbn:de:0030-drops-230893},
  doi =		{10.4230/DagRep.15.2.89},
  annote =	{Keywords: databases, finite model theory, multi-valued logic, provenance, semirings, weighted automata, weighted logic}
}
Document
DOI: 10.4230/LIPIcs.ESA.2025.29
The Tape Reconfiguration Problem and Its Consequences for Dominating Set Reconfiguration

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

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

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

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

Copy BibTex To Clipboard

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

Authors: Georg Schindling

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

Abstract
The notion of homomorphism indistinguishability offers a combinatorial framework for characterizing equivalence relations of graphs, in particular equivalences in counting logics within finite model theory. That is, for certain graph classes, two structures agree on all homomorphism counts from the class if and only if they satisfy the same sentences in a corresponding logic. This perspective often reveals connections between the combinatorial properties of graph classes and the syntactic structure of logical fragments. In this work, we extend this perspective to logics with restricted requantification, refining the stratification of logical resources in finite-variable counting logics. Specifically, we generalize Lovász-type theorems for these logics with either restricted conjunction or bounded quantifier-rank and present new combinatorial proofs of existing results. To this end, we introduce novel path and tree decompositions that incorporate the concept of reusability and develop characterizations based on pursuit-evasion games. Leveraging this framework, we establish that classes of bounded pathwidth and treewidth with reusability constraints are homomorphism distinguishing closed. Finally, we develop a comonadic perspective on requantification by constructing new comonads that encapsulate restricted-reusability pebble games. We show a tight correspondence between their coalgebras and path/tree decompositions, yielding categorical characterizations of reusability in graph decompositions. This unifies logical, combinatorial, and categorical perspectives on the notion of reusability.
Cite as

Georg Schindling. Homomorphism Indistinguishability and Game Comonads for Restricted Conjunction and Requantification. In 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 345, pp. 89:1-89:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{schindling:LIPIcs.MFCS.2025.89,
  author =	{Schindling, Georg},
  title =	{{Homomorphism Indistinguishability and Game Comonads for Restricted Conjunction and Requantification}},
  booktitle =	{50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)},
  pages =	{89:1--89: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.89},
  URN =		{urn:nbn:de:0030-drops-241962},
  doi =		{10.4230/LIPIcs.MFCS.2025.89},
  annote =	{Keywords: homomorphism indistinguishability, game comonads, finite variable counting logic, restricted conjunction, restricted requantification, tree decomposition, path decomposition}
}
  • Refine by Type
  • 77 Document/PDF
  • 35 Document/HTML
  • 1 Volume

  • Refine by Publication Year
  • 8 2026
  • 24 2025
  • 3 2024
  • 2 2023
  • 2 2022
  • Show More...

  • Refine by Author
  • 24 Kolaitis, Phokion G.
  • 5 Grohe, Martin
  • 4 Bulatov, Andrei A.
  • 4 ten Cate, Balder
  • 3 Fagin, Ronald
  • Show More...

  • Refine by Series/Journal
  • 43 LIPIcs
  • 2 OASIcs
  • 2 TGDK
  • 6 DagRep
  • 12 DFU
  • Show More...

  • Refine by Classification
  • 11 Theory of computation → Finite Model Theory
  • 7 Theory of computation → Complexity theory and logic
  • 6 Theory of computation → Logic
  • 5 Theory of computation → Problems, reductions and completeness
  • 4 Theory of computation → Logic and databases
  • Show More...

  • Refine by Keyword
  • 8 finite model theory
  • 6 data exchange
  • 5 computational complexity
  • 5 constraint satisfaction
  • 4 complexity
  • 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