4 Search Results for "Olsák, Miroslav"

Document
DOI: 10.4230/LIPIcs.STACS.2026.15
The Complexity of Resilience for Digraph Queries

Authors: Manuel Bodirsky and Žaneta Semanišinová

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

Abstract
We prove a complexity dichotomy for the resilience problem for unions of conjunctive digraph queries (i.e., for existential positive sentences over the signature {R} of directed graphs). Specifically, for every union μ of conjunctive digraph queries, the following problem is in P or NP-complete: given a directed multigraph G and a natural number u, can we remove u edges from G so that G ⊧ ¬ μ? In fact, we verify a more general dichotomy conjecture from [Bodirsky et al., 2024] for all resilience problems in the special case of directed graphs, and show that for such unions of queries μ there exists a countably infinite (`dual') valued structure Δ_μ which either primitively positively constructs 1-in-3-3-SAT, and hence the resilience problem for μ is NP-complete by general principles, or has a pseudo cyclic canonical fractional polymorphism, and the resilience problem for μ is in P.
Cite as

Manuel Bodirsky and Žaneta Semanišinová. The Complexity of Resilience for Digraph Queries. In 43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 364, pp. 15:1-15:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{bodirsky_et_al:LIPIcs.STACS.2026.15,
  author =	{Bodirsky, Manuel and Semani\v{s}inov\'{a}, \v{Z}aneta},
  title =	{{The Complexity of Resilience for Digraph Queries}},
  booktitle =	{43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026)},
  pages =	{15:1--15: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.15},
  URN =		{urn:nbn:de:0030-drops-255045},
  doi =		{10.4230/LIPIcs.STACS.2026.15},
  annote =	{Keywords: valued constraints, unions of conjunctive queries, resilience, computational complexity, pp-constructions}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2025.83
Three Fundamental Questions in Modern Infinite-Domain Constraint Satisfaction

Authors: Michael Pinsker, Jakub Rydval, Moritz Schöbi, and Christoph Spiess

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

Abstract
The Feder-Vardi dichotomy conjecture for Constraint Satisfaction Problems (CSPs) with finite templates, confirmed independently by Bulatov and Zhuk, has an extension to certain well-behaved infinite templates due to Bodirsky and Pinsker which remains wide open. We provide answers to three fundamental questions on the scope of the Bodirsky-Pinsker conjecture. Our first two main results provide two simplifications of this scope, one of structural, and the other one of algebraic nature. The former simplification implies that the conjecture is equivalent to its restriction to templates without algebraicity, a crucial assumption in the most powerful classification methods. The latter yields that the higher-arity invariants of any template within its scope can be assumed to be essentially injective, and any algebraic condition characterizing any complexity class within the conjecture closed under Datalog reductions must be satisfiable by injections, thus lifting the mystery of the better applicability of certain conditions over others. Our third main result uses the first one to show that any non-trivially tractable template within the scope serves, up to a Datalog-computable modification of it, as the witness of the tractability of a non-finitely tractable finite-domain Promise Constraint Satisfaction Problem (PCSP) by the so-called sandwich method. This generalizes a recent result of Mottet and provides a strong hitherto unknown connection between the Bodirsky-Pinsker conjecture and finite-domain PCSPs.
Cite as

Michael Pinsker, Jakub Rydval, Moritz Schöbi, and Christoph Spiess. Three Fundamental Questions in Modern Infinite-Domain Constraint Satisfaction. In 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 345, pp. 83:1-83:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{pinsker_et_al:LIPIcs.MFCS.2025.83,
  author =	{Pinsker, Michael and Rydval, Jakub and Sch\"{o}bi, Moritz and Spiess, Christoph},
  title =	{{Three Fundamental Questions in Modern Infinite-Domain Constraint Satisfaction}},
  booktitle =	{50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)},
  pages =	{83:1--83: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.83},
  URN =		{urn:nbn:de:0030-drops-241903},
  doi =		{10.4230/LIPIcs.MFCS.2025.83},
  annote =	{Keywords: (Promise) Constraint Satisfaction Problem, dichotomy conjecture, polymorphism, identity, algebraicity, homogeneity, \omega-categoricity, finite boundedness, Datalog}
}
Document
DOI: 10.4230/LIPIcs.ITP.2022.16
The Isabelle ENIGMA

Authors: Zarathustra A. Goertzel, Jan Jakubův, Cezary Kaliszyk, Miroslav Olšák, Jelle Piepenbrock, and Josef Urban

Published in: LIPIcs, Volume 237, 13th International Conference on Interactive Theorem Proving (ITP 2022)

Abstract
We significantly improve the performance of the E automated theorem prover on the Isabelle Sledgehammer problems by combining learning and theorem proving in several ways. In particular, we develop targeted versions of the ENIGMA guidance for the Isabelle problems, targeted versions of neural premise selection, and targeted strategies for E. The methods are trained in several iterations over hundreds of thousands untyped and typed first-order problems extracted from Isabelle. Our final best single-strategy ENIGMA and premise selection system improves the best previous version of E by 25.3% in 15 seconds, outperforming also all other previous ATP and SMT systems.
Cite as

Zarathustra A. Goertzel, Jan Jakubův, Cezary Kaliszyk, Miroslav Olšák, Jelle Piepenbrock, and Josef Urban. The Isabelle ENIGMA. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 16:1-16:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{goertzel_et_al:LIPIcs.ITP.2022.16,
  author =	{Goertzel, Zarathustra A. and Jakub\r{u}v, Jan and Kaliszyk, Cezary and Ol\v{s}\'{a}k, Miroslav and Piepenbrock, Jelle and Urban, Josef},
  title =	{{The Isabelle ENIGMA}},
  booktitle =	{13th International Conference on Interactive Theorem Proving (ITP 2022)},
  pages =	{16:1--16:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-252-5},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{237},
  editor =	{Andronick, June and de Moura, Leonardo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.16},
  URN =		{urn:nbn:de:0030-drops-167253},
  doi =		{10.4230/LIPIcs.ITP.2022.16},
  annote =	{Keywords: E Prover, ENIGMA, Premise Selection, Isabelle/Sledgehammer}
}
Document
Track A: Algorithms, Complexity and Games
DOI: 10.4230/LIPIcs.ICALP.2019.57
Dichotomy for Symmetric Boolean PCSPs

Authors: Miron Ficak, Marcin Kozik, Miroslav Olšák, and Szymon Stankiewicz

Published in: LIPIcs, Volume 132, 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019)

Abstract
In one of the most actively studied version of Constraint Satisfaction Problem, a CSP is defined by a relational structure called a template. In the decision version of the problem the goal is to determine whether a structure given on input admits a homomorphism into this template. Two recent independent results of Bulatov [FOCS'17] and Zhuk [FOCS'17] state that each finite template defines CSP which is tractable or NP-complete. In a recent paper Brakensiek and Guruswami [SODA'18] proposed an extension of the CSP framework. This extension, called Promise Constraint Satisfaction Problem, includes many naturally occurring computational questions, e.g. approximate coloring, that cannot be cast as CSPs. A PCSP is a combination of two CSPs defined by two similar templates; the computational question is to distinguish a YES instance of the first one from a NO instance of the second. The computational complexity of many PCSPs remains unknown. Even the case of Boolean templates (solved for CSP by Schaefer [STOC'78]) remains wide open. The main result of Brakensiek and Guruswami [SODA'18] shows that Boolean PCSPs exhibit a dichotomy (PTIME vs. NPC) when "all the clauses are symmetric and allow for negation of variables". In this paper we remove the "allow for negation of variables" assumption from the theorem. The "symmetric" assumption means that changing the order of variables in a constraint does not change its satisfiability. The "negation of variables" means that both of the templates share a relation which can be used to effectively negate Boolean variables. The main result of this paper establishes dichotomy for all the symmetric boolean templates. The tractability case of our theorem and the theorem of Brakensiek and Guruswami are almost identical. The main difference, and the main contribution of this work, is the new reason for hardness and the reasoning proving the split.
Cite as

Miron Ficak, Marcin Kozik, Miroslav Olšák, and Szymon Stankiewicz. Dichotomy for Symmetric Boolean PCSPs. In 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 132, pp. 57:1-57:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{ficak_et_al:LIPIcs.ICALP.2019.57,
  author =	{Ficak, Miron and Kozik, Marcin and Ol\v{s}\'{a}k, Miroslav and Stankiewicz, Szymon},
  title =	{{Dichotomy for Symmetric Boolean PCSPs}},
  booktitle =	{46th International Colloquium on Automata, Languages, and Programming (ICALP 2019)},
  pages =	{57:1--57:12},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-109-2},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{132},
  editor =	{Baier, Christel and Chatzigiannakis, Ioannis and Flocchini, Paola and Leonardi, Stefano},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2019.57},
  URN =		{urn:nbn:de:0030-drops-106339},
  doi =		{10.4230/LIPIcs.ICALP.2019.57},
  annote =	{Keywords: promise constraint satisfaction problem, PCSP, algebraic approach}
}
  • Refine by Type
  • 4 Document/PDF
  • 2 Document/HTML

  • Refine by Publication Year
  • 1 2026
  • 1 2025
  • 1 2022
  • 1 2019

  • Refine by Author
  • 2 Olšák, Miroslav
  • 1 Bodirsky, Manuel
  • 1 Ficak, Miron
  • 1 Goertzel, Zarathustra A.
  • 1 Jakubův, Jan
  • Show More...

  • Refine by Series/Journal
  • 4 LIPIcs

  • Refine by Classification
  • 2 Theory of computation → Complexity theory and logic
  • 1 Theory of computation → Automated reasoning
  • 1 Theory of computation → Computational complexity and cryptography
  • 1 Theory of computation → Constraint and logic programming
  • 1 Theory of computation → Database query processing and optimization (theory)
  • Show More...

  • Refine by Keyword
  • 1 (Promise) Constraint Satisfaction Problem
  • 1 Datalog
  • 1 E Prover
  • 1 ENIGMA
  • 1 Isabelle/Sledgehammer
  • 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