14 Search Results for "Cook, Stephen A."

Document
DOI: 10.4230/LIPIcs.CCC.2024.15
Quantum Automating TC⁰-Frege Is LWE-Hard

Authors: Noel Arteche, Gaia Carenini, and Matthew Gray

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

Abstract
We prove the first hardness results against efficient proof search by quantum algorithms. We show that under Learning with Errors (LWE), the standard lattice-based cryptographic assumption, no quantum algorithm can weakly automate TC⁰-Frege. This extends the line of results of Krajíček and Pudlák (Information and Computation, 1998), Bonet, Pitassi, and Raz (FOCS, 1997), and Bonet, Domingo, Gavaldà, Maciel, and Pitassi (Computational Complexity, 2004), who showed that Extended Frege, TC⁰-Frege and AC⁰-Frege, respectively, cannot be weakly automated by classical algorithms if either the RSA cryptosystem or the Diffie-Hellman key exchange protocol are secure. To the best of our knowledge, this is the first interaction between quantum computation and propositional proof search.
Cite as

Noel Arteche, Gaia Carenini, and Matthew Gray. Quantum Automating TC⁰-Frege Is LWE-Hard. In 39th Computational Complexity Conference (CCC 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 300, pp. 15:1-15:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{arteche_et_al:LIPIcs.CCC.2024.15,
  author =	{Arteche, Noel and Carenini, Gaia and Gray, Matthew},
  title =	{{Quantum Automating TC⁰-Frege Is LWE-Hard}},
  booktitle =	{39th Computational Complexity Conference (CCC 2024)},
  pages =	{15:1--15:25},
  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.15},
  URN =		{urn:nbn:de:0030-drops-204117},
  doi =		{10.4230/LIPIcs.CCC.2024.15},
  annote =	{Keywords: automatability, post-quantum cryptography, feasible interpolation}
}
Document
DOI: 10.4230/LIPIcs.CCC.2024.33
Failure of Feasible Disjunction Property for k-DNF Resolution and NP-Hardness of Automating It

Authors: Michal Garlík

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

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

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

Copy BibTex To Clipboard

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

Authors: Noam Mazor and Rafael Pass

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

Abstract
We demonstrate that under believable cryptographic hardness assumptions, Gap versions of standard meta-complexity problems, such as the Minimum Circuit Size Problem (MCSP) and the Minimum Time-Bounded Kolmogorov Complexity problem (MKTP) are not NP-complete w.r.t. Levin (i.e., witness-preserving many-to-one) reductions. In more detail: - Assuming the existence of indistinguishability obfuscation, and subexponentially-secure one-way functions, an appropriate Gap version of MCSP is not NP-complete under randomized Levin-reductions. - Assuming the existence of subexponentially-secure indistinguishability obfuscation, subexponentially-secure one-way functions and injective PRGs, an appropriate Gap version of MKTP is not NP-complete under randomized Levin-reductions.
Cite as

Noam Mazor and Rafael Pass. Gap MCSP Is Not (Levin) NP-Complete in Obfustopia. In 39th Computational Complexity Conference (CCC 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 300, pp. 36:1-36:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{mazor_et_al:LIPIcs.CCC.2024.36,
  author =	{Mazor, Noam and Pass, Rafael},
  title =	{{Gap MCSP Is Not (Levin) NP-Complete in Obfustopia}},
  booktitle =	{39th Computational Complexity Conference (CCC 2024)},
  pages =	{36:1--36:21},
  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.36},
  URN =		{urn:nbn:de:0030-drops-204322},
  doi =		{10.4230/LIPIcs.CCC.2024.36},
  annote =	{Keywords: Kolmogorov complexity, MCSP, Levin Reduction}
}
Document
Track A: Algorithms, Complexity and Games
DOI: 10.4230/LIPIcs.ICALP.2024.12
From Proof Complexity to Circuit Complexity via Interactive Protocols

Authors: Noel Arteche, Erfan Khaniki, Ján Pich, and Rahul Santhanam

Published in: LIPIcs, Volume 297, 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)

Abstract
Folklore in complexity theory suspects that circuit lower bounds against NC¹ or P/poly, currently out of reach, are a necessary step towards proving strong proof complexity lower bounds for systems like Frege or Extended Frege. Establishing such a connection formally, however, is already daunting, as it would imply the breakthrough separation NEXP ⊈ P/poly, as recently observed by Pich and Santhanam [Pich and Santhanam, 2023]. We show such a connection conditionally for the Implicit Extended Frege proof system (iEF) introduced by Krajíček [Krajíček, 2004], capable of formalizing most of contemporary complexity theory. In particular, we show that if iEF proves efficiently the standard derandomization assumption that a concrete Boolean function is hard on average for subexponential-size circuits, then any superpolynomial lower bound on the length of iEF proofs implies #P ⊈ FP/poly (which would in turn imply, for example, PSPACE ⊈ P/poly). Our proof exploits the formalization inside iEF of the soundness of the sum-check protocol of Lund, Fortnow, Karloff, and Nisan [Lund et al., 1992]. This has consequences for the self-provability of circuit upper bounds in iEF. Interestingly, further improving our result seems to require progress in constructing interactive proof systems with more efficient provers.
Cite as

Noel Arteche, Erfan Khaniki, Ján Pich, and Rahul Santhanam. From Proof Complexity to Circuit Complexity via Interactive Protocols. In 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 297, pp. 12:1-12:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{arteche_et_al:LIPIcs.ICALP.2024.12,
  author =	{Arteche, Noel and Khaniki, Erfan and Pich, J\'{a}n and Santhanam, Rahul},
  title =	{{From Proof Complexity to Circuit Complexity via Interactive Protocols}},
  booktitle =	{51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)},
  pages =	{12:1--12:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-322-5},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{297},
  editor =	{Bringmann, Karl and Grohe, Martin and Puppis, Gabriele and Svensson, Ola},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2024.12},
  URN =		{urn:nbn:de:0030-drops-201557},
  doi =		{10.4230/LIPIcs.ICALP.2024.12},
  annote =	{Keywords: proof complexity, circuit complexity, interactive protocols}
}
Document
Track A: Algorithms, Complexity and Games
DOI: 10.4230/LIPIcs.ICALP.2024.18
It’s Hard to HAC Average Linkage!

Authors: MohammadHossein Bateni, Laxman Dhulipala, Kishen N. Gowda, D. Ellis Hershkowitz, Rajesh Jayaram, and Jakub Łącki

Published in: LIPIcs, Volume 297, 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)

Abstract
Average linkage Hierarchical Agglomerative Clustering (HAC) is an extensively studied and applied method for hierarchical clustering. Recent applications to massive datasets have driven significant interest in near-linear-time and efficient parallel algorithms for average linkage HAC. We provide hardness results that rule out such algorithms. On the sequential side, we establish a runtime lower bound of n^{3/2-ε} on n node graphs for sequential combinatorial algorithms under standard fine-grained complexity assumptions. This essentially matches the best-known running time for average linkage HAC. On the parallel side, we prove that average linkage HAC likely cannot be parallelized even on simple graphs by showing that it is CC-hard on trees of diameter 4. On the possibility side, we demonstrate that average linkage HAC can be efficiently parallelized (i.e., it is in NC) on paths and can be solved in near-linear time when the height of the output cluster hierarchy is small.
Cite as

MohammadHossein Bateni, Laxman Dhulipala, Kishen N. Gowda, D. Ellis Hershkowitz, Rajesh Jayaram, and Jakub Łącki. It’s Hard to HAC Average Linkage!. In 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 297, pp. 18:1-18:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{bateni_et_al:LIPIcs.ICALP.2024.18,
  author =	{Bateni, MohammadHossein and Dhulipala, Laxman and Gowda, Kishen N. and Hershkowitz, D. Ellis and Jayaram, Rajesh and {\L}\k{a}cki, Jakub},
  title =	{{It’s Hard to HAC Average Linkage!}},
  booktitle =	{51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)},
  pages =	{18:1--18:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-322-5},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{297},
  editor =	{Bringmann, Karl and Grohe, Martin and Puppis, Gabriele and Svensson, Ola},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2024.18},
  URN =		{urn:nbn:de:0030-drops-201613},
  doi =		{10.4230/LIPIcs.ICALP.2024.18},
  annote =	{Keywords: Clustering, Hierarchical Graph Clustering, HAC, Fine-Grained Complexity, Parallel Algorithms, CC}
}
Document
Track A: Algorithms, Complexity and Games
DOI: 10.4230/LIPIcs.ICALP.2024.117
Bounds on the Total Coefficient Size of Nullstellensatz Proofs of the Pigeonhole Principle

Authors: Aaron Potechin and Aaron Zhang

Published in: LIPIcs, Volume 297, 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)

Abstract
We show that the minimum total coefficient size of a Nullstellensatz proof of the pigeonhole principle on n+1 pigeons and n holes is 2^{Θ(n)}. We also investigate the ordering principle and construct an explicit Nullstellensatz proof for the ordering principle on n elements with total coefficient size 2ⁿ - n.
Cite as

Aaron Potechin and Aaron Zhang. Bounds on the Total Coefficient Size of Nullstellensatz Proofs of the Pigeonhole Principle. In 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 297, pp. 117:1-117:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{potechin_et_al:LIPIcs.ICALP.2024.117,
  author =	{Potechin, Aaron and Zhang, Aaron},
  title =	{{Bounds on the Total Coefficient Size of Nullstellensatz Proofs of the Pigeonhole Principle}},
  booktitle =	{51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)},
  pages =	{117:1--117:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-322-5},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{297},
  editor =	{Bringmann, Karl and Grohe, Martin and Puppis, Gabriele and Svensson, Ola},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2024.117},
  URN =		{urn:nbn:de:0030-drops-202604},
  doi =		{10.4230/LIPIcs.ICALP.2024.117},
  annote =	{Keywords: Proof complexity, Nullstellensatz, pigeonhole principle, coefficient size}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.CSL.2020.5
From Classical Proof Theory to P versus NP: a Guide to Bounded Theories (Invited Talk)

Authors: Iddo Tzameret

Published in: LIPIcs, Volume 152, 28th EACSL Annual Conference on Computer Science Logic (CSL 2020)

Abstract
This talk explores the question of what does logic and specifically proof theory can tell us about the fundamental hardness questions in computational complexity. We start with a brief description of the main concepts behind bounded arithmetic which is a family of weak formal theories of arithmetic that mirror in a precise manner the world of propositional proofs: if a statement of a given form is provable in a given bounded arithmetic theory then the same statement is suitably translated to a family of propositional formulas with short (polynomial-size) proofs in a corresponding propositional proof system. We will proceed to describe the motivations behind the study of bounded arithmetic theories, their corresponding propositional proof systems, and how they relate to the fundamental complexity class separations and circuit lower bounds questions in computational complexity. We provide a collage of results and recent developments showing how bounded arithmetic and propositional proof complexity form a cohesive framework in which both concrete combinatorial questions about complexity as well as meta-mathematical questions about provability of statements of complexity theory itself, are studied. Specific topics we shall mention are: (i) The bounded reverse mathematics program [Stephen Cook and Phuong Nguyen, 2010]: studying the weakest possible axiomatic assumptions that can prove important results in mathematics and computing (cf. [Iddo Tzameret and Stephen A. Cook, 2017; Pavel Hrubeš and Iddo Tzameret, 2015]), and the correspondence between circuit classes and theories. (ii) The meta-mathematics of computational complexity: what kind of reasoning power do we need in order to prove major results in complexity theory itself, and applications to complexity lower bounds (cf. [Razborov, 1995; Rahul Santhanam and Jan Pich, 2019]). (iii) Proof complexity: the systematic treatment of propositional proofs as combinatorial and algebraic objects and their algorithmic applications (cf. [Samuel Buss, 2012; Tonnian Pitassi and Iddo Tzameret, 2016; Noah Fleming et al., 2019]).
Cite as

Iddo Tzameret. From Classical Proof Theory to P versus NP: a Guide to Bounded Theories (Invited Talk). In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 5:1-5:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{tzameret:LIPIcs.CSL.2020.5,
  author =	{Tzameret, Iddo},
  title =	{{From Classical Proof Theory to P versus NP: a Guide to Bounded Theories}},
  booktitle =	{28th EACSL Annual Conference on Computer Science Logic (CSL 2020)},
  pages =	{5:1--5:2},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-132-0},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{152},
  editor =	{Fern\'{a}ndez, Maribel and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2020.5},
  URN =		{urn:nbn:de:0030-drops-116482},
  doi =		{10.4230/LIPIcs.CSL.2020.5},
  annote =	{Keywords: Bounded arithmetic, complexity class separations, circuit complexity, proof complexity, weak theories of arithmetic, feasible mathematics}
}
Document
DOI: 10.4230/LIPIcs.CSL.2018.18
A Recursion-Theoretic Characterisation of the Positive Polynomial-Time Functions

Authors: Anupam Das and Isabel Oitavem

Published in: LIPIcs, Volume 119, 27th EACSL Annual Conference on Computer Science Logic (CSL 2018)

Abstract
We extend work of Lautemann, Schwentick and Stewart [Clemens Lautemann et al., 1996] on characterisations of the "positive" polynomial-time predicates (posP, also called mP by Grigni and Sipser [Grigni and Sipser, 1992]) to function classes. Our main result is the obtention of a function algebra for the positive polynomial-time functions (posFP) by imposing a simple uniformity constraint on the bounded recursion operator in Cobham's characterisation of FP. We show that a similar constraint on a function algebra based on safe recursion, in the style of Bellantoni and Cook [Stephen Bellantoni and Stephen A. Cook, 1992], yields an "implicit" characterisation of posFP, mentioning neither explicit bounds nor explicit monotonicity constraints.
Cite as

Anupam Das and Isabel Oitavem. A Recursion-Theoretic Characterisation of the Positive Polynomial-Time Functions. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 18:1-18:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{das_et_al:LIPIcs.CSL.2018.18,
  author =	{Das, Anupam and Oitavem, Isabel},
  title =	{{A Recursion-Theoretic Characterisation of the Positive Polynomial-Time Functions}},
  booktitle =	{27th EACSL Annual Conference on Computer Science Logic (CSL 2018)},
  pages =	{18:1--18:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-088-0},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{119},
  editor =	{Ghica, Dan R. and Jung, Achim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.18},
  URN =		{urn:nbn:de:0030-drops-96851},
  doi =		{10.4230/LIPIcs.CSL.2018.18},
  annote =	{Keywords: Monotone complexity, Positive complexity, Function classes, Function algebras, Recursion-theoretic characterisations, Implicit complexity, Logic}
}
Document
DOI: 10.4230/LIPIcs.CSL.2013.296
Theories for Subexponential-size Bounded-depth Frege Proofs

Authors: Kaveh Ghasemloo and Stephen A. Cook

Published in: LIPIcs, Volume 23, Computer Science Logic 2013 (CSL 2013)

Abstract
This paper is a contribution to our understanding of the relationship between uniform and nonuniform proof complexity. The latter studies the lengths of proofs in various propositional proof systems such as Frege and bounded-depth Frege systems, and the former studies the strength of the corresponding logical theories such as VNC1 and V0 in [Cook/Nguyen, 2010]. A superpolynomial lower bound on the length of proofs in a propositional proof system for a family of tautologies expressing a result like the pigeonhole principle implies that the result is not provable in the theory associated with the propositional proof system. We define a new class of bounded arithmetic theories n^epsilon-ioV^\infinity for epsilon < 1 and show that they correspond to complexity classes AltTime(O(1),O(n^epsilon)), uniform classes of subexponential-size bounded-depth circuits DepthSize(O(1),2^O(n^epsilon)). To accomplish this we introduce the novel idea of using types to control the amount of composition in our bounded arithmetic theories. This allows our theories to capture complexity classes that have weaker closure properties and are not closed under composition. We show that the proofs of Sigma^B_0-theorems in our theories translate to subexponential-size bounded-depth Frege proofs. We use these theories to formalize the complexity theory result that problems in uniform NC1 circuits can be computed by uniform subexponential bounded-depth circuits in [Allender/Koucky, 2010]. We prove that our theories contain a variation of the theory VNC1 for the complexity class NC1. We formalize Buss's proof in [Buss, 1993] that the (unbalanced) Boolean Formula Evaluation problem is in NC1 and use it to prove the soundness of Frege systems. As a corollary, we obtain an alternative proof of [Filmus et al, ICALP, 2011] that polynomial-size Frege proofs can be simulated by subexponential-size bounded-depth Frege proofs. Our results can be extended to theories corresponding to other nice complexity classes inside NTimeSpace(n^O(1), n^o(1)) such as NL. This is achieved by essentially formalizing the containment NTimeSpace(n^O(1), n^o(1)) \subseteq AltTime(O(1), O(n^epsilon)) for all epsilon > 0.
Cite as

Kaveh Ghasemloo and Stephen A. Cook. Theories for Subexponential-size Bounded-depth Frege Proofs. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 296-315, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@InProceedings{ghasemloo_et_al:LIPIcs.CSL.2013.296,
  author =	{Ghasemloo, Kaveh and Cook, Stephen A.},
  title =	{{Theories for Subexponential-size Bounded-depth Frege Proofs}},
  booktitle =	{Computer Science Logic 2013 (CSL 2013)},
  pages =	{296--315},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-60-6},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{23},
  editor =	{Ronchi Della Rocca, Simona},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.296},
  URN =		{urn:nbn:de:0030-drops-42044},
  doi =		{10.4230/LIPIcs.CSL.2013.296},
  annote =	{Keywords: Computational Complexity Theory, Proof Complexity, Bounded Arithmetic, NC1-Frege, AC0- Frege}
}
Document
DOI: 10.4230/LIPIcs.STACS.2013.622
Pebbling, Entropy and Branching Program Size Lower Bounds

Authors: Balagopal Komarath and Jayalal M. N. Sarma

Published in: LIPIcs, Volume 20, 30th International Symposium on Theoretical Aspects of Computer Science (STACS 2013)

Abstract
We contribute to the program of proving lower bounds on the size of branching programs solving the Tree Evaluation Problem introduced in (Stephen A. Cook, Pierre McKenzie, Dustin Wehr, Mark Braverman, and Rahul Santhanam, 2012). Proving an exponential lower bound for the size of the non-deterministic thrifty branching programs would separate NL from P under the thrifty hypothesis. In this context, we consider a restriction of non-deterministic thrifty branching programs called bitwise-independence. We show that any bitwise-independent non-deterministic thrifty branching program solving BT_2(h,k) must have at least 1/2 k^{h/2} states. Prior to this work, lower bounds were known for general branching programs only for fixed heights h=2,3,4 (Stephen A. Cook, Pierre McKenzie, Dustin Wehr, Mark Braverman, and Rahul Santhanam, 2012). Our lower bounds are also tight (up to a factor of k), since the known (Stephen A. Cook, Pierre McKenzie, Dustin Wehr, Mark Braverman, and Rahul Santhanam, 2012) non-deterministic thrifty branching programs for this problem of size O(k^{h/2+1}) are bitwise-independent. We prove our results by associating a fractional pebbling strategy with any bitwise-independent non-deterministic thrifty branching program solving the Tree Evaluation Problem. Such a connection was not known previously even for fixed heights. Our main technique is the entropy method introduced by Jukna and Zak (S. Jukna and S. Žák, 2003) originally in the context of proving lower bounds for read-once branching programs. We also show that the previous lower bounds known (Stephen A. Cook, Pierre McKenzie, Dustin Wehr, Mark Braverman, and Rahul Santhanam, 2012) for deterministic branching programs for Tree Evaluation Problem can be obtained using this approach. Using this method, we also show tight lower bounds for any k-way deterministic branching program solving Tree Evaluation Problem when the instances are restricted to have the same group operation in all internal nodes.
Cite as

Balagopal Komarath and Jayalal M. N. Sarma. Pebbling, Entropy and Branching Program Size Lower Bounds. In 30th International Symposium on Theoretical Aspects of Computer Science (STACS 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 20, pp. 622-633, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@InProceedings{komarath_et_al:LIPIcs.STACS.2013.622,
  author =	{Komarath, Balagopal and Sarma, Jayalal M. N.},
  title =	{{Pebbling, Entropy and Branching Program Size Lower Bounds}},
  booktitle =	{30th International Symposium on Theoretical Aspects of Computer Science (STACS 2013)},
  pages =	{622--633},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-50-7},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{20},
  editor =	{Portier, Natacha and Wilke, Thomas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2013.622},
  URN =		{urn:nbn:de:0030-drops-39709},
  doi =		{10.4230/LIPIcs.STACS.2013.622},
  annote =	{Keywords: Pebbling, Entropy Method, Branching Programs, Size Lower Bounds.}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.CSL.2012.9
Connecting Complexity Classes, Weak Formal Theories, and Propositional Proof Systems (Invited Talk)

Authors: Stephen A. Cook

Published in: LIPIcs, Volume 16, Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL (2012)

Abstract
This is a survey talk explaining the connection between the three items mentioned in the title.
Cite as

Stephen A. Cook. Connecting Complexity Classes, Weak Formal Theories, and Propositional Proof Systems (Invited Talk). In Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 16, pp. 9-11, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{cook:LIPIcs.CSL.2012.9,
  author =	{Cook, Stephen A.},
  title =	{{Connecting Complexity Classes, Weak Formal Theories, and Propositional Proof Systems}},
  booktitle =	{Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL},
  pages =	{9--11},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-42-2},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{16},
  editor =	{C\'{e}gielski, Patrick and Durand, Arnaud},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2012.9},
  URN =		{urn:nbn:de:0030-drops-36594},
  doi =		{10.4230/LIPIcs.CSL.2012.9},
  annote =	{Keywords: Complexity Classes, Weak Formal Theories, Propositional Proof Systems}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.CSL.2012.12
Satisfiability: where Theory meets Practice (Invited Talk)

Authors: Inês Lynce

Published in: LIPIcs, Volume 16, Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL (2012)

Abstract
Propositional Satisfiability (SAT) is a keystone in the history of computer science. SAT was the first problem shown to be NP-complete in 1971 by Stephen Cook. Having passed more than 40 years from then, SAT is now a lively research field where theory and practice have a natural intermixing. In this talk, we overview the use of SAT in practical domains, where SAT is thought in a broad sense, i.e. including SAT extensions such as Maximum Satisfiability (MaxSAT), Pseudo-Boolean Optimization (PBO) and Quantified Boolean Formulas (QBF).
Cite as

Inês Lynce. Satisfiability: where Theory meets Practice (Invited Talk). In Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 16, pp. 12-13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{lynce:LIPIcs.CSL.2012.12,
  author =	{Lynce, In\^{e}s},
  title =	{{Satisfiability: where Theory meets Practice}},
  booktitle =	{Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL},
  pages =	{12--13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-42-2},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{16},
  editor =	{C\'{e}gielski, Patrick and Durand, Arnaud},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2012.12},
  URN =		{urn:nbn:de:0030-drops-36600},
  doi =		{10.4230/LIPIcs.CSL.2012.12},
  annote =	{Keywords: Propositional Satisfiability, SAT solvers, Applications}
}
Document
DOI: 10.4230/LIPIcs.CSL.2011.381
A Formal Theory for the Complexity Class Associated with the Stable Marriage Problem

Authors: Dai Tri Man Lê, Stephen A. Cook, and Yuli Ye

Published in: LIPIcs, Volume 12, Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL (2011)

Abstract
Subramanian defined the complexity class CC as the set of problems log-space reducible to the comparator circuit value problem. He proved that several other problems are complete for CC, including the stable marriage problem, and finding the lexicographical first maximal matching in a bipartite graph. We suggest alternative definitions of CC based on different reducibilities and introduce a two-sorted theory VCC* based on one of them. We sharpen and simplify Subramanian's completeness proofs for the above two problems and formalize them in VCC*.
Cite as

Dai Tri Man Lê, Stephen A. Cook, and Yuli Ye. A Formal Theory for the Complexity Class Associated with the Stable Marriage Problem. In Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 12, pp. 381-395, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@InProceedings{le_et_al:LIPIcs.CSL.2011.381,
  author =	{L\^{e}, Dai Tri Man and Cook, Stephen A. and Ye, Yuli},
  title =	{{A Formal Theory for the Complexity Class Associated with the Stable Marriage Problem}},
  booktitle =	{Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL},
  pages =	{381--395},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-32-3},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{12},
  editor =	{Bezem, Marc},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2011.381},
  URN =		{urn:nbn:de:0030-drops-32440},
  doi =		{10.4230/LIPIcs.CSL.2011.381},
  annote =	{Keywords: bounded arithmetic, complexity theory, comparator circuits}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2009.2311
Fractional Pebbling and Thrifty Branching Programs

Authors: Mark Braverman, Stephen Cook, Pierre McKenzie, Rahul Santhanam, and Dustin Wehr

Published in: LIPIcs, Volume 4, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (2009)

Abstract
We study the branching program complexity of the {\em tree evaluation problem}, introduced in \cite{BrCoMcSaWe09} as a candidate for separating \nl\ from\logcfl. The input to the problem is a rooted, balanced $d$-ary tree of height$h$, whose internal nodes are labelled with $d$-ary functions on$[k]=\{1,\ldots,k\}$, and whose leaves are labelled with elements of $[k]$.Each node obtains a value in $[k]$ equal to its $d$-ary function applied to the values of its $d$ children. The output is the value of the root. Deterministic $k$-way branching programs as related to black pebbling algorithms have been studied in \cite{BrCoMcSaWe09}. Here we introduce the notion of {\em fractional pebbling} of graphs to study non-deterministicbranching program size. We prove that this yields non-deterministic branching programs with $\Theta(k^{h/2+1})$ states solving the Boolean problem ``determine whether the root has value 1'' for binary trees - this isasymptotically better than the branching program size corresponding toblack-white pebbling. We prove upper and lower bounds on the fractionalpebbling number of $d$-ary trees, as well as a general result relating thefractional pebbling number of a graph to the black-white pebbling number. We introduce a simple semantic restriction called {\em thrifty} on $k$-way branching programs solving tree evaluation problems and show that the branchingprogram size bound of $\Theta(k^h)$ is tight (up to a constant factor) for all $h\ge 2$ for deterministic thrifty programs. We show that thenon-deterministic branching programs that correspond to fractional pebbling are thrifty as well, and that the bound of $\Theta(k^{h/2+1})$ is tight for non-deterministic thrifty programs for $h=2,3,4$. We hypothesise that thrifty branching programs are optimal among $k$-way branching programs solving the tree evaluation problem - proving this for deterministic programs would separate \lspace\ from \logcfl\, and proving it for non-deterministic programs would separate \nl\ from \logcfl.
Cite as

Mark Braverman, Stephen Cook, Pierre McKenzie, Rahul Santhanam, and Dustin Wehr. Fractional Pebbling and Thrifty Branching Programs. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. Leibniz International Proceedings in Informatics (LIPIcs), Volume 4, pp. 109-120, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)

Copy BibTex To Clipboard

@InProceedings{braverman_et_al:LIPIcs.FSTTCS.2009.2311,
  author =	{Braverman, Mark and Cook, Stephen and McKenzie, Pierre and Santhanam, Rahul and Wehr, Dustin},
  title =	{{Fractional Pebbling and Thrifty Branching Programs}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science},
  pages =	{109--120},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-13-2},
  ISSN =	{1868-8969},
  year =	{2009},
  volume =	{4},
  editor =	{Kannan, Ravi and Narayan Kumar, K.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2009.2311},
  URN =		{urn:nbn:de:0030-drops-23111},
  doi =		{10.4230/LIPIcs.FSTTCS.2009.2311},
  annote =	{Keywords: Branching programs, space complexity, tree evaluation, pebbling}
}
  • Refine by Author
  • 3 Cook, Stephen A.
  • 2 Arteche, Noel
  • 2 Santhanam, Rahul
  • 1 Bateni, MohammadHossein
  • 1 Braverman, Mark
  • Show More...

  • Refine by Classification
  • 5 Theory of computation → Proof complexity
  • 2 Theory of computation → Circuit complexity
  • 2 Theory of computation → Complexity theory and logic
  • 1 Theory of computation → Algebraic complexity theory
  • 1 Theory of computation → Computational complexity and cryptography
  • Show More...

  • Refine by Keyword
  • 2 circuit complexity
  • 2 proof complexity
  • 1 AC0- Frege
  • 1 Applications
  • 1 Bounded Arithmetic
  • Show More...

  • Refine by Type
  • 14 document

  • Refine by Publication Year
  • 6 2024
  • 2 2012
  • 2 2013
  • 1 2009
  • 1 2011
  • Show More...

© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact