4 Search Results for "Papamakarios, Theodoros"

Document
DOI: 10.4230/LIPIcs.CCC.2025.14
On the Automatability of Tree-Like k-DNF Resolution

Authors: Gaia Carenini and Susanna F. de Rezende

Published in: LIPIcs, Volume 339, 40th Computational Complexity Conference (CCC 2025)

Abstract
A proof system 𝒫 is said to be automatable in time f(N) if there exists an algorithm that given as input an unsatisfiable formula F outputs a refutation of F in the proof system 𝒫 in time f(N), where N is the size of the smallest 𝒫-refutation of F plus the size of F. Atserias and Bonet (ECCC 2002), observed that tree-like k-DNF resolution is automatable in time N^{c⋅klog N} for a universal constant c. We show that, under the randomized exponential-time hypothesis (rETH), this is tight up to a O(log k)-factor in the exponent, i.e., we prove that tree-like k-DNF resolution, for k at most logarithmic in the number of variables of F, is not automatable in time N^o((k/log k)⋅log N) unless rETH is false. Our proof builds on the non-automatability results for resolution by Atserias and Müller (FOCS 2019), for algebraic proof systems by de Rezende, Göös, Nordström, Pitassi, Robere and Sokolov (STOC 2021), and for tree-like resolution by de Rezende (LAGOS 2021).
Cite as

Gaia Carenini and Susanna F. de Rezende. On the Automatability of Tree-Like k-DNF Resolution. In 40th Computational Complexity Conference (CCC 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 339, pp. 14:1-14:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{carenini_et_al:LIPIcs.CCC.2025.14,
  author =	{Carenini, Gaia and de Rezende, Susanna F.},
  title =	{{On the Automatability of Tree-Like k-DNF Resolution}},
  booktitle =	{40th Computational Complexity Conference (CCC 2025)},
  pages =	{14:1--14:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-379-9},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{339},
  editor =	{Srinivasan, Srikanth},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2025.14},
  URN =		{urn:nbn:de:0030-drops-237081},
  doi =		{10.4230/LIPIcs.CCC.2025.14},
  annote =	{Keywords: Proof Complexity, Tree-like k-DNF Resolution, Automatability}
}
Document
DOI: 10.4230/LIPIcs.CCC.2024.22
Depth-d Frege Systems Are Not Automatable Unless 𝖯 = NP

Authors: Theodoros Papamakarios

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

Abstract
We show that for any integer d > 0, depth-d Frege systems are NP-hard to automate. Namely, given a set S of depth-d formulas, it is NP-hard to find a depth-d Frege refutation of S in time polynomial in the size of the shortest such refutation. This extends the result of Atserias and Müller [JACM, 2020] for the non-automatability of resolution - a depth-1 Frege system - to Frege systems of any depth d > 0.
Cite as

Theodoros Papamakarios. Depth-d Frege Systems Are Not Automatable Unless 𝖯 = NP. In 39th Computational Complexity Conference (CCC 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 300, pp. 22:1-22:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{papamakarios:LIPIcs.CCC.2024.22,
  author =	{Papamakarios, Theodoros},
  title =	{{Depth-d Frege Systems Are Not Automatable Unless 𝖯 = NP}},
  booktitle =	{39th Computational Complexity Conference (CCC 2024)},
  pages =	{22:1--22:17},
  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.22},
  URN =		{urn:nbn:de:0030-drops-204187},
  doi =		{10.4230/LIPIcs.CCC.2024.22},
  annote =	{Keywords: Proof complexity, Automatability, Bounded-depth Frege}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2023.74
A Super-Polynomial Separation Between Resolution and Cut-Free Sequent Calculus

Authors: Theodoros Papamakarios

Published in: LIPIcs, Volume 272, 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023)

Abstract
We show a quadratic separation between resolution and cut-free sequent calculus width. We use this gap to get, for the first time, first, a super-polynomial separation between resolution and cut-free sequent calculus for refuting CNF formulas, and secondly, a quadratic separation between resolution width and monomial space in polynomial calculus with resolution. Our super-polynomial separation between resolution and cut-free sequent calculus only applies when clauses are seen as disjunctions of unbounded arity; our examples have linear size cut-free sequent calculus proofs writing, in a particular way, their clauses using binary disjunctions. Interestingly, this shows that the complexity of sequent calculus depends on how disjunctions are represented.
Cite as

Theodoros Papamakarios. A Super-Polynomial Separation Between Resolution and Cut-Free Sequent Calculus. In 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 272, pp. 74:1-74:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{papamakarios:LIPIcs.MFCS.2023.74,
  author =	{Papamakarios, Theodoros},
  title =	{{A Super-Polynomial Separation Between Resolution and Cut-Free Sequent Calculus}},
  booktitle =	{48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023)},
  pages =	{74:1--74:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-292-1},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{272},
  editor =	{Leroux, J\'{e}r\^{o}me and Lombardy, Sylvain and Peleg, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2023.74},
  URN =		{urn:nbn:de:0030-drops-186085},
  doi =		{10.4230/LIPIcs.MFCS.2023.74},
  annote =	{Keywords: Proof Complexity, Resolution, Cut-free LK}
}
Document
Track A: Algorithms, Complexity and Games
DOI: 10.4230/LIPIcs.ICALP.2022.100
Space Characterizations of Complexity Measures and Size-Space Trade-Offs in Propositional Proof Systems

Authors: Theodoros Papamakarios and Alexander Razborov

Published in: LIPIcs, Volume 229, 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022)

Abstract
We identify two new big clusters of proof complexity measures equivalent up to polynomial and log n factors. The first cluster contains, among others, the logarithm of tree-like resolution size, regularized (that is, multiplied by the logarithm of proof length) clause and monomial space, and clause space, both ordinary and regularized, in regular and tree-like resolution. As a consequence, separating clause or monomial space from the (logarithm of) tree-like resolution size is the same as showing a strong trade-off between clause or monomial space and proof length, and is the same as showing a super-critical trade-off between clause space and depth. The second cluster contains width, Σ₂ space (a generalization of clause space to depth 2 Frege systems), both ordinary and regularized, as well as the logarithm of tree-like size in the system R(log). As an application of some of these simulations, we improve a known size-space trade-off for polynomial calculus with resolution. In terms of lower bounds, we show a quadratic lower bound on tree-like resolution size for formulas refutable in clause space 4. We introduce on our way yet another proof complexity measure intermediate between depth and the logarithm of tree-like size that might be of independent interest.
Cite as

Theodoros Papamakarios and Alexander Razborov. Space Characterizations of Complexity Measures and Size-Space Trade-Offs in Propositional Proof Systems. In 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 229, pp. 100:1-100:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{papamakarios_et_al:LIPIcs.ICALP.2022.100,
  author =	{Papamakarios, Theodoros and Razborov, Alexander},
  title =	{{Space Characterizations of Complexity Measures and Size-Space Trade-Offs in Propositional Proof Systems}},
  booktitle =	{49th International Colloquium on Automata, Languages, and Programming (ICALP 2022)},
  pages =	{100:1--100:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-235-8},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{229},
  editor =	{Boja\'{n}czyk, Miko{\l}aj and Merelli, Emanuela and Woodruff, David P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2022.100},
  URN =		{urn:nbn:de:0030-drops-164419},
  doi =		{10.4230/LIPIcs.ICALP.2022.100},
  annote =	{Keywords: Proof Complexity, Resolution, Size-Space Trade-offs}
}
  • Refine by Type
  • 4 Document/PDF
  • 1 Document/HTML

  • Refine by Publication Year
  • 1 2025
  • 1 2024
  • 1 2023
  • 1 2022

  • Refine by Author
  • 3 Papamakarios, Theodoros
  • 1 Carenini, Gaia
  • 1 Razborov, Alexander
  • 1 de Rezende, Susanna F.

  • Refine by Series/Journal
  • 4 LIPIcs

  • Refine by Classification
  • 3 Theory of computation → Proof complexity
  • 1 Theory of computation

  • Refine by Keyword
  • 3 Proof Complexity
  • 2 Automatability
  • 2 Resolution
  • 1 Bounded-depth Frege
  • 1 Cut-free LK
  • 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