5 Search Results for "Lichter, Moritz"

Document
DOI: 10.4230/LIPIcs.CSL.2024.36
Limitations of Game Comonads for Invertible-Map Equivalence via Homomorphism Indistinguishability

Authors: Moritz Lichter, Benedikt Pago, and Tim Seppelt

Published in: LIPIcs, Volume 288, 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)

Abstract
Abramsky, Dawar, and Wang (2017) introduced the pebbling comonad for k-variable counting logic and thereby initiated a line of work that imports category theoretic machinery to finite model theory. Such game comonads have been developed for various logics, yielding characterisations of logical equivalences in terms of isomorphisms in the associated co-Kleisli category. We show a first limitation of this approach by studying linear-algebraic logic, which is strictly more expressive than first-order counting logic and whose k-variable logical equivalence relations are known as invertible-map equivalences (IM). We show that there exists no finite-rank comonad on the category of graphs whose co-Kleisli isomorphisms characterise IM-equivalence, answering a question of Ó Conghaile and Dawar (CSL 2021). We obtain this result by ruling out a characterisation of IM-equivalence in terms of homomorphism indistinguishability and employing the Lovász-type theorem for game comonads established by Reggio (2022). Two graphs are homomorphism indistinguishable over a graph class if they admit the same number of homomorphisms from every graph in the class. The IM-equivalences cannot be characterised in this way, neither when counting homomorphisms in the natural numbers, nor in any finite prime field.
Cite as

Moritz Lichter, Benedikt Pago, and Tim Seppelt. Limitations of Game Comonads for Invertible-Map Equivalence via Homomorphism Indistinguishability. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 36:1-36:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{lichter_et_al:LIPIcs.CSL.2024.36,
  author =	{Lichter, Moritz and Pago, Benedikt and Seppelt, Tim},
  title =	{{Limitations of Game Comonads for Invertible-Map Equivalence via Homomorphism Indistinguishability}},
  booktitle =	{32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
  pages =	{36:1--36:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-310-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{288},
  editor =	{Murano, Aniello and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.36},
  URN =		{urn:nbn:de:0030-drops-196799},
  doi =		{10.4230/LIPIcs.CSL.2024.36},
  annote =	{Keywords: finite model theory, graph isomorphism, linear-algebraic logic, homomorphism indistinguishability, game comonads, invertible-map equivalence}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2023.133
Witnessed Symmetric Choice and Interpretations in Fixed-Point Logic with Counting

Authors: Moritz Lichter

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

Abstract
At the core of the quest for a logic for Ptime is a mismatch between algorithms making arbitrary choices and isomorphism-invariant logics. One approach to tackle this problem is witnessed symmetric choice. It allows for choices from definable orbits certified by definable witnessing automorphisms. We consider the extension of fixed-point logic with counting (IFPC) with witnessed symmetric choice (IFPC+WSC) and a further extension with an interpretation operator (IFPC+WSC+I). The latter operator evaluates a subformula in the structure defined by an interpretation. When similarly extending pure fixed-point logic (IFP), IFP+WSC+I simulates counting which IFP+WSC fails to do. For IFPC+WSC, it is unknown whether the interpretation operator increases expressiveness and thus allows studying the relation between WSC and interpretations beyond counting. In this paper, we separate IFPC+WSC from IFPC+WSC+I by showing that IFPC+WSC is not closed under FO-interpretations. By the same argument, we answer an open question of Dawar and Richerby regarding non-witnessed symmetric choice in IFP. Additionally, we prove that nesting WSC-operators increases the expressiveness using the so-called CFI graphs. We show that if IFPC+WSC+I canonizes a particular class of base graphs, then it also canonizes the corresponding CFI graphs. This differs from various other logics, where CFI graphs provide difficult instances.
Cite as

Moritz Lichter. Witnessed Symmetric Choice and Interpretations in Fixed-Point Logic with Counting. In 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 261, pp. 133:1-133:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{lichter:LIPIcs.ICALP.2023.133,
  author =	{Lichter, Moritz},
  title =	{{Witnessed Symmetric Choice and Interpretations in Fixed-Point Logic with Counting}},
  booktitle =	{50th International Colloquium on Automata, Languages, and Programming (ICALP 2023)},
  pages =	{133:1--133:20},
  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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2023.133},
  URN =		{urn:nbn:de:0030-drops-181858},
  doi =		{10.4230/LIPIcs.ICALP.2023.133},
  annote =	{Keywords: witnessed symmetric choice, interpretation, fixed-point logic, counting, CFI graphs, logic for PTime}
}
Document
DOI: 10.4230/LIPIcs.SAT.2022.1
SAT Preprocessors and Symmetry

Authors: Markus Anders

Published in: LIPIcs, Volume 236, 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)

Abstract
Exploitation of symmetries is an indispensable approach to solve certain classes of difficult SAT instances. Numerous techniques for the use of symmetry in SAT have evolved over the past few decades. But no matter how symmetries are used precisely, they have to be detected first. We investigate how to detect more symmetry, faster. The initial idea is to reap the benefits of SAT preprocessing for symmetry detection. As it turns out, applying an off-the-shelf preprocessor before handling symmetry runs into problems: the preprocessor can haphazardly remove symmetry from formulas, severely impeding symmetry exploitation. Our main contribution is a theoretical framework that captures the relationship of SAT preprocessing techniques and symmetry. Based on this, we create a symmetry-aware preprocessor that can be applied safely before handling symmetry. We then demonstrate that applying the preprocessor does not only substantially decrease symmetry detection and breaking times, but also uncovers hidden symmetry not detectable in the original instances. Overall, we depart the conventional view of treating symmetry detection as a black-box, presenting a new application-specific approach to symmetry detection in SAT.
Cite as

Markus Anders. SAT Preprocessors and Symmetry. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 1:1-1:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{anders:LIPIcs.SAT.2022.1,
  author =	{Anders, Markus},
  title =	{{SAT Preprocessors and Symmetry}},
  booktitle =	{25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
  pages =	{1:1--1:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-242-6},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{236},
  editor =	{Meel, Kuldeep S. and Strichman, Ofer},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.1},
  URN =		{urn:nbn:de:0030-drops-166752},
  doi =		{10.4230/LIPIcs.SAT.2022.1},
  annote =	{Keywords: boolean satisfiability, symmetry exploitation, graph isomorphism}
}
Document
DOI: 10.4230/LIPIcs.ESA.2021.6
Parallel Computation of Combinatorial Symmetries

Authors: Markus Anders and Pascal Schweitzer

Published in: LIPIcs, Volume 204, 29th Annual European Symposium on Algorithms (ESA 2021)

Abstract
In practice symmetries of combinatorial structures are computed by transforming the structure into an annotated graph whose automorphisms correspond exactly to the desired symmetries. An automorphism solver is then employed to compute the automorphism group of the constructed graph. Such solvers have been developed for over 50 years, and highly efficient sequential, single core tools are available. However no competitive parallel tools are available for the task. We introduce a new parallel randomized algorithm that is based on a modification of the individualization-refinement paradigm used by sequential solvers. The use of randomization crucially enables parallelization. We report extensive benchmark results that show that our solver is competitive to state-of-the-art solvers on a single thread, while scaling remarkably well with the use of more threads. This results in order-of-magnitude improvements on many graph classes over state-of-the-art solvers. In fact, our tool is the first parallel graph automorphism tool that outperforms current sequential tools.
Cite as

Markus Anders and Pascal Schweitzer. Parallel Computation of Combinatorial Symmetries. In 29th Annual European Symposium on Algorithms (ESA 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 204, pp. 6:1-6:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{anders_et_al:LIPIcs.ESA.2021.6,
  author =	{Anders, Markus and Schweitzer, Pascal},
  title =	{{Parallel Computation of Combinatorial Symmetries}},
  booktitle =	{29th Annual European Symposium on Algorithms (ESA 2021)},
  pages =	{6:1--6:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-204-4},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{204},
  editor =	{Mutzel, Petra and Pagh, Rasmus and Herman, Grzegorz},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ESA.2021.6},
  URN =		{urn:nbn:de:0030-drops-145875},
  doi =		{10.4230/LIPIcs.ESA.2021.6},
  annote =	{Keywords: graph isomorphism, automorphism groups, algorithm engineering, parallel algorithms}
}
Document
DOI: 10.4230/LIPIcs.CSL.2021.31
Canonization for Bounded and Dihedral Color Classes in Choiceless Polynomial Time

Authors: Moritz Lichter and Pascal Schweitzer

Published in: LIPIcs, Volume 183, 29th EACSL Annual Conference on Computer Science Logic (CSL 2021)

Abstract
In the quest for a logic capturing Ptime the next natural classes of structures to consider are those with bounded color class size. We present a canonization procedure for graphs with dihedral color classes of bounded size in the logic of Choiceless Polynomial Time (CPT), which then captures Ptime on this class of structures. This is the first result of this form for non-abelian color classes. The first step proposes a normal form which comprises a "rigid assemblage". This roughly means that the local automorphism groups form 2-injective 3-factor subdirect products. Structures with color classes of bounded size can be reduced canonization preservingly to normal form in CPT. In the second step, we show that for graphs in normal form with dihedral color classes of bounded size, the canonization problem can be solved in CPT. We also show the same statement for general ternary structures in normal form if the dihedral groups are defined over odd domains.
Cite as

Moritz Lichter and Pascal Schweitzer. Canonization for Bounded and Dihedral Color Classes in Choiceless Polynomial Time. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 31:1-31:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{lichter_et_al:LIPIcs.CSL.2021.31,
  author =	{Lichter, Moritz and Schweitzer, Pascal},
  title =	{{Canonization for Bounded and Dihedral Color Classes in Choiceless Polynomial Time}},
  booktitle =	{29th EACSL Annual Conference on Computer Science Logic (CSL 2021)},
  pages =	{31:1--31:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-175-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{183},
  editor =	{Baier, Christel and Goubault-Larrecq, Jean},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2021.31},
  URN =		{urn:nbn:de:0030-drops-134650},
  doi =		{10.4230/LIPIcs.CSL.2021.31},
  annote =	{Keywords: Choiceless polynomial time, canonization, relational structures, bounded color class size, dihedral groups}
}
  • Refine by Author
  • 3 Lichter, Moritz
  • 2 Anders, Markus
  • 2 Schweitzer, Pascal
  • 1 Pago, Benedikt
  • 1 Seppelt, Tim

  • Refine by Classification
  • 3 Theory of computation → Complexity theory and logic
  • 3 Theory of computation → Finite Model Theory
  • 2 Mathematics of computing → Graph algorithms
  • 1 Theory of computation → Graph algorithms analysis
  • 1 Theory of computation → Shared memory algorithms

  • Refine by Keyword
  • 3 graph isomorphism
  • 1 CFI graphs
  • 1 Choiceless polynomial time
  • 1 algorithm engineering
  • 1 automorphism groups
  • Show More...

  • Refine by Type
  • 5 document

  • Refine by Publication Year
  • 2 2021
  • 1 2022
  • 1 2023
  • 1 2024

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 Imprint Privacy Contact