Search Results

Documents authored by Garlík, Michal

Document
DOI: 10.4230/LIPIcs.LICS.2026.49
Meta-Mathematics of Algebraic Complexity

Authors: Michal Garlík, Svyatolav Gryaznov, Jiaqi Lu, Rahul Santhanam, and Iddo Tzameret

Published in: LIPIcs, Volume 380, 41st Annual Symposium on Logic in Computer Science (LICS 2026)

Abstract
We initiate the study of the meta-mathematics of algebraic circuit lower bounds, aiming both to gain insight into the methods sufficient and necessary to prove algebraic circuit lower bounds, and to contribute to the study of bounded arithmetic as a logical foundation for complexity lower bounds. We demonstrate that while algebraic circuit lower bounds are hard for somewhat weak proof systems such as polynomial calculus resolution (PCR), contemporary lower bounds are efficiently provable in proof systems and bounded arithmetic theories corresponding to NC², such as VNC² and the corresponding class of propositional Frege proofs of quasipolynomial-size. Moreover, going below VNC² into algebraic constant-depth reasoning is likely insufficient to efficiently prove already constant-depth algebraic circuit lower bounds. Specifically, we show the following. - NC²-reasoning and rank method. Algebraic circuit lower bounds are often proved via the "rank method", with recent prominent applications including the constant-depth lower bounds of Limaye, Srinivasan and Tavenas [Limaye et al., 2025] and Forbes [Forbes, 2024]. We show that these rank-based arguments can be formalized in the bounded arithmetic theory VNC², which captures reasoning with NC² concepts. This complements the work of Tzameret and Cook [Tzameret and Cook, 2021], who formalized structural upper bounds in this theory, and provides a unified framework for studying barriers to current algebraic complexity methods, complementing barriers studied by Efremenko, Garg, Makam, Oliveira, and Wigderson [Klim Efremenko et al., 2018; Ankit Garg et al., 2019]. - Sparsity algebraic reasoning. We show that Polynomial Calculus Resolution (PCR) cannot efficiently prove superpolynomial algebraic circuit lower bounds for any family of polynomials. Moreover, PCR cannot efficiently prove exponential constant-depth circuit lower bounds for any family of polynomials. - Constant-depth algebraic reasoning. We introduce the Tensor Rank Principle and demonstrate it is hard for PCR. We show that if this principle is hard against constant-depth Ideal Proof System (IPS) then constant-depth IPS cannot efficiently prove constant-depth algebraic circuit lower bounds.
Cite as

Michal Garlík, Svyatolav Gryaznov, Jiaqi Lu, Rahul Santhanam, and Iddo Tzameret. Meta-Mathematics of Algebraic Complexity. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 49:1-49:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{garlik_et_al:LIPIcs.LICS.2026.49,
  author =	{Garl{\'\i}k, Michal and Gryaznov, Svyatolav and Lu, Jiaqi and Santhanam, Rahul and Tzameret, Iddo},
  title =	{{Meta-Mathematics of Algebraic Complexity}},
  booktitle =	{41st Annual Symposium on Logic in Computer Science (LICS 2026)},
  pages =	{49:1--49:25},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-434-5},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{380},
  editor =	{Faggian, Claudia 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.LICS.2026.49},
  URN =		{urn:nbn:de:0030-drops-268360},
  doi =		{10.4230/LIPIcs.LICS.2026.49},
  annote =	{Keywords: Complexity lower bounds, Bounded arithmetic, Feasible constructive mathematics, Algebraic complexity, Proof complexity, Meta-complexity, Algebraic circuit lower bounds, Polynomial Calculus Resolution, Barriers}
}
Document
DOI: 10.4230/LIPIcs.CCC.2024.33
Failure of Feasible Disjunction Property for k-DNF Resolution and NP-Hardness of Automating It

Authors: Michal Garlík

Published in: LIPIcs, Volume 300, 39th Computational Complexity Conference (CCC 2024)

Abstract
We show that for every integer k ≥ 2, the Res(k) propositional proof system does not have the weak feasible disjunction property. Next, we generalize a result of Atserias and Müller [Atserias and Müller, 2019] to Res(k). We show that if NP is not included in P (resp. QP, SUBEXP) then for every integer k ≥ 1, Res(k) is not automatable in polynomial (resp. quasi-polynomial, subexponential) time.
Cite as

Michal Garlík. Failure of Feasible Disjunction Property for k-DNF Resolution and NP-Hardness of Automating It. In 39th Computational Complexity Conference (CCC 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 300, pp. 33:1-33:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{garlik:LIPIcs.CCC.2024.33,
  author =	{Garl{\'\i}k, Michal},
  title =	{{Failure of Feasible Disjunction Property for k-DNF Resolution and NP-Hardness of Automating It}},
  booktitle =	{39th Computational Complexity Conference (CCC 2024)},
  pages =	{33:1--33:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-331-7},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{300},
  editor =	{Santhanam, Rahul},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2024.33},
  URN =		{urn:nbn:de:0030-drops-204295},
  doi =		{10.4230/LIPIcs.CCC.2024.33},
  annote =	{Keywords: reflection principle, feasible disjunction property, k-DNF Resolution}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2019.37
Resolution Lower Bounds for Refutation Statements

Authors: Michal Garlík

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

Abstract
For any unsatisfiable CNF formula we give an exponential lower bound on the size of resolution refutations of a propositional statement that the formula has a resolution refutation. We describe three applications. (1) An open question in [Atserias and Müller, 2019] asks whether a certain natural propositional encoding of the above statement is hard for Resolution. We answer by giving an exponential size lower bound. (2) We show exponential resolution size lower bounds for reflection principles, thereby improving a result in [Albert Atserias and María Luisa Bonet, 2004]. (3) We provide new examples of CNFs that exponentially separate Res(2) from Resolution (an exponential separation of these two proof systems was originally proved in [Nathan Segerlind et al., 2004]).
Cite as

Michal Garlík. Resolution Lower Bounds for Refutation Statements. In 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 138, pp. 37:1-37:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{garlik:LIPIcs.MFCS.2019.37,
  author =	{Garl{\'\i}k, Michal},
  title =	{{Resolution Lower Bounds for Refutation Statements}},
  booktitle =	{44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)},
  pages =	{37:1--37:13},
  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.37},
  URN =		{urn:nbn:de:0030-drops-109817},
  doi =		{10.4230/LIPIcs.MFCS.2019.37},
  annote =	{Keywords: reflection principles, refutation statements, Resolution, proof complexity}
}
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