Search Results

Documents authored by Berkholz, Christoph

Document
DOI: 10.4230/LIPIcs.STACS.2024.11
A Characterization of Efficiently Compilable Constraint Languages

Authors: Christoph Berkholz, Stefan Mengel, and Hermann Wilhelm

Published in: LIPIcs, Volume 289, 41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024)

Abstract
A central task in knowledge compilation is to compile a CNF-SAT instance into a succinct representation format that allows efficient operations such as testing satisfiability, counting, or enumerating all solutions. Useful representation formats studied in this area range from ordered binary decision diagrams (OBDDs) to circuits in decomposable negation normal form (DNNFs). While it is known that there exist CNF formulas that require exponential size representations, the situation is less well studied for other types of constraints than Boolean disjunctive clauses. The constraint satisfaction problem (CSP) is a powerful framework that generalizes CNF-SAT by allowing arbitrary sets of constraints over any finite domain. The main goal of our work is to understand for which type of constraints (also called the constraint language) it is possible to efficiently compute representations of polynomial size. We answer this question completely and prove two tight characterizations of efficiently compilable constraint languages, depending on whether target format is structured. We first identify the combinatorial property of "strong blockwise decomposability" and show that if a constraint language has this property, we can compute DNNF representations of linear size. For all other constraint languages we construct families of CSP-instances that provably require DNNFs of exponential size. For a subclass of "strong uniformly blockwise decomposable" constraint languages we obtain a similar dichotomy for structured DNNFs. In fact, strong (uniform) blockwise decomposability even allows efficient compilation into multi-valued analogs of OBDDs and FBDDs, respectively. Thus, we get complete characterizations for all knowledge compilation classes between O(B)DDs and DNNFs.
Cite as

Christoph Berkholz, Stefan Mengel, and Hermann Wilhelm. A Characterization of Efficiently Compilable Constraint Languages. In 41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 289, pp. 11:1-11:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{berkholz_et_al:LIPIcs.STACS.2024.11,
  author =	{Berkholz, Christoph and Mengel, Stefan and Wilhelm, Hermann},
  title =	{{A Characterization of Efficiently Compilable Constraint Languages}},
  booktitle =	{41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024)},
  pages =	{11:1--11:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-311-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{289},
  editor =	{Beyersdorff, Olaf and Kant\'{e}, Mamadou Moustapha and Kupferman, Orna and Lokshtanov, Daniel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2024.11},
  URN =		{urn:nbn:de:0030-drops-197214},
  doi =		{10.4230/LIPIcs.STACS.2024.11},
  annote =	{Keywords: constraint satisfaction, knowledge compilation, dichotomy, DNNF}
}
Document
DOI: 10.4230/LIPIcs.STACS.2024.12
Modal Logic Is More Succinct Iff Bi-Implication Is Available in Some Form

Authors: Christoph Berkholz, Dietrich Kuske, and Christian Schwarz

Published in: LIPIcs, Volume 289, 41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024)

Abstract
Is it possible to write significantly smaller formulae, when using more Boolean operators in addition to the De Morgan basis (and, or, not)? For propositional logic a negative answer was given by Pratt: every formula with additional operators can be translated to the De Morgan basis with only polynomial increase in size. Surprisingly, for modal logic the picture is different: we show that adding bi-implication allows to write exponentially smaller formulae. Moreover, we provide a complete classification of finite sets of Boolean operators showing they are either of no help (allow polynomial translations to the De Morgan basis) or can express properties as succinct as modal logic with additional bi-implication. More precisely, these results are shown for the modal logic T (and therefore for K). We complement this result showing that the modal logic S5 behaves as propositional logic: no additional Boolean operators make it possible to write significantly smaller formulae.
Cite as

Christoph Berkholz, Dietrich Kuske, and Christian Schwarz. Modal Logic Is More Succinct Iff Bi-Implication Is Available in Some Form. In 41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 289, pp. 12:1-12:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{berkholz_et_al:LIPIcs.STACS.2024.12,
  author =	{Berkholz, Christoph and Kuske, Dietrich and Schwarz, Christian},
  title =	{{Modal Logic Is More Succinct Iff Bi-Implication Is Available in Some Form}},
  booktitle =	{41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024)},
  pages =	{12:1--12:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-311-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{289},
  editor =	{Beyersdorff, Olaf and Kant\'{e}, Mamadou Moustapha and Kupferman, Orna and Lokshtanov, Daniel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2024.12},
  URN =		{urn:nbn:de:0030-drops-197228},
  doi =		{10.4230/LIPIcs.STACS.2024.12},
  annote =	{Keywords: succinctness, modal logic}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2023.113
A Dichotomy for Succinct Representations of Homomorphisms

Authors: Christoph Berkholz and Harry Vinall-Smeeth

Published in: LIPIcs, Volume 261, 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023)

Abstract
The task of computing homomorphisms between two finite relational structures A and B is a well-studied question with numerous applications. Since the set Hom(A, B) of all homomorphisms may be very large having a method of representing it in a succinct way, especially one which enables us to perform efficient enumeration and counting, could be extremely useful. One simple yet powerful way of doing so is to decompose Hom(A, B) using union and Cartesian product. Such data structures, called d-representations, have been introduced by Olteanu and Závodný [Olteanu and Závodný, 2015] in the context of database theory. Their results also imply that if the treewidth of the left-hand side structure A is bounded, then a d-representation of polynomial size can be found in polynomial time. We show that for structures of bounded arity this is optimal: if the treewidth is unbounded then there are instances where the size of any d-representation is superpolynomial. Along the way we develop tools for proving lower bounds on the size of d-representations, in particular we define a notion of reduction suitable for this context and prove an almost tight lower bound on the size of d-representations of all k-cliques in a graph.
Cite as

Christoph Berkholz and Harry Vinall-Smeeth. A Dichotomy for Succinct Representations of Homomorphisms. In 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 261, pp. 113:1-113:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{berkholz_et_al:LIPIcs.ICALP.2023.113,
  author =	{Berkholz, Christoph and Vinall-Smeeth, Harry},
  title =	{{A Dichotomy for Succinct Representations of Homomorphisms}},
  booktitle =	{50th International Colloquium on Automata, Languages, and Programming (ICALP 2023)},
  pages =	{113:1--113:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-278-5},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{261},
  editor =	{Etessami, Kousha and Feige, Uriel 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.2023.113},
  URN =		{urn:nbn:de:0030-drops-181653},
  doi =		{10.4230/LIPIcs.ICALP.2023.113},
  annote =	{Keywords: homomorphism problem, CSP, succinct representations, enumeration, lower bound, treewidth}
}
Document
DOI: 10.4230/DagRep.12.1.101
Finite and Algorithmic Model Theory (Dagstuhl Seminar 22051)

Authors: Albert Atserias, Christoph Berkholz, Kousha Etessami, and Joanna Ochremiak

Published in: Dagstuhl Reports, Volume 12, Issue 1 (2022)

Abstract
Finite and algorithmic model theory (FAMT) studies the expressive power of logical languages on finite structures or, more generally, structures that can be finitely presented. These are the structures that serve as input to computation, and for this reason the study of FAMT is intimately connected with computer science. Over the last four decades, the subject has developed through a close interaction between theoretical computer science and related areas of mathematics, including logic and combinatorics. This report documents the program and the outcomes of Dagstuhl Seminar 22051 "Finite and Algorithmic Model Theory".
Cite as

Albert Atserias, Christoph Berkholz, Kousha Etessami, and Joanna Ochremiak. Finite and Algorithmic Model Theory (Dagstuhl Seminar 22051). In Dagstuhl Reports, Volume 12, Issue 1, pp. 101-118, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@Article{atserias_et_al:DagRep.12.1.101,
  author =	{Atserias, Albert and Berkholz, Christoph and Etessami, Kousha and Ochremiak, Joanna},
  title =	{{Finite and Algorithmic Model Theory (Dagstuhl Seminar 22051)}},
  pages =	{101--118},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2022},
  volume =	{12},
  number =	{1},
  editor =	{Atserias, Albert and Berkholz, Christoph and Etessami, Kousha and Ochremiak, Joanna},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.12.1.101},
  URN =		{urn:nbn:de:0030-drops-169232},
  doi =		{10.4230/DagRep.12.1.101},
  annote =	{Keywords: automata and game theory, database theory, descriptive complexity, finite model theory, homomorphism counts, Query enumeration}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2019.58
Constant Delay Enumeration with FPT-Preprocessing for Conjunctive Queries of Bounded Submodular Width

Authors: Christoph Berkholz and Nicole Schweikardt

Published in: LIPIcs, Volume 138, 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)

Abstract
Marx (STOC 2010, J. ACM 2013) introduced the notion of submodular width of a conjunctive query (CQ) and showed that for any class Phi of Boolean CQs of bounded submodular width, the model-checking problem for Phi on the class of all finite structures is fixed-parameter tractable (FPT). Note that for non-Boolean queries, the size of the query result may be far too large to be computed entirely within FPT time. We investigate the free-connex variant of submodular width and generalise Marx’s result to non-Boolean queries as follows: For every class Phi of CQs of bounded free-connex submodular width, within FPT-preprocessing time we can build a data structure that allows to enumerate, without repetition and with constant delay, all tuples of the query result. Our proof builds upon Marx’s splitting routine to decompose the query result into a union of results; but we have to tackle the additional technical difficulty to ensure that these can be enumerated efficiently.
Cite as

Christoph Berkholz and Nicole Schweikardt. Constant Delay Enumeration with FPT-Preprocessing for Conjunctive Queries of Bounded Submodular Width. In 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 138, pp. 58:1-58:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{berkholz_et_al:LIPIcs.MFCS.2019.58,
  author =	{Berkholz, Christoph and Schweikardt, Nicole},
  title =	{{Constant Delay Enumeration with FPT-Preprocessing for Conjunctive Queries of Bounded Submodular Width}},
  booktitle =	{44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)},
  pages =	{58:1--58:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-117-7},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{138},
  editor =	{Rossmanith, Peter and Heggernes, Pinar and Katoen, Joost-Pieter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2019.58},
  URN =		{urn:nbn:de:0030-drops-110021},
  doi =		{10.4230/LIPIcs.MFCS.2019.58},
  annote =	{Keywords: conjunctive queries, constant delay enumeration, hypertree decompositions, submodular width, fixed-parameter tractability}
}
Document
DOI: 10.4230/LIPIcs.ICDT.2018.8
Answering UCQs under Updates and in the Presence of Integrity Constraints

Authors: Christoph Berkholz, Jens Keppeler, and Nicole Schweikardt

Published in: LIPIcs, Volume 98, 21st International Conference on Database Theory (ICDT 2018)

Abstract
We investigate the query evaluation problem for fixed queries over fully dynamic databases where tuples can be inserted or deleted. The task is to design a dynamic data structure that can immediately report the new result of a fixed query after every database update. We consider unions of conjunctive queries (UCQs) and focus on the query evaluation tasks testing (decide whether an input tuple belongs to the query result), enumeration (enumerate, without repetition, all tuples in the query result), and counting (output the number of tuples in the query result). We identify three increasingly restrictive classes of UCQs which we call t-hierarchical, q-hierarchical, and exhaustively q-hierarchical UCQs. Our main results provide the following dichotomies: If the query's homomorphic core is t-hierarchical (q-hierarchical, exhaustively q-hierarchical), then the testing (enumeration, counting) problem can be solved with constant update time and constant testing time (delay, counting time). Otherwise, it cannot be solved with sublinear update time and sublinear testing time (delay, counting time), unless the OV-conjecture and/or the OMv-conjecture fails. We also study the complexity of query evaluation in the dynamic setting in the presence of integrity constraints, and we obtain similar dichotomy results for the special case of small domain constraints (i.e., constraints which state that all values in a particular column of a relation belong to a fixed domain of constant size).
Cite as

Christoph Berkholz, Jens Keppeler, and Nicole Schweikardt. Answering UCQs under Updates and in the Presence of Integrity Constraints. In 21st International Conference on Database Theory (ICDT 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 98, pp. 8:1-8:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{berkholz_et_al:LIPIcs.ICDT.2018.8,
  author =	{Berkholz, Christoph and Keppeler, Jens and Schweikardt, Nicole},
  title =	{{Answering UCQs under Updates and in the Presence of Integrity Constraints}},
  booktitle =	{21st International Conference on Database Theory (ICDT 2018)},
  pages =	{8:1--8:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-063-7},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{98},
  editor =	{Kimelfeld, Benny and Amsterdamer, Yael},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICDT.2018.8},
  URN =		{urn:nbn:de:0030-drops-85990},
  doi =		{10.4230/LIPIcs.ICDT.2018.8},
  annote =	{Keywords: dynamic query evaluation, union of conjunctive queries, constant-delay enumeration, counting problem, testing}
}
Document
DOI: 10.4230/LIPIcs.STACS.2018.11
The Relation between Polynomial Calculus, Sherali-Adams, and Sum-of-Squares Proofs

Authors: Christoph Berkholz

Published in: LIPIcs, Volume 96, 35th Symposium on Theoretical Aspects of Computer Science (STACS 2018)

Abstract
We relate different approaches for proving the unsatisfiability of a system of real polynomial equations over Boolean variables. On the one hand, there are the static proof systems Sherali-Adams and sum-of-squares (a.k.a. Lasserre), which are based on linear and semi-definite programming relaxations. On the other hand, we consider polynomial calculus, which is a dynamic algebraic proof system that models Gröbner basis computations. Our first result is that sum-of-squares simulates polynomial calculus: any polynomial calculus refutation of degree d can be transformed into a sum-of-squares refutation of degree 2d and only polynomial increase in size. In contrast, our second result shows that this is not the case for Sherali-Adams: there are systems of polynomial equations that have polynomial calculus refutations of degree 3 and polynomial size, but require Sherali-Adams refutations of large degree and exponential size. A corollary of our first result is that the proof systems Positivstellensatz and Positivstellensatz Calculus, which have been separated over non-Boolean polynomials, simulate each other in the presence of Boolean axioms.
Cite as

Christoph Berkholz. The Relation between Polynomial Calculus, Sherali-Adams, and Sum-of-Squares Proofs. In 35th Symposium on Theoretical Aspects of Computer Science (STACS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 96, pp. 11:1-11:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{berkholz:LIPIcs.STACS.2018.11,
  author =	{Berkholz, Christoph},
  title =	{{The Relation between Polynomial Calculus, Sherali-Adams, and Sum-of-Squares Proofs}},
  booktitle =	{35th Symposium on Theoretical Aspects of Computer Science (STACS 2018)},
  pages =	{11:1--11:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-062-0},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{96},
  editor =	{Niedermeier, Rolf and Vall\'{e}e, Brigitte},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2018.11},
  URN =		{urn:nbn:de:0030-drops-85279},
  doi =		{10.4230/LIPIcs.STACS.2018.11},
  annote =	{Keywords: Proof Complexity, Polynomial Calculus, Sum-of-Squares, Sherali-Adams}
}
Document
DOI: 10.4230/LIPIcs.ICDT.2017.8
Answering FO+MOD Queries Under Updates on Bounded Degree Databases

Authors: Christoph Berkholz, Jens Keppeler, and Nicole Schweikardt

Published in: LIPIcs, Volume 68, 20th International Conference on Database Theory (ICDT 2017)

Abstract
We investigate the query evaluation problem for fixed queries over fully dynamic databases, where tuples can be inserted or deleted. The task is to design a dynamic algorithm that immediately reports the new result of a fixed query after every database update. We consider queries in first-order logic (FO) and its extension with modulo-counting quantifiers (FO+MOD), and show that they can be efficiently evaluated under updates, provided that the dynamic database does not exceed a certain degree bound. In particular, we construct a data structure that allows to answer a Boolean FO+MOD query and to compute the size of the query result within constant time after every database update. Furthermore, after every update we are able to immediately enumerate the new query result with constant delay between the output tuples. The time needed to build the data structure is linear in the size of the database. Our results extend earlier work on the evaluation of first-order queries on static databases of bounded degree and rely on an effective Hanf normal form for FO+MOD recently obtained by [Heimberg, Kuske, and Schweikardt, LICS, 2016].
Cite as

Christoph Berkholz, Jens Keppeler, and Nicole Schweikardt. Answering FO+MOD Queries Under Updates on Bounded Degree Databases. In 20th International Conference on Database Theory (ICDT 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 68, pp. 8:1-8:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{berkholz_et_al:LIPIcs.ICDT.2017.8,
  author =	{Berkholz, Christoph and Keppeler, Jens and Schweikardt, Nicole},
  title =	{{Answering FO+MOD Queries Under Updates on Bounded Degree Databases}},
  booktitle =	{20th International Conference on Database Theory (ICDT 2017)},
  pages =	{8:1--8:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-024-8},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{68},
  editor =	{Benedikt, Michael and Orsi, Giorgio},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICDT.2017.8},
  URN =		{urn:nbn:de:0030-drops-70535},
  doi =		{10.4230/LIPIcs.ICDT.2017.8},
  annote =	{Keywords: dynamic databases, query enumeration, counting problem, first-order logic with modulo-counting quantifiers, Hanf locality}
}
Document
DOI: 10.4230/LIPIcs.ICALP.2016.57
Supercritical Space-Width Trade-Offs for Resolution

Authors: Christoph Berkholz and Jakob Nordström

Published in: LIPIcs, Volume 55, 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)

Abstract
We show that there are CNF formulas which can be refuted in resolution in both small space and small width, but for which any small-width resolution proof must have space exceeding by far the linear worst-case upper bound. This significantly strengthens the space-width trade-offs in [Ben-Sasson 2009], and provides one more example of trade-offs in the "supercritical" regime above worst case recently identified by [Razborov 2016]. We obtain our results by using Razborov’s new hardness condensation technique and combining it with the space lower bounds in [Ben-Sasson and Nordström 2008].
Cite as

Christoph Berkholz and Jakob Nordström. Supercritical Space-Width Trade-Offs for Resolution. In 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 55, pp. 57:1-57:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{berkholz_et_al:LIPIcs.ICALP.2016.57,
  author =	{Berkholz, Christoph and Nordstr\"{o}m, Jakob},
  title =	{{Supercritical Space-Width Trade-Offs for Resolution}},
  booktitle =	{43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)},
  pages =	{57:1--57:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-013-2},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{55},
  editor =	{Chatzigiannakis, Ioannis and Mitzenmacher, Michael and Rabani, Yuval and Sangiorgi, Davide},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2016.57},
  URN =		{urn:nbn:de:0030-drops-62266},
  doi =		{10.4230/LIPIcs.ICALP.2016.57},
  annote =	{Keywords: Proof complexity, resolution, space, width, trade-offs, supercritical}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2014.109
Parameterized Complexity of Fixed Variable Logics

Authors: Christoph Berkholz and Michael Elberfeld

Published in: LIPIcs, Volume 29, 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)

Abstract
We study the complexity of model checking formulas in first-order logic parameterized by the number of distinct variables in the formula. This problem, which is not known to be fixed-parameter tractable, resisted to be properly classified in the context of parameterized complexity. We show that it is complete for a newly-defined complexity class that we propose as an analog of the classical class PSPACE in parameterized complexity. We support this intuition by the following findings: First, the proposed class admits a definition in terms of alternating Turing machines in a similar way as PSPACE can be defined in terms of polynomial-time alternating machines. Second, we show that parameterized versions of other PSPACE-complete problems, like winning certain pebble games and finding restricted resolution refutations, are complete for this class.
Cite as

Christoph Berkholz and Michael Elberfeld. Parameterized Complexity of Fixed Variable Logics. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 109-120, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@InProceedings{berkholz_et_al:LIPIcs.FSTTCS.2014.109,
  author =	{Berkholz, Christoph and Elberfeld, Michael},
  title =	{{Parameterized Complexity of Fixed Variable Logics}},
  booktitle =	{34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
  pages =	{109--120},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-77-4},
  ISSN =	{1868-8969},
  year =	{2014},
  volume =	{29},
  editor =	{Raman, Venkatesh and Suresh, S. P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.109},
  URN =		{urn:nbn:de:0030-drops-48367},
  doi =		{10.4230/LIPIcs.FSTTCS.2014.109},
  annote =	{Keywords: Parameterized complexity, polynomial space, first-order logic, pebble games, regular resolutions}
}
Document
DOI: 10.4230/LIPIcs.CSL.2013.61
Bounds for the quantifier depth in finite-variable logics: Alternation hierarchy

Authors: Christoph Berkholz, Andreas Krebs, and Oleg Verbitsky

Published in: LIPIcs, Volume 23, Computer Science Logic 2013 (CSL 2013)

Abstract
Given two structures G and H distinguishable in FO^k (first-order logic with k variables), let A^k(G,H) denote the minimum alternation depth of a FO^k formula distinguishing G from H. Let A^k(n) be the maximum value of A^k(G,H) over n-element structures. We prove the strictness of the quantifier alternation hierarchy of FO^2 in a strong quantitative form, namely A^2(n) >= n/8-2, which is tight up to a constant factor. For each k >= 2, it holds that A^k(n) > log_(k+1) n-2 even over colored trees, which is also tight up to a constant factor if k >= 3. For k >= 3 the last lower bound holds also over uncolored trees, while the alternation hierarchy of FO^2 collapses even over all uncolored graphs. We also show examples of colored graphs G and H on n vertices that can be distinguished in FO^2 much more succinctly if the alternation number is increased just by one: while in Sigma_i it is possible to distinguish G from H with bounded quantifier depth, in Pi_i this requires quantifier depth Omega(n2). The quadratic lower bound is best possible here because, if G and H can be distinguished in FO^k with i quantifier alternations, this can be done with quantifier depth n^(2k-2).
Cite as

Christoph Berkholz, Andreas Krebs, and Oleg Verbitsky. Bounds for the quantifier depth in finite-variable logics: Alternation hierarchy. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 61-80, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@InProceedings{berkholz_et_al:LIPIcs.CSL.2013.61,
  author =	{Berkholz, Christoph and Krebs, Andreas and Verbitsky, Oleg},
  title =	{{Bounds for the quantifier depth in finite-variable logics: Alternation hierarchy}},
  booktitle =	{Computer Science Logic 2013 (CSL 2013)},
  pages =	{61--80},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-60-6},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{23},
  editor =	{Ronchi Della Rocca, Simona},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.61},
  URN =		{urn:nbn:de:0030-drops-41907},
  doi =		{10.4230/LIPIcs.CSL.2013.61},
  annote =	{Keywords: Alternation hierarchy, finite-variable logic}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact