Search Results

Documents authored by Tantow, Johannes

Document
DOI: 10.4230/LIPIcs.ESA.2025.56
PLS-Completeness of String Permutations

Authors: Dominik Scheder and Johannes Tantow

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

Abstract
Bitstrings can be permuted via permutations and compared via the lexicographic order. In this paper we study the complexity of finding a minimum of a bitstring via given permutations. As finding a global optimum is known to be NP-complete [László Babai and Eugene M. Luks, 1983], we study the local optima via the class PLS [David S. Johnson et al., 1988] and show hardness for PLS. Additionally, we show that even for one permutation the global optimization problem is NP-complete and give a formula that has these permutation as its symmetries. This answers an open question inspired from Kołodziejczyk and Thapen [Leszek Aleksander Kolodziejczyk and Neil Thapen, 2024] and stated at the SAT and interactions seminar in Dagstuhl.
Cite as

Dominik Scheder and Johannes Tantow. PLS-Completeness of String Permutations. In 33rd Annual European Symposium on Algorithms (ESA 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 351, pp. 56:1-56:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{scheder_et_al:LIPIcs.ESA.2025.56,
  author =	{Scheder, Dominik and Tantow, Johannes},
  title =	{{PLS-Completeness of String Permutations}},
  booktitle =	{33rd Annual European Symposium on Algorithms (ESA 2025)},
  pages =	{56:1--56:14},
  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.56},
  URN =		{urn:nbn:de:0030-drops-245245},
  doi =		{10.4230/LIPIcs.ESA.2025.56},
  annote =	{Keywords: PLS, total search problems, local search, permutation groups, symmetry}
}
Artifact
Software
DOI: 10.4230/artifacts.23826
knowsys/CertifyingDatalog

Authors: Johannes Tantow, Lukas Gerlach, Stephan Mennicke, and Markus Krötzsch

Abstract
Cite as

Johannes Tantow, Lukas Gerlach, Stephan Mennicke, Markus Krötzsch. knowsys/CertifyingDatalog (Software, Lean Formalization). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@misc{dagstuhl-artifact-23826,
   title = {{knowsys/CertifyingDatalog}}, 
   author = {Tantow, Johannes and Gerlach, Lukas and Mennicke, Stephan and Kr\"{o}tzsch, Markus},
   note = {Software, version 0.2.0., swhId: \href{https://archive.softwareheritage.org/swh:1:dir:57aca8aba4c9f62a87ba52360ad701b8e9cf7b45;origin=https://github.com/knowsys/CertifyingDatalog;visit=swh:1:snp:617e84a1a49818c83a6a7c32cda6267fc6f09596;anchor=swh:1:rev:7adf4abd7826dd529491551f192c5815d430313a}{\texttt{swh:1:dir:57aca8aba4c9f62a87ba52360ad701b8e9cf7b45}} (visited on 2025-09-22)},
   url = {https://github.com/knowsys/CertifyingDatalog/tree/v0.2.0},
   doi = {10.4230/artifacts.23826},
}
Document
DOI: 10.4230/LIPIcs.ITP.2025.36
Verifying Datalog Reasoning with Lean

Authors: Johannes Tantow, Lukas Gerlach, Stephan Mennicke, and Markus Krötzsch

Published in: LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025)

Abstract
Datalog is an essential logical rule language with many applications, and modern rule engines compute logical consequences for Datalog with high performance and scalability. While Datalog is rather simple and, in principle, explainable by design, such sophisticated implementations and optimizations are hard to verify. We therefore propose a certificate-based approach to validate results of Datalog reasoners in a formally verified checker for Datalog proofs. Using the proof assistant Lean, we implement such a checker and verify its correctness against direct formalizations of the Datalog semantics. We propose two JSON encodings for Datalog proofs: one using the widely supported Datalog proof trees, and one using directed acyclic graphs for succinctness. To evaluate the practical feasibility and performance of our approach, we validate proofs that we obtain by converting derivation traces of an existing Datalog reasoner into our tool-independent format.
Cite as

Johannes Tantow, Lukas Gerlach, Stephan Mennicke, and Markus Krötzsch. Verifying Datalog Reasoning with Lean. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 36:1-36:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{tantow_et_al:LIPIcs.ITP.2025.36,
  author =	{Tantow, Johannes and Gerlach, Lukas and Mennicke, Stephan and Kr\"{o}tzsch, Markus},
  title =	{{Verifying Datalog Reasoning with Lean}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{36:1--36:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-396-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{352},
  editor =	{Forster, Yannick and Keller, Chantal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.36},
  URN =		{urn:nbn:de:0030-drops-246342},
  doi =		{10.4230/LIPIcs.ITP.2025.36},
  annote =	{Keywords: Certifying Algorithms, Datalog, Formal Verification}
}
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact