DROPS

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.ITCS.2026.81

Supercritical Tradeoff Between Size and Depth for Resolution over Parities

Authors: Dmitry Itsykson and Alexander Knop

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

Abstract

Alekseev and Itsykson (STOC 2025) proved the existence of an unsatisfiable CNF formula such that any resolution over parities (Res(⊕)) refutation must either have exponential size (in the formula size) or superlinear depth (in the number of variables). In this paper, we extend this result by constructing a formula with the same hardness properties, but which additionally admits a resolution refutation of quasi-polynomial size. This establishes a supercritical tradeoff between size and depth for resolution over parities. The proof builds on the framework of Alekseev and Itsykson and relies on a lifting argument applied to the supercritical tradeoff between width and depth in resolution, proposed by Buss and Thapen (IPL 2026).

Cite as

Dmitry Itsykson and Alexander Knop. Supercritical Tradeoff Between Size and Depth for Resolution over Parities. In 17th Innovations in Theoretical Computer Science Conference (ITCS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 362, pp. 81:1-81:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{itsykson_et_al:LIPIcs.ITCS.2026.81,
  author =	{Itsykson, Dmitry and Knop, Alexander},
  title =	{{Supercritical Tradeoff Between Size and Depth for Resolution over Parities}},
  booktitle =	{17th Innovations in Theoretical Computer Science Conference (ITCS 2026)},
  pages =	{81:1--81:20},
  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.81},
  URN =		{urn:nbn:de:0030-drops-253680},
  doi =		{10.4230/LIPIcs.ITCS.2026.81},
  annote =	{Keywords: lifting theorems, resolution depth, resolution over parities, resolution width, supercritical tradeoff}
}

Document

DOI: 10.4230/LIPIcs.MFCS.2025.9

Linear Time Subsequence and Supersequence Regex Matching

Authors: Antoine Amarilli, Florin Manea, Tina Ringleb, and Markus L. Schmid

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

Abstract

It is well-known that checking whether a given string w matches a given regular expression r can be done in quadratic time O(|w|⋅ |r|) and that this cannot be improved to a truly subquadratic running time of O((|w|⋅ |r|)^{1-ε}) assuming the strong exponential time hypothesis (SETH). We study a different matching paradigm where we ask instead whether w has a subsequence that matches r, and show that regex matching in this sense can be solved in linear time O(|w| + |r|). Further, the same holds if we ask for a supersequence. We show that the quantitative variants where we want to compute a longest or shortest subsequence or supersequence of w that matches r can be solved in O(|w|⋅ |r|), i. e., asymptotically no worse than classical regex matching; and we show that O(|w| + |r|) is conditionally not possible for these problems. We also investigate these questions with respect to other natural string relations like the infix, prefix, left-extension or extension relation instead of the subsequence and supersequence relation. We further study the complexity of the universal problem where we ask if all subsequences (or supersequences, infixes, prefixes, left-extensions or extensions) of an input string satisfy a given regular expression.

Cite as

Antoine Amarilli, Florin Manea, Tina Ringleb, and Markus L. Schmid. Linear Time Subsequence and Supersequence Regex Matching. In 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 345, pp. 9:1-9:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{amarilli_et_al:LIPIcs.MFCS.2025.9,
  author =	{Amarilli, Antoine and Manea, Florin and Ringleb, Tina and Schmid, Markus L.},
  title =	{{Linear Time Subsequence and Supersequence Regex Matching}},
  booktitle =	{50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)},
  pages =	{9:1--9: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.9},
  URN =		{urn:nbn:de:0030-drops-241162},
  doi =		{10.4230/LIPIcs.MFCS.2025.9},
  annote =	{Keywords: subsequence, supersequence, regular language, regular expression, automata}
}

Document

DOI: 10.4230/LIPIcs.SAT.2025.7

Redundancy Rules for MaxSAT

Authors: Ilario Bonacina, Maria Luisa Bonet, Sam Buss, and Massimo Lauria

Published in: LIPIcs, Volume 341, 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)

Abstract

The concept of redundancy in SAT leads to more expressive and powerful proof search techniques, e.g., able to express various inprocessing techniques, and originates interesting hierarchies of proof systems [Heule et.al'20, Buss-Thapen'19]. Redundancy has also been integrated in MaxSAT [Ihalainen et.al'22, Berg et.al'23, Bonacina et.al'24]. In this paper, we define a structured hierarchy of redundancy proof systems for MaxSAT, with the goal of studying its proof complexity. We obtain MaxSAT variants of proof systems such as SPR, PR, SR, and others, previously defined for SAT. All our rules are polynomially checkable, unlike [Ihalainen et.al'22]. Moreover, they are simpler and weaker than [Berg et.al'23], and possibly amenable to lower bounds. This work also complements the approach of [Bonacina et.al'24]. Their proof systems use different rule sets for soft and hard clauses, while here we propose a system using only hard clauses and blocking variables. This is easier to integrate with current solvers and proof checkers. We discuss the strength of the systems introduced, we show some limitations of them, and we give a short cost-SR proof that any assignment for the weak pigeonhole principle PHP^m_n falsifies at least m-n clauses.

Cite as

Ilario Bonacina, Maria Luisa Bonet, Sam Buss, and Massimo Lauria. Redundancy Rules for MaxSAT. In 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 341, pp. 7:1-7:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{bonacina_et_al:LIPIcs.SAT.2025.7,
  author =	{Bonacina, Ilario and Bonet, Maria Luisa and Buss, Sam and Lauria, Massimo},
  title =	{{Redundancy Rules for MaxSAT}},
  booktitle =	{28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)},
  pages =	{7:1--7:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-381-2},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{341},
  editor =	{Berg, Jeremias and Nordstr\"{o}m, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2025.7},
  URN =		{urn:nbn:de:0030-drops-237411},
  doi =		{10.4230/LIPIcs.SAT.2025.7},
  annote =	{Keywords: MaxSAT, Redundancy Rules, Pigeonhole Principle}
}

Document

DOI: 10.4230/LIPIcs.SAT.2025.6

An Algebraic Approach to MaxCSP

Authors: Ilario Bonacina and Jordi Levy

Published in: LIPIcs, Volume 341, 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)

Abstract

Recently, there have been some attempts to base SAT and MaxSAT solvers on calculi beyond Resolution, even trying to solve SAT using MaxSAT proof systems. One of these directions was to perform MaxSAT sound inferences using polynomials over finite fields, extending the proof system Polynomial Calculus, which is known to be more powerful than Resolution. In this work, we extend the use of the Polynomial Calculus for optimization, showing its completeness over many-valued variables. This allows using a more direct and efficient encoding of CSP problems (e.g., k-Coloring) and solving the maximization version of the problem on such encoding (e.g., Max-k-Coloring).

Cite as

Ilario Bonacina and Jordi Levy. An Algebraic Approach to MaxCSP. In 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 341, pp. 6:1-6:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{bonacina_et_al:LIPIcs.SAT.2025.6,
  author =	{Bonacina, Ilario and Levy, Jordi},
  title =	{{An Algebraic Approach to MaxCSP}},
  booktitle =	{28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)},
  pages =	{6:1--6:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-381-2},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{341},
  editor =	{Berg, Jeremias and Nordstr\"{o}m, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2025.6},
  URN =		{urn:nbn:de:0030-drops-237407},
  doi =		{10.4230/LIPIcs.SAT.2025.6},
  annote =	{Keywords: MaxCSP, Polynomial Calculus, MaxSAT}
}

Document

DOI: 10.4230/LIPIcs.SAT.2025.21

Improving Reduction Techniques in Pseudo-Boolean Conflict Analysis

Authors: Orestis Lomis, Jo Devriendt, Hendrik Bierlee, and Tias Guns

Published in: LIPIcs, Volume 341, 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)

Abstract

Recent pseudo-Boolean (PB) solvers leverage the cutting planes proof system to perform SAT-style conflict analysis during search. This process learns implied PB constraints, which can prune later parts of the search tree and is crucial to a PB solver’s performance. A key step in PB conflict analysis is the reduction of a reason constraint, which caused a variable propagation that contributed to the conflict. While necessary, reduction generally makes the reason constraint less strong. Consequently, different approaches to reduction have been proposed, broadly categorised as division- or saturation-based, with the aim of preserving the strength of the reason constraint as much as possible. This paper proposes two novel techniques in each reduction category. We theoretically show how each technique yields reason constraints which are at least as strong as those obtained from existing reduction methods. We then evaluate the empirical effectiveness of the reduction techniques on hard knapsack instances and the most recent PB'24 competition benchmarks.

Cite as

Orestis Lomis, Jo Devriendt, Hendrik Bierlee, and Tias Guns. Improving Reduction Techniques in Pseudo-Boolean Conflict Analysis. In 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 341, pp. 21:1-21:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{lomis_et_al:LIPIcs.SAT.2025.21,
  author =	{Lomis, Orestis and Devriendt, Jo and Bierlee, Hendrik and Guns, Tias},
  title =	{{Improving Reduction Techniques in Pseudo-Boolean Conflict Analysis}},
  booktitle =	{28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)},
  pages =	{21:1--21:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-381-2},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{341},
  editor =	{Berg, Jeremias and Nordstr\"{o}m, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2025.21},
  URN =		{urn:nbn:de:0030-drops-237551},
  doi =		{10.4230/LIPIcs.SAT.2025.21},
  annote =	{Keywords: Constraint Programming, Pseudo-Boolean Reasoning, Conflict Analysis}
}

Document

DOI: 10.4230/LIPIcs.CCC.2025.28

Provably Total Functions in the Polynomial Hierarchy

Authors: Noah Fleming, Deniz Imrek, and Christophe Marciot

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

Abstract

TFNP studies the complexity of total, verifiable search problems, and represents the first layer of the total function polynomial hierarchy (TFPH). Recently, problems in higher levels of the TFPH have gained significant attention, partly due to their close connection to circuit lower bounds. However, very little is known about the relationships between problems in levels of the hierarchy beyond TFNP. Connections to proof complexity have had an outsized impact on our understanding of the relationships between subclasses of TFNP in the black-box model. Subclasses are characterized by provability in certain proof systems, which has allowed for tools from proof complexity to be applied in order to separate TFNP problems. In this work we begin a systematic study of the relationship between subclasses of total search problems in the polynomial hierarchy and proof systems. We show that, akin to TFNP, reductions to a problem in TFΣ_d are equivalent to proofs of the formulas expressing the totality of the problems in some Σ_d-proof system. Having established this general correspondence, we examine important subclasses of TFPH. We show that reductions to the StrongAvoid problem are equivalent to proofs in a Σ₂-variant of the (unary) Sherali-Adams proof system. As well, we explore the TFPH classes which result from well-studied proof systems, introducing a number of new TFΣ₂ classes which characterize variants of DNF resolution, as well as TFΣ_d classes capturing levels of Σ_d-bounded-depth Frege.

Cite as

Noah Fleming, Deniz Imrek, and Christophe Marciot. Provably Total Functions in the Polynomial Hierarchy. In 40th Computational Complexity Conference (CCC 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 339, pp. 28:1-28:40, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{fleming_et_al:LIPIcs.CCC.2025.28,
  author =	{Fleming, Noah and Imrek, Deniz and Marciot, Christophe},
  title =	{{Provably Total Functions in the Polynomial Hierarchy}},
  booktitle =	{40th Computational Complexity Conference (CCC 2025)},
  pages =	{28:1--28:40},
  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.28},
  URN =		{urn:nbn:de:0030-drops-237223},
  doi =		{10.4230/LIPIcs.CCC.2025.28},
  annote =	{Keywords: TFNP, TFPH, Proof Complxity, Characterizations}
}

Document

DOI: 10.4230/LIPIcs.CCC.2025.8

Amortized Closure and Its Applications in Lifting for Resolution over Parities

Authors: Klim Efremenko and Dmitry Itsykson

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

Abstract

The notion of closure of a set of linear forms, first introduced by Efremenko, Garlik, and Itsykson [Klim Efremenko et al., 2024], has proven instrumental in proving lower bounds on the sizes of regular and bounded-depth Res(⊕) refutations [Klim Efremenko et al., 2024; Yaroslav Alekseev and Dmitry Itsykson, 2025]. In this work, we present amortized closure, an enhancement that retains the properties of original closure [Klim Efremenko et al., 2024] but offers tighter control on its growth. Specifically, adding a new linear form increases the amortized closure by at most one. We explore two applications that highlight the power of this new concept. Utilizing our newly defined amortized closure, we extend and provide a succinct and elegant proof of the recent lifting theorem by Chattopadhyay and Dvorak [Arkadev Chattopadhyay and Pavel Dvorak, 2025]. Namely we show that for an unsatisfiable CNF formula φ and a 1-stifling gadget g: {0,1}^𝓁 → {0,1}, if the lifted formula φ∘g has a tree-like Res(⊕) refutation of size 2^d and width w, then φ has a resolution refutation of depth d and width w. The original theorem by Chattopadhyay and Dvorak [Arkadev Chattopadhyay and Pavel Dvorak, 2025] applies only to the more restrictive class of strongly stifling gadgets. As a more significant application of amortized closure, we show improved lower bounds for bounded-depth Res(⊕), extending the depth beyond that of Alekseev and Itsykson [Yaroslav Alekseev and Dmitry Itsykson, 2025]. Our result establishes an exponential lower bound for depth-Ω(n log n) Res(⊕) refutations of lifted Tseitin formulas, a notable improvement over the existing depth-Ω(n log log n) Res(⊕) lower bound.

Cite as

Klim Efremenko and Dmitry Itsykson. Amortized Closure and Its Applications in Lifting for Resolution over Parities. In 40th Computational Complexity Conference (CCC 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 339, pp. 8:1-8:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{efremenko_et_al:LIPIcs.CCC.2025.8,
  author =	{Efremenko, Klim and Itsykson, Dmitry},
  title =	{{Amortized Closure and Its Applications in Lifting for Resolution over Parities}},
  booktitle =	{40th Computational Complexity Conference (CCC 2025)},
  pages =	{8:1--8:24},
  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.8},
  URN =		{urn:nbn:de:0030-drops-237023},
  doi =		{10.4230/LIPIcs.CCC.2025.8},
  annote =	{Keywords: lifting, resolution over parities, closure of linear forms, lower bounds, width, depth, size vs depth tradeoff}
}

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.15

Algebraic Pseudorandomness in VNC⁰

Authors: Robert Andrews

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

Abstract

We study the arithmetic complexity of hitting set generators, which are pseudorandom objects used for derandomization of the polynomial identity testing problem. We give new explicit constructions of hitting set generators whose outputs are computable in VNC⁰, i.e., can be computed by arithmetic formulas of constant size. Unconditionally, we construct a VNC⁰-computable generator that hits arithmetic circuits of constant depth and polynomial size. We also give conditional constructions, under strong but plausible hardness assumptions, of VNC⁰-computable generators that hit arithmetic formulas and arithmetic branching programs of polynomial size, respectively. As a corollary of our constructions, we derive lower bounds for subsystems of the Geometric Ideal Proof System of Grochow and Pitassi. Constructions of such generators are implicit in prior work of Kayal on lower bounds for the degree of annihilating polynomials. Our main contribution is a construction whose correctness relies on circuit complexity lower bounds rather than degree lower bounds.

Cite as

Robert Andrews. Algebraic Pseudorandomness in VNC⁰. In 40th Computational Complexity Conference (CCC 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 339, pp. 15:1-15:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{andrews:LIPIcs.CCC.2025.15,
  author =	{Andrews, Robert},
  title =	{{Algebraic Pseudorandomness in VNC⁰}},
  booktitle =	{40th Computational Complexity Conference (CCC 2025)},
  pages =	{15:1--15:15},
  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.15},
  URN =		{urn:nbn:de:0030-drops-237092},
  doi =		{10.4230/LIPIcs.CCC.2025.15},
  annote =	{Keywords: Polynomial identity testing, Algebraic circuits, Ideal Proof System}
}

Document

Track A: Algorithms, Complexity and Games

DOI: 10.4230/LIPIcs.ICALP.2025.22

New Bounds for the Ideal Proof System in Positive Characteristic

Authors: Amik Raj Behera, Nutan Limaye, Varun Ramanathan, and Srikanth Srinivasan

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

Abstract

In this work, we prove upper and lower bounds over fields of positive characteristics for several fragments of the Ideal Proof System (IPS), an algebraic proof system introduced by Grochow and Pitassi (J. ACM 2018). Our results extend the works of Forbes, Shpilka, Tzameret, and Wigderson (Theory of Computing 2021) and also of Govindasamy, Hakoniemi, and Tzameret (FOCS 2022). These works primarily focused on proof systems over fields of characteristic 0, and we are able to extend these results to positive characteristic. The question of proving general IPS lower bounds over positive characteristic is motivated by the important question of proving AC⁰[p]-Frege lower bounds. This connection was observed by Grochow and Pitassi (J. ACM 2018). Additional motivation comes from recent developments in algebraic complexity theory due to Forbes (CCC 2024) who showed how to extend previous lower bounds over characteristic 0 to positive characteristic. In our work, we adapt the functional lower bound method of Forbes et al. (Theory of Computing 2021) to prove exponential-size lower bounds for various subsystems of IPS. In order to establish these size lower bounds, we first prove a tight degree lower bound for a variant of Subset Sum over positive characteristic. This forms the core of all our lower bounds. Additionally, we derive upper bounds for the instances presented above. We show that they have efficient constant-depth IPS refutations. This demonstrates that constant-depth IPS refutations are stronger than the proof systems considered above even in positive characteristic. We also show that constant-depth IPS can efficiently refute a general class of instances, namely all symmetric instances, thereby further uncovering the strength of these algebraic proofs in positive characteristic.

Cite as

Amik Raj Behera, Nutan Limaye, Varun Ramanathan, and Srikanth Srinivasan. New Bounds for the Ideal Proof System in Positive Characteristic. In 52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 334, pp. 22:1-22:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{behera_et_al:LIPIcs.ICALP.2025.22,
  author =	{Behera, Amik Raj and Limaye, Nutan and Ramanathan, Varun and Srinivasan, Srikanth},
  title =	{{New Bounds for the Ideal Proof System in Positive Characteristic}},
  booktitle =	{52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025)},
  pages =	{22:1--22: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.22},
  URN =		{urn:nbn:de:0030-drops-233992},
  doi =		{10.4230/LIPIcs.ICALP.2025.22},
  annote =	{Keywords: Ideal Proof Systems, Algebraic Complexity, Positive Characteristic}
}

Document

DOI: 10.4230/LIPIcs.ICDT.2025.21

Targeted Least Cardinality Candidate Key for Relational Databases

Authors: Vasileios Nakos, Hung Q. Ngo, and Charalampos E. Tsourakakis

Published in: LIPIcs, Volume 328, 28th International Conference on Database Theory (ICDT 2025)

Abstract

Functional dependencies (FDs) are a central theme in databases, playing a major role in the design of database schemas and the optimization of queries [Ramakrishnan and Gehrke, 2003]. In this work, we introduce the targeted least cardinality candidate key problem (TCAND). This problem is defined over a set of functional dependencies ℱ and a target variable set T ⊆ V, and it aims to find the smallest set X ⊆ V such that the FD X → T can be derived from ℱ. The TCAND problem generalizes the well-known NP-hard problem of finding the least cardinality candidate key [Lucchesi and Osborn, 1978], which has been previously demonstrated to be at least as difficult as the set cover problem. We present an integer programming (IP) formulation for the TCAND problem, analogous to a layered set cover problem. We analyze its linear programming (LP) relaxation from two perspectives: we propose two approximation algorithms and investigate the integrality gap. Our findings indicate that the approximation upper bounds for our algorithms are not significantly improvable through LP rounding, a notable distinction from the standard Set Cover problem. Additionally, we discover that a generalization of the TCAND problem is equivalent to a variant of the Set Cover problem, named Red Blue Set Cover [Carr et al., 2000], which cannot be approximated within a sub-polynomial factor in polynomial time under plausible conjectures [Chlamtáč et al., 2023]. Despite the extensive history surrounding the issue of identifying the least cardinality candidate key, our research contributes new theoretical insights, novel algorithms, and demonstrates that the general TCAND problem poses complexities beyond those encountered in the Set Cover problem.

Cite as

Vasileios Nakos, Hung Q. Ngo, and Charalampos E. Tsourakakis. Targeted Least Cardinality Candidate Key for Relational Databases. In 28th International Conference on Database Theory (ICDT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 328, pp. 21:1-21:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{nakos_et_al:LIPIcs.ICDT.2025.21,
  author =	{Nakos, Vasileios and Ngo, Hung Q. and Tsourakakis, Charalampos E.},
  title =	{{Targeted Least Cardinality Candidate Key for Relational Databases}},
  booktitle =	{28th International Conference on Database Theory (ICDT 2025)},
  pages =	{21:1--21:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-364-5},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{328},
  editor =	{Roy, Sudeepa and Kara, Ahmet},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICDT.2025.21},
  URN =		{urn:nbn:de:0030-drops-229628},
  doi =		{10.4230/LIPIcs.ICDT.2025.21},
  annote =	{Keywords: functional dependencies, candidate key, approximation algorithms, hardness}
}

Document

DOI: 10.4230/LIPIcs.SAT.2024.20

The Strength of the Dominance Rule

Authors: Leszek Aleksander Kołodziejczyk and Neil Thapen

Published in: LIPIcs, Volume 305, 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)

Abstract

It has become standard that, when a SAT solver decides that a CNF Γ is unsatisfiable, it produces a certificate of unsatisfiability in the form of a refutation of Γ in some proof system. The system typically used is DRAT, which is equivalent to extended resolution (ER) - for example, until this year DRAT refutations were required in the annual SAT competition. Recently [Bogaerts et al. 2023] introduced a new proof system, associated with the tool VeriPB, which is at least as strong as DRAT and is further able to handle certain symmetry-breaking techniques. We show that this system simulates the proof system G₁, which allows limited reasoning with QBFs and forms the first level above ER in a natural hierarchy of proof systems. This hierarchy is not known to be strict, but nevertheless this is evidence that the system of [Bogaerts et al. 2023] is plausibly strictly stronger than ER and DRAT. In the other direction, we show that symmetry-breaking for a single symmetry can be handled inside ER.

Cite as

Leszek Aleksander Kołodziejczyk and Neil Thapen. The Strength of the Dominance Rule. In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, pp. 20:1-20:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{kolodziejczyk_et_al:LIPIcs.SAT.2024.20,
  author =	{Ko{\l}odziejczyk, Leszek Aleksander and Thapen, Neil},
  title =	{{The Strength of the Dominance Rule}},
  booktitle =	{27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)},
  pages =	{20:1--20:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-334-8},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{305},
  editor =	{Chakraborty, Supratik and Jiang, Jie-Hong Roland},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2024.20},
  URN =		{urn:nbn:de:0030-drops-205421},
  doi =		{10.4230/LIPIcs.SAT.2024.20},
  annote =	{Keywords: proof complexity, DRAT, symmetry breaking, dominance}
}

Document

DOI: 10.4230/LIPIcs.STACS.2024.59

Lower Bounds for Set-Blocked Clauses Proofs

Authors: Emre Yolcu

Published in: LIPIcs, Volume 289, 41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024)

Abstract

We study propositional proof systems with inference rules that formalize restricted versions of the ability to make assumptions that hold without loss of generality, commonly used informally to shorten proofs. Each system we study is built on resolution. They are called BC⁻, RAT⁻, SBC⁻, and GER⁻, denoting respectively blocked clauses, resolution asymmetric tautologies, set-blocked clauses, and generalized extended resolution - all "without new variables." They may be viewed as weak versions of extended resolution (ER) since they are defined by first generalizing the extension rule and then taking away the ability to introduce new variables. Except for SBC⁻, they are known to be strictly between resolution and extended resolution. Several separations between these systems were proved earlier by exploiting the fact that they effectively simulate ER. We answer the questions left open: We prove exponential lower bounds for SBC⁻ proofs of a binary encoding of the pigeonhole principle, which separates ER from SBC⁻. Using this new separation, we prove that both RAT⁻ and GER⁻ are exponentially separated from SBC⁻. This completes the picture of their relative strengths.

Cite as

Emre Yolcu. Lower Bounds for Set-Blocked Clauses Proofs. In 41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 289, pp. 59:1-59:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{yolcu:LIPIcs.STACS.2024.59,
  author =	{Yolcu, Emre},
  title =	{{Lower Bounds for Set-Blocked Clauses Proofs}},
  booktitle =	{41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024)},
  pages =	{59:1--59:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-311-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{289},
  editor =	{Beyersdorff, Olaf and Kant\'{e}, Mamadou Moustapha and Kupferman, Orna and Lokshtanov, Daniel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2024.59},
  URN =		{urn:nbn:de:0030-drops-197698},
  doi =		{10.4230/LIPIcs.STACS.2024.59},
  annote =	{Keywords: proof complexity, separations, resolution, extended resolution, blocked clauses}
}

Document

RANDOM

DOI: 10.4230/LIPIcs.APPROX/RANDOM.2023.56

Robustness for Space-Bounded Statistical Zero Knowledge

Authors: Eric Allender, Jacob Gray, Saachi Mutreja, Harsha Tirumala, and Pengxiang Wang

Published in: LIPIcs, Volume 275, Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques (APPROX/RANDOM 2023)

Abstract

We show that the space-bounded Statistical Zero Knowledge classes SZK_L and NISZK_L are surprisingly robust, in that the power of the verifier and simulator can be strengthened or weakened without affecting the resulting class. Coupled with other recent characterizations of these classes [Eric Allender et al., 2023], this can be viewed as lending support to the conjecture that these classes may coincide with the non-space-bounded classes SZK and NISZK, respectively.

Cite as

Eric Allender, Jacob Gray, Saachi Mutreja, Harsha Tirumala, and Pengxiang Wang. Robustness for Space-Bounded Statistical Zero Knowledge. In Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques (APPROX/RANDOM 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 275, pp. 56:1-56:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{allender_et_al:LIPIcs.APPROX/RANDOM.2023.56,
  author =	{Allender, Eric and Gray, Jacob and Mutreja, Saachi and Tirumala, Harsha and Wang, Pengxiang},
  title =	{{Robustness for Space-Bounded Statistical Zero Knowledge}},
  booktitle =	{Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques (APPROX/RANDOM 2023)},
  pages =	{56:1--56:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-296-9},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{275},
  editor =	{Megow, Nicole and Smith, Adam},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.APPROX/RANDOM.2023.56},
  URN =		{urn:nbn:de:0030-drops-188815},
  doi =		{10.4230/LIPIcs.APPROX/RANDOM.2023.56},
  annote =	{Keywords: Interactive Proofs}
}

21 Search Results for "Buss, Sam"

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Thanks for your feedback!

Could not send message