15 Search Results for "Galesi, Nicola"

Document
DOI: 10.4230/LIPIcs.ITCS.2026.8
Intersection Theorems: A Potential Approach to Proof Complexity Lower Bounds

Authors: Yaroslav Alekseev and Nikita Gaevoy

Published in: LIPIcs, Volume 362, 17th Innovations in Theoretical Computer Science Conference (ITCS 2026)

Abstract
Recently, Göös et al. [Göös et al., 2024] showed that Res ⋏ uSA = RevRes in the following sense: if a formula φ has refutations of size at most s and width/degree at most w in both Res and uSA, then there is a refutation for φ of size at most poly(s ⋅ 2^w) in RevRes. Their proof relies on the TFNP characterization of the aforementioned proof systems. In our work, we give a direct and simplified proof of this result, simultaneously achieving better bounds: we show that if for a formula φ there are refutations of size at most s in both Res and uSA, then there is a refutation of φ of size at most poly(s) in RevRes. This potentially allows us to "lift" size lower bounds from RevRes to Res for the formulas for which there are upper bounds in uSA. This kind of lifting was not possible before because of the exponential blow-up in size from the width. Similarly, we improve the bounds in another intersection theorem from [Göös et al., 2024] by giving a direct proof of Res ⋏ uNS = RevResT. Finally, we generalize those intersection theorems to some proof systems for which we currently do not have a TFNP characterization. For example, we show that Res(⊕) ⋏ u-wRes(⊕) = RevRes(⊕), which effectively allows us to reduce the problem of proving Pigeonhole Principle lower bounds in Res(⊕) to proving Pigeonhole Principle lower bounds in RevRes(⊕), a potentially weaker proof system.
Cite as

Yaroslav Alekseev and Nikita Gaevoy. Intersection Theorems: A Potential Approach to Proof Complexity Lower Bounds. In 17th Innovations in Theoretical Computer Science Conference (ITCS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 362, pp. 8:1-8:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{alekseev_et_al:LIPIcs.ITCS.2026.8,
  author =	{Alekseev, Yaroslav and Gaevoy, Nikita},
  title =	{{Intersection Theorems: A Potential Approach to Proof Complexity Lower Bounds}},
  booktitle =	{17th Innovations in Theoretical Computer Science Conference (ITCS 2026)},
  pages =	{8:1--8:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-410-9},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{362},
  editor =	{Saraf, Shubhangi},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITCS.2026.8},
  URN =		{urn:nbn:de:0030-drops-252953},
  doi =		{10.4230/LIPIcs.ITCS.2026.8},
  annote =	{Keywords: proof complexity, intersection theorems}
}
Document
DOI: 10.4230/LIPIcs.ITCS.2026.60
Total Search Problems in ZPP

Authors: Noah Fleming, Stefan Grosser, Siddhartha Jain, Jiawei Li, Hanlin Ren, Morgan Shirley, and Weiqiang Yuan

Published in: LIPIcs, Volume 362, 17th Innovations in Theoretical Computer Science Conference (ITCS 2026)

Abstract
We initiate a systematic study of TFZPP, the class of total NP search problems solvable by polynomial time randomized algorithms. TFZPP contains a variety of important search problems such as Bertrand-Chebyshev (finding a prime between N and 2N), refuter problems for many circuit lower bounds, and Lossy-Code. The Lossy-Code problem has found prominence due to its fundamental connections to derandomization, catalytic computing, and the metamathematics of complexity theory, among other areas. While TFZPP collapses to FP under standard derandomization assumptions in the white-box setting, we are able to separate TFZPP from the major TFNP subclasses in the black-box setting. In fact, we are able to separate it from every uniform TFNP class assuming that NP is not in quasi-polynomial time. To do so, we extend the connection between proof complexity and black-box TFNP to randomized proof systems and randomized reductions. Next, we turn to developing a taxonomy of TFZPP problems. We highlight a problem called Nephew, originating from an infinity axiom in set theory. We show that Nephew is in PWPP∩ TFZPP and conjecture that it is not reducible to Lossy-Code. Intriguingly, except for some artificial examples, most other black-box TFZPP problems that we are aware of reduce to Lossy-Code: - We define a problem called Empty-Child capturing finding a leaf in a rooted (binary) tree, and show that this problem is equivalent to Lossy-Code. We also show that a variant of Empty-Child with "heights" is complete for the intersection of SOPL and Lossy-Code. - We strengthen Lossy-Code with several combinatorial inequalities such as the AM-GM inequality. Somewhat surprisingly, we show the resulting new problems are still reducible to Lossy-Code. A technical highlight of this result is that they are proved by formalizations in bounded arithmetic, specifically in Jeřábek’s theory APC₁ (JSL 2007). - Finally, we show that the Dense-Linear-Ordering problem reduces to Lossy-Code.
Cite as

Noah Fleming, Stefan Grosser, Siddhartha Jain, Jiawei Li, Hanlin Ren, Morgan Shirley, and Weiqiang Yuan. Total Search Problems in ZPP. In 17th Innovations in Theoretical Computer Science Conference (ITCS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 362, pp. 60:1-60:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{fleming_et_al:LIPIcs.ITCS.2026.60,
  author =	{Fleming, Noah and Grosser, Stefan and Jain, Siddhartha and Li, Jiawei and Ren, Hanlin and Shirley, Morgan and Yuan, Weiqiang},
  title =	{{Total Search Problems in ZPP}},
  booktitle =	{17th Innovations in Theoretical Computer Science Conference (ITCS 2026)},
  pages =	{60:1--60:26},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-410-9},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{362},
  editor =	{Saraf, Shubhangi},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITCS.2026.60},
  URN =		{urn:nbn:de:0030-drops-253473},
  doi =		{10.4230/LIPIcs.ITCS.2026.60},
  annote =	{Keywords: TFNP, lossy code, randomized proof systems, query complexity}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2025.18
Supercritical Size-Width Tree-Like Resolution Trade-Offs for Graph Isomorphism

Authors: Christoph Berkholz, Moritz Lichter, and Harry Vinall-Smeeth

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

Abstract
We study the refutation complexity of graph isomorphism in the tree-like resolution calculus. Torán and Wörz [Jacobo Torán and Florian Wörz, 2023] showed that there is a resolution refutation of narrow width k for two graphs if and only if they can be distinguished in (k+1)-variable first-order logic (FO^{k+1}). While DAG-like narrow width k resolution refutations have size at most n^k, tree-like refutations may be much larger. We show that there are graphs of order n, whose isomorphism can be refuted in narrow width k but only in tree-like size 2^{Ω(n^{k/2})}. This is a supercritical trade-off where bounding one parameter (the narrow width) causes the other parameter (the size) to grow above its worst case. The size lower bound is super-exponential in the formula size and improves a related supercritical trade-off by Razborov [Alexander A. Razborov, 2016]. To prove our result, we develop a new variant of the k-pebble EF-game for FO^k to reason about tree-like refutation size in a similar way as the Prover-Delayer games in proof complexity. We analyze this game on the compressed CFI graphs introduced by Grohe, Lichter, Neuen, and Schweitzer [Martin Grohe et al., 2023]. Using a recent improved robust compressed CFI construction of de Rezende, Fleming, Janett, Nordström, and Pang [Susanna F. de Rezende et al., 2024], we obtain a similar bound for width k (instead of the stronger but less common narrow width) and make the result more robust.
Cite as

Christoph Berkholz, Moritz Lichter, and Harry Vinall-Smeeth. Supercritical Size-Width Tree-Like Resolution Trade-Offs for Graph Isomorphism. In 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 345, pp. 18:1-18:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{berkholz_et_al:LIPIcs.MFCS.2025.18,
  author =	{Berkholz, Christoph and Lichter, Moritz and Vinall-Smeeth, Harry},
  title =	{{Supercritical Size-Width Tree-Like Resolution Trade-Offs for Graph Isomorphism}},
  booktitle =	{50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)},
  pages =	{18:1--18:19},
  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.18},
  URN =		{urn:nbn:de:0030-drops-241253},
  doi =		{10.4230/LIPIcs.MFCS.2025.18},
  annote =	{Keywords: Proof complexity, Resolution, Width, Tree-like size, Supercritical trade-off, Lower bound, Finite model theory, CFI graphs}
}
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.2025.36
Lifting with Colourful Sunflowers

Authors: Susanna F. de Rezende and Marc Vinyals

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

Abstract
We show that a generalization of the DAG-like query-to-communication lifting theorem, when proven using sunflowers over non-binary alphabets, yields lower bounds on the monotone circuit complexity and proof complexity of natural functions and formulas that are better than previously known results obtained using the approximation method. These include an n^Ω(k) lower bound for the clique function up to k ≤ n^{1/2-ε}, and an exp(Ω(n^{1/3-ε})) lower bound for a function in P.
Cite as

Susanna F. de Rezende and Marc Vinyals. Lifting with Colourful Sunflowers. In 40th Computational Complexity Conference (CCC 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 339, pp. 36:1-36:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{derezende_et_al:LIPIcs.CCC.2025.36,
  author =	{de Rezende, Susanna F. and Vinyals, Marc},
  title =	{{Lifting with Colourful Sunflowers}},
  booktitle =	{40th Computational Complexity Conference (CCC 2025)},
  pages =	{36:1--36:19},
  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.36},
  URN =		{urn:nbn:de:0030-drops-237303},
  doi =		{10.4230/LIPIcs.CCC.2025.36},
  annote =	{Keywords: lifting, sunflower, clique, colouring, monotone circuit, cutting planes}
}
Document
Track A: Algorithms, Complexity and Games
DOI: 10.4230/LIPIcs.ICALP.2025.21
Multiparty Communication Complexity of Collision-Finding and Cutting Planes Proofs of Concise Pigeonhole Principles

Authors: Paul Beame and Michael Whitmeyer

Published in: LIPIcs, Volume 334, 52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025)

Abstract
We prove several results concerning the communication complexity of a collision-finding problem, each of which has applications to the complexity of cutting-plane proofs, which make inferences based on integer linear inequalities. In particular, we prove an Ω(n^{1-1/k} log k /2^k) lower bound on the k-party number-in-hand communication complexity of collision-finding. This implies a 2^{n^{1-o(1)}} lower bound on the size of tree-like cutting-planes refutations of the bit pigeonhole principle CNFs, which are compact and natural propositional encodings of the negation of the pigeonhole principle, improving on the best previous lower bound of 2^{Ω(√n)}. Using the method of density-restoring partitions, we also extend that previous lower bound to the full range of pigeonhole parameters. Finally, using a refinement of a bottleneck-counting framework of Haken and Cook and Sokolov for DAG-like communication protocols, we give a 2^{Ω(n^{1/4})} lower bound on the size of fully general (not necessarily tree-like) cutting planes refutations of the same bit pigeonhole principle formulas, improving on the best previous lower bound of 2^{Ω(n^{1/8})}.
Cite as

Paul Beame and Michael Whitmeyer. Multiparty Communication Complexity of Collision-Finding and Cutting Planes Proofs of Concise Pigeonhole Principles. In 52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 334, pp. 21:1-21:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{beame_et_al:LIPIcs.ICALP.2025.21,
  author =	{Beame, Paul and Whitmeyer, Michael},
  title =	{{Multiparty Communication Complexity of Collision-Finding and Cutting Planes Proofs of Concise Pigeonhole Principles}},
  booktitle =	{52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025)},
  pages =	{21:1--21:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-372-0},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{334},
  editor =	{Censor-Hillel, Keren and Grandoni, Fabrizio and Ouaknine, Jo\"{e}l and Puppis, Gabriele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2025.21},
  URN =		{urn:nbn:de:0030-drops-233982},
  doi =		{10.4230/LIPIcs.ICALP.2025.21},
  annote =	{Keywords: Proof Complexity, Communication Complexity}
}
Document
DOI: 10.4230/LIPIcs.CSL.2025.6
Equi-Rank Homomorphism Preservation Theorem on Finite Structures

Authors: Benjamin Rossman

Published in: LIPIcs, Volume 326, 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)

Abstract
The Homomorphism Preservation Theorem (HPT) of classical model theory states that a first-order sentence is preserved under homomorphisms if, and only if, it is equivalent to an existential-positive sentence. This theorem remains valid when restricted to finite structures, as demonstrated by the author in [Rossman, 2008; Rossman, 2017] via distinct model-theoretic and circuit-complexity based proofs. In this paper, we present a third (and significantly simpler) proof of the finitary HPT based on a generalized Cai-Fürer-Immerman construction. This method establishes a tight correspondence between syntactic parameters of a homomorphism-preserved sentence (quantifier rank, variable width, alternation height) and structural parameters of its minimal models (tree-width, tree-depth, decomposition height). Consequently, we prove a conjectured "equi-rank" version of the finitary HPT. In contrast, previous versions of the finitary HPT possess additional properties, but incur blow-ups in the quantifier rank of the equivalent existential-positive sentence.
Cite as

Benjamin Rossman. Equi-Rank Homomorphism Preservation Theorem on Finite Structures. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 6:1-6:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{rossman:LIPIcs.CSL.2025.6,
  author =	{Rossman, Benjamin},
  title =	{{Equi-Rank Homomorphism Preservation Theorem on Finite Structures}},
  booktitle =	{33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
  pages =	{6:1--6:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-362-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{326},
  editor =	{Endrullis, J\"{o}rg and Schmitz, Sylvain},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2025.6},
  URN =		{urn:nbn:de:0030-drops-227634},
  doi =		{10.4230/LIPIcs.CSL.2025.6},
  annote =	{Keywords: finite model theory, preservation theorems, quantifier rank}
}
Document
DOI: 10.4230/LIPIcs.CCC.2023.4
On the Algebraic Proof Complexity of Tensor Isomorphism

Authors: Nicola Galesi, Joshua A. Grochow, Toniann Pitassi, and Adrian She

Published in: LIPIcs, Volume 264, 38th Computational Complexity Conference (CCC 2023)

Abstract
The Tensor Isomorphism problem (TI) has recently emerged as having connections to multiple areas of research within complexity and beyond, but the current best upper bound is essentially the brute force algorithm. Being an algebraic problem, TI (or rather, proving that two tensors are non-isomorphic) lends itself very naturally to algebraic and semi-algebraic proof systems, such as the Polynomial Calculus (PC) and Sum of Squares (SoS). For its combinatorial cousin Graph Isomorphism, essentially optimal lower bounds are known for approaches based on PC and SoS (Berkholz & Grohe, SODA '17). Our main results are an Ω(n) lower bound on PC degree or SoS degree for Tensor Isomorphism, and a nontrivial upper bound for testing isomorphism of tensors of bounded rank. We also show that PC cannot perform basic linear algebra in sub-linear degree, such as comparing the rank of two matrices (which is essentially the same as 2-TI), or deriving BA = I from AB = I. As linear algebra is a key tool for understanding tensors, we introduce a strictly stronger proof system, PC+Inv, which allows as derivation rules all substitution instances of the implication AB = I → BA = I. We conjecture that even PC+Inv cannot solve TI in polynomial time either, but leave open getting lower bounds on PC+Inv for any system of equations, let alone those for TI. We also highlight many other open questions about proof complexity approaches to TI.
Cite as

Nicola Galesi, Joshua A. Grochow, Toniann Pitassi, and Adrian She. On the Algebraic Proof Complexity of Tensor Isomorphism. In 38th Computational Complexity Conference (CCC 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 264, pp. 4:1-4:40, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{galesi_et_al:LIPIcs.CCC.2023.4,
  author =	{Galesi, Nicola and Grochow, Joshua A. and Pitassi, Toniann and She, Adrian},
  title =	{{On the Algebraic Proof Complexity of Tensor Isomorphism}},
  booktitle =	{38th Computational Complexity Conference (CCC 2023)},
  pages =	{4:1--4:40},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-282-2},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{264},
  editor =	{Ta-Shma, Amnon},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2023.4},
  URN =		{urn:nbn:de:0030-drops-182748},
  doi =		{10.4230/LIPIcs.CCC.2023.4},
  annote =	{Keywords: Algebraic proof complexity, Tensor Isomorphism, Graph Isomorphism, Polynomial Calculus, Sum-of-Squares, reductions, lower bounds, proof complexity of linear algebra}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2022.23
On Vanishing Sums of Roots of Unity in Polynomial Calculus and Sum-Of-Squares

Authors: Ilario Bonacina, Nicola Galesi, and Massimo Lauria

Published in: LIPIcs, Volume 241, 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)

Abstract
Vanishing sums of roots of unity can be seen as a natural generalization of knapsack from Boolean variables to variables taking values over the roots of unity. We show that these sums are hard to prove for polynomial calculus and for sum-of-squares, both in terms of degree and size.
Cite as

Ilario Bonacina, Nicola Galesi, and Massimo Lauria. On Vanishing Sums of Roots of Unity in Polynomial Calculus and Sum-Of-Squares. In 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 241, pp. 23:1-23:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{bonacina_et_al:LIPIcs.MFCS.2022.23,
  author =	{Bonacina, Ilario and Galesi, Nicola and Lauria, Massimo},
  title =	{{On Vanishing Sums of Roots of Unity in Polynomial Calculus and Sum-Of-Squares}},
  booktitle =	{47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)},
  pages =	{23:1--23:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-256-3},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{241},
  editor =	{Szeider, Stefan and Ganian, Robert and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2022.23},
  URN =		{urn:nbn:de:0030-drops-168211},
  doi =		{10.4230/LIPIcs.MFCS.2022.23},
  annote =	{Keywords: polynomial calculus, sum-of-squares, roots of unity, knapsack}
}
Document
DOI: 10.4230/LIPIcs.STACS.2022.24
Depth Lower Bounds in Stabbing Planes for Combinatorial Principles

Authors: Stefan Dantchev, Nicola Galesi, Abdul Ghani, and Barnaby Martin

Published in: LIPIcs, Volume 219, 39th International Symposium on Theoretical Aspects of Computer Science (STACS 2022)

Abstract
Stabbing Planes is a proof system introduced very recently which, informally speaking, extends the DPLL method by branching on integer linear inequalities instead of single variables. The techniques known so far to prove size and depth lower bounds for Stabbing Planes are generalizations of those used for the Cutting Planes proof system established via communication complexity arguments. Rank lower bounds for Cutting Planes are also obtained by geometric arguments called protection lemmas. In this work we introduce two new geometric approaches to prove size/depth lower bounds in Stabbing Planes working for any formula: (1) the antichain method, relying on Sperner’s Theorem and (2) the covering method which uses results on essential coverings of the boolean cube by linear polynomials, which in turn relies on Alon’s combinatorial Nullenstellensatz. We demonstrate their use on classes of combinatorial principles such as the Pigeonhole principle, the Tseitin contradictions and the Linear Ordering Principle. By the first method we prove almost linear size lower bounds and optimal logarithmic depth lower bounds for the Pigeonhole principle and analogous lower bounds for the Tseitin contradictions over the complete graph and for the Linear Ordering Principle. By the covering method we obtain a superlinear size lower bound and a logarithmic depth lower bound for Stabbing Planes proof of Tseitin contradictions over a grid graph.
Cite as

Stefan Dantchev, Nicola Galesi, Abdul Ghani, and Barnaby Martin. Depth Lower Bounds in Stabbing Planes for Combinatorial Principles. In 39th International Symposium on Theoretical Aspects of Computer Science (STACS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 219, pp. 24:1-24:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{dantchev_et_al:LIPIcs.STACS.2022.24,
  author =	{Dantchev, Stefan and Galesi, Nicola and Ghani, Abdul and Martin, Barnaby},
  title =	{{Depth Lower Bounds in Stabbing Planes for Combinatorial Principles}},
  booktitle =	{39th International Symposium on Theoretical Aspects of Computer Science (STACS 2022)},
  pages =	{24:1--24:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-222-8},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{219},
  editor =	{Berenbrink, Petra and Monmege, Benjamin},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2022.24},
  URN =		{urn:nbn:de:0030-drops-158349},
  doi =		{10.4230/LIPIcs.STACS.2022.24},
  annote =	{Keywords: proof complexity, computational complexity, lower bounds, cutting planes, stabbing planes}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2019.49
Bounded-Depth Frege Complexity of Tseitin Formulas for All Graphs

Authors: Nicola Galesi, Dmitry Itsykson, Artur Riazanov, and Anastasia Sofronova

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

Abstract
We prove that there is a constant K such that Tseitin formulas for an undirected graph G requires proofs of size 2^{tw(G)^{Omega(1/d)}} in depth-d Frege systems for d<(K log n)/(log log n), where tw(G) is the treewidth of G. This extends Håstad recent lower bound for the grid graph to any graph. Furthermore, we prove tightness of our bound up to a multiplicative constant in the top exponent. Namely, we show that if a Tseitin formula for a graph G has size s, then for all large enough d, it has a depth-d Frege proof of size 2^{tw(G)^{O(1/d)}} poly(s). Through this result we settle the question posed by M. Alekhnovich and A. Razborov of showing that the class of Tseitin formulas is quasi-automatizable for resolution.
Cite as

Nicola Galesi, Dmitry Itsykson, Artur Riazanov, and Anastasia Sofronova. Bounded-Depth Frege Complexity of Tseitin Formulas for All Graphs. In 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 138, pp. 49:1-49:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{galesi_et_al:LIPIcs.MFCS.2019.49,
  author =	{Galesi, Nicola and Itsykson, Dmitry and Riazanov, Artur and Sofronova, Anastasia},
  title =	{{Bounded-Depth Frege Complexity of Tseitin Formulas for All Graphs}},
  booktitle =	{44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)},
  pages =	{49:1--49:15},
  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.49},
  URN =		{urn:nbn:de:0030-drops-109932},
  doi =		{10.4230/LIPIcs.MFCS.2019.49},
  annote =	{Keywords: Tseitin formula, treewidth, AC0-Frege}
}
Document
DOI: 10.4230/LIPIcs.CCC.2019.6
Resolution and the Binary Encoding of Combinatorial Principles

Authors: Stefan Dantchev, Nicola Galesi, and Barnaby Martin

Published in: LIPIcs, Volume 137, 34th Computational Complexity Conference (CCC 2019)

Abstract
Res(s) is an extension of Resolution working on s-DNFs. We prove tight n^{Omega(k)} lower bounds for the size of refutations of the binary version of the k-Clique Principle in Res(o(log log n)). Our result improves that of Lauria, Pudlák et al. [Massimo Lauria et al., 2017] who proved the lower bound for Res(1), i.e. Resolution. The exact complexity of the (unary) k-Clique Principle in Resolution is unknown. To prove the lower bound we do not use any form of the Switching Lemma [Nathan Segerlind et al., 2004], instead we apply a recursive argument specific for binary encodings. Since for the k-Clique and other principles lower bounds in Resolution for the unary version follow from lower bounds in Res(log n) for their binary version we start a systematic study of the complexity of proofs in Resolution-based systems for families of contradictions given in the binary encoding. We go on to consider the binary version of the weak Pigeonhole Principle Bin-PHP^m_n for m>n. Using the the same recursive approach we prove the new result that for any delta>0, Bin-PHP^m_n requires proofs of size 2^{n^{1-delta}} in Res(s) for s=o(log^{1/2}n). Our lower bound is almost optimal since for m >= 2^{sqrt{n log n}} there are quasipolynomial size proofs of Bin-PHP^m_n in Res(log n). Finally we propose a general theory in which to compare the complexity of refuting the binary and unary versions of large classes of combinatorial principles, namely those expressible as first order formulae in Pi_2-form and with no finite model.
Cite as

Stefan Dantchev, Nicola Galesi, and Barnaby Martin. Resolution and the Binary Encoding of Combinatorial Principles. In 34th Computational Complexity Conference (CCC 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 137, pp. 6:1-6:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{dantchev_et_al:LIPIcs.CCC.2019.6,
  author =	{Dantchev, Stefan and Galesi, Nicola and Martin, Barnaby},
  title =	{{Resolution and the Binary Encoding of Combinatorial Principles}},
  booktitle =	{34th Computational Complexity Conference (CCC 2019)},
  pages =	{6:1--6:25},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-116-0},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{137},
  editor =	{Shpilka, Amir},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2019.6},
  URN =		{urn:nbn:de:0030-drops-108287},
  doi =		{10.4230/LIPIcs.CCC.2019.6},
  annote =	{Keywords: Proof complexity, k-DNF resolution, binary encodings, Clique and Pigeonhole principle}
}
Document
DOI: 10.4230/LIPIcs.CCC.2015.433
The Space Complexity of Cutting Planes Refutations

Authors: Nicola Galesi, Pavel Pudlák, and Neil Thapen

Published in: LIPIcs, Volume 33, 30th Conference on Computational Complexity (CCC 2015)

Abstract
We study the space complexity of the cutting planes proof system, in which the lines in a proof are integral linear inequalities. We measure the space used by a refutation as the number of linear inequalities that need to be kept on a blackboard while verifying it. We show that any unsatisfiable set of linear inequalities has a cutting planes refutation in space five. This is in contrast to the weaker resolution proof system, for which the analogous space measure has been well-studied and many optimal linear lower bounds are known. Motivated by this result we consider a natural restriction of cutting planes, in which all coefficients have size bounded by a constant. We show that there is a CNF which requires super-constant space to refute in this system. The system nevertheless already has an exponential speed-up over resolution with respect to size, and we additionally show that it is stronger than resolution with respect to space, by constructing constant-space cutting planes proofs, with coefficients bounded by two, of the pigeonhole principle. We also consider variable instance space for cutting planes, where we count the number of instances of variables on the blackboard, and total space, where we count the total number of symbols.
Cite as

Nicola Galesi, Pavel Pudlák, and Neil Thapen. The Space Complexity of Cutting Planes Refutations. In 30th Conference on Computational Complexity (CCC 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 33, pp. 433-447, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{galesi_et_al:LIPIcs.CCC.2015.433,
  author =	{Galesi, Nicola and Pudl\'{a}k, Pavel and Thapen, Neil},
  title =	{{The Space Complexity of Cutting Planes Refutations}},
  booktitle =	{30th Conference on Computational Complexity (CCC 2015)},
  pages =	{433--447},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-81-1},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{33},
  editor =	{Zuckerman, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2015.433},
  URN =		{urn:nbn:de:0030-drops-50551},
  doi =		{10.4230/LIPIcs.CCC.2015.433},
  annote =	{Keywords: Proof Complexity, Cutting Planes, Space Complexity}
}
Document
DOI: 10.4230/DagRep.2.11.87
SAT Interactions (Dagstuhl Seminar 12471)

Authors: Nadia Creignou, Nicola Galesi, Oliver Kullmann, and Heribert Vollmer

Published in: Dagstuhl Reports, Volume 2, Issue 11 (2013)

Abstract
This report documents the programme and outcomes of Dagstuhl Seminar 12471 "SAT Interactions". The seminar brought together researchers from different areas from theoretical computer science as well as the area of SAT solvers. A key objective of the seminar has been to initiate or consolidate discussions among the different groups for a fresh attack on one of the most important problems in theoretical computer science and mathematics.
Cite as

Nadia Creignou, Nicola Galesi, Oliver Kullmann, and Heribert Vollmer. SAT Interactions (Dagstuhl Seminar 12471). In Dagstuhl Reports, Volume 2, Issue 11, pp. 87-101, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@Article{creignou_et_al:DagRep.2.11.87,
  author =	{Creignou, Nadia and Galesi, Nicola and Kullmann, Oliver and Vollmer, Heribert},
  title =	{{SAT Interactions (Dagstuhl Seminar 12471)}},
  pages =	{87--101},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2013},
  volume =	{2},
  number =	{11},
  editor =	{Creignou, Nadia and Galesi, Nicola and Kullmann, Oliver and Vollmer, Heribert},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.2.11.87},
  URN =		{urn:nbn:de:0030-drops-39786},
  doi =		{10.4230/DagRep.2.11.87},
  annote =	{Keywords: satisfiability problem, computational complexity, P-NP question, proof complexity, combinatorics, SAT-solvers, quantified Boolean formulas}
}
Document
DOI: 10.4230/DagSemProc.10061.4
Hardness of Parameterized Resolution

Authors: Olaf Beyersdorff, Nicola Galesi, and Massimo Lauria

Published in: Dagstuhl Seminar Proceedings, Volume 10061, Circuits, Logic, and Games (2010)

Abstract
Parameterized Resolution and, moreover, a general framework for parameterized proof complexity was introduced by Dantchev, Martin, and Szeider (FOCS'07). In that paper, Dantchev et al. show a complexity gap in tree-like Parameterized Resolution for propositional formulas arising from translations of first-order principles. We broadly investigate Parameterized Resolution obtaining the following main results: 1) We introduce a purely combinatorial approach to obtain lower bounds to the proof size in tree-like Parameterized Resolution. For this we devise a new asymmetric Prover-Delayer game which characterizes proofs in (parameterized) tree-like Resolution. By exhibiting good Delayer strategies we then show lower bounds for the pigeonhole principle as well as the order principle. 2) Interpreting a well-known FPT algorithm for vertex cover as a DPLL procedure for Parameterized Resolution, we devise a proof search algorithm for Parameterized Resolution and show that tree-like Parameterized Resolution allows short refutations of all parameterized contradictions given as bounded-width CNF's. 3) We answer a question posed by Dantchev, Martin, and Szeider showing that dag-like Parameterized Resolution is not fpt-bounded. We obtain this result by proving that the pigeonhole principle requires proofs of size $n^{Omega(k)}$ in dag-like Parameterized Resolution. For this lower bound we use a different Prover-Delayer game which was developed for Resolution by Pudlák.
Cite as

Olaf Beyersdorff, Nicola Galesi, and Massimo Lauria. Hardness of Parameterized Resolution. In Circuits, Logic, and Games. Dagstuhl Seminar Proceedings, Volume 10061, pp. 1-28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{beyersdorff_et_al:DagSemProc.10061.4,
  author =	{Beyersdorff, Olaf and Galesi, Nicola and Lauria, Massimo},
  title =	{{Hardness of Parameterized Resolution}},
  booktitle =	{Circuits, Logic, and Games},
  pages =	{1--28},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{10061},
  editor =	{Benjamin Rossman and Thomas Schwentick and Denis Th\'{e}rien and Heribert Vollmer},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.10061.4},
  URN =		{urn:nbn:de:0030-drops-25254},
  doi =		{10.4230/DagSemProc.10061.4},
  annote =	{Keywords: Proof complexity, parameterized complexity, Resolution, Prover-Delayer Games}
}
  • Refine by Type
  • 15 Document/PDF
  • 7 Document/HTML

  • Refine by Publication Year
  • 2 2026
  • 5 2025
  • 1 2023
  • 2 2022
  • 2 2019
  • Show More...

  • Refine by Author
  • 8 Galesi, Nicola
  • 2 Dantchev, Stefan
  • 2 Lauria, Massimo
  • 2 Martin, Barnaby
  • 2 de Rezende, Susanna F.
  • Show More...

  • Refine by Series/Journal
  • 13 LIPIcs
  • 1 DagRep
  • 1 DagSemProc

  • Refine by Classification
  • 7 Theory of computation → Proof complexity
  • 2 Theory of computation → Computational complexity and cryptography
  • 1 Computing methodologies → Representation of polynomials
  • 1 Mathematics of computing
  • 1 Theory of computation
  • Show More...

  • Refine by Keyword
  • 3 Proof Complexity
  • 3 Proof complexity
  • 3 proof complexity
  • 2 Resolution
  • 2 computational complexity
  • 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