Document Open Access Logo

Provability of the Circuit Size Hierarchy and Its Consequences

Authors Marco Carmosino, Valentine Kabanets, Antonina Kolokolova, Igor C. Oliveira, Dimitrios Tsintsilidas

PDF
Thumbnail PDF

File

LIPIcs.ITCS.2025.30.pdf
  • Filesize: 0.84 MB
  • 22 pages

Document Identifiers

Author Details

Marco Carmosino
  • IBM Research, Cambridge, MA, USA
Valentine Kabanets
  • Simon Fraser University, Burnaby, Canada
Antonina Kolokolova
  • Memorial University of Newfoundland, St. John, Canada
Igor C. Oliveira
  • University of Warwick, UK
Dimitrios Tsintsilidas
  • University of Warwick, UK

Funding

This work received support from the Royal Society University Research Fellowship URF⧵R1⧵191059; the UKRI Frontier Research Guarantee Grant EP/Y007999/1; the Centre for Discrete Mathematics and its Applications (DIMAP) at the University of Warwick, and the Natural Sciences and Engineering Research Council of Canada.

Acknowledgements

We thank Emil Jeřábek for a discussion about witnessing theorems in bounded arithmetic. We are also grateful to Hanlin Ren for a suggestion that improved our bounds in Corollary 10.

Cite As Get BibTex

Marco Carmosino, Valentine Kabanets, Antonina Kolokolova, Igor C. Oliveira, and Dimitrios Tsintsilidas. Provability of the Circuit Size Hierarchy and Its Consequences. In 16th Innovations in Theoretical Computer Science Conference (ITCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 325, pp. 30:1-30:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.ITCS.2025.30

Abstract

The Circuit Size Hierarchy (CSH^a_b) states that if a > b ≥ 1 then the set of functions on n variables computed by Boolean circuits of size n^a is strictly larger than the set of functions computed by circuits of size n^b. This result, which is a cornerstone of circuit complexity theory, follows from the non-constructive proof of the existence of functions of large circuit complexity obtained by Shannon in 1949. 
Are there more "constructive" proofs of the Circuit Size Hierarchy? Can we quantify this? Motivated by these questions, we investigate the provability of CSH^a_b in theories of bounded arithmetic. Among other contributions, we establish the following results:  
i) Given any a > b > 1, CSH^a_b is provable in Buss’s theory 𝖳²₂. 
ii) In contrast, if there are constants a > b > 1 such that CSH^a_b is provable in the theory 𝖳¹₂, then there is a constant ε > 0 such that 𝖯^NP requires non-uniform circuits of size at least n^{1 + ε}.  In other words, an improved upper bound on the proof complexity of CSH^a_b would lead to new lower bounds in complexity theory. 
We complement these results with a proof of the Formula Size Hierarchy (FSH^a_b) in PV₁ with parameters a > 2 and b = 3/2. This is in contrast with typical formalizations of complexity lower bounds in bounded arithmetic, which require APC₁ or stronger theories and are not known to hold even in 𝖳¹₂.

Subject Classification

ACM Subject Classification
  • Theory of computation → Complexity theory and logic
  • Theory of computation → Proof complexity
  • Theory of computation → Circuit complexity
  • Theory of computation → Proof theory
Keywords
  • Bounded Arithmetic
  • Circuit Complexity
  • Hierarchy Theorems

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

References

  1. Sanjeev Arora and Boaz Barak. Computational Complexity - A Modern Approach. Cambridge University Press, 2009. URL: http://www.cambridge.org/catalogue/catalogue.asp?isbn=9780521424264.
  2. Samuel R. Buss. Bounded Arithmetic. Bibliopolis, 1986. Google Scholar
  3. Samuel R. Buss. Bounded arithmetic and propositional proof complexity. In Logic of Computation, pages 67-121. Springer Berlin Heidelberg, 1997. Google Scholar
  4. Lijie Chen, Jiatu Li, and Igor C. Oliveira. Reverse mathematics of complexity lower bounds. In Symposium on Foundations of Computer Science (FOCS), 2024. Google Scholar
  5. Lijie Chen, Dylan M. McKay, Cody D. Murray, and R. Ryan Williams. Relations and equivalences between circuit lower bounds and Karp-Lipton theorems. In Computational Complexity Conference (CCC), pages 30:1-30:21, 2019. URL: https://doi.org/10.4230/LIPIcs.CCC.2019.30.
  6. Alan Cobham. The intrinsic computational difficulty of functions. Proc. Logic, Methodology and Philosophy of Science, pages 24-30, 1965. Google Scholar
  7. Stephen A. Cook. Feasibly constructive proofs and the propositional calculus (preliminary version). In Symposium on Theory of Computing (STOC), pages 83-97, 1975. URL: https://doi.org/10.1145/800116.803756.
  8. Stephen A. Cook and Phuong Nguyen. Logical Foundations of Proof Complexity. Cambridge University Press, 2010. URL: https://doi.org/10.1017/CBO9780511676277.
  9. Russell Impagliazzo and Avi Wigderson. P = BPP if E requires exponential circuits: Derandomizing the XOR lemma. In Symposium on the Theory of Computing (STOC), pages 220-229, 1997. URL: https://doi.org/10.1145/258533.258590.
  10. Emil Jeřábek. Dual weak pigeonhole principle, boolean complexity, and derandomization. Annals of Pure and Applied Logic, 129(1-3):1-37, 2004. URL: https://doi.org/10.1016/j.apal.2003.12.003.
  11. Emil Jeřábek. Weak pigeonhole principle and randomized computation. PhD thesis, Charles University in Prague, 2005. Google Scholar
  12. Emil Jeřábek. The strength of sharply bounded induction. Mathematical Logic Quarterly, 52(6):613-624, 2006. URL: https://doi.org/10.1002/malq.200610019.
  13. Emil Jeřábek. Approximate counting in bounded arithmetic. Journal of Symbolic Logic, 72(3):959-993, 2007. URL: https://doi.org/10.2178/jsl/1191333850.
  14. Stasys Jukna. Boolean Function Complexity: Advances and Frontiers. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-24508-4.
  15. Ravi Kannan. Circuit-size lower bounds and non-reducibility to sparse sets. Information and Control, 55(1):40-56, 1982. URL: https://doi.org/10.1016/S0019-9958(82)90382-5.
  16. Jan Krajíček. Bounded Arithmetic, Propositional Logic, and Complexity Theory. Encyclopedia of Mathematics and its Applications. Cambridge University Press, 1995. Google Scholar
  17. Jan Krajíček. Small circuits and dual weak PHP in the universal theory of p-time algorithms. ACM Transactions on Computational Logic (TOCL), 22(2):1-4, 2021. URL: https://doi.org/10.1145/3446207.
  18. Jan Krajíček and Igor C. Oliveira. Unprovability of circuit upper bounds in Cook’s theory PV. Logical Methods in Computer Science, 13(1), 2017. URL: https://doi.org/10.23638/LMCS-13(1:4)2017.
  19. Jan Krajíček, Pavel Pudlák, and Gaisi Takeuti. Bounded arithmetic and the polynomial hierarchy. Annals of Pure and Applied Logic, 52(1-2):143-153, 1991. URL: https://doi.org/10.1016/0168-0072(91)90043-L.
  20. Jan Krajíček. Proof Complexity. Encyclopedia of Mathematics and its Applications. Cambridge University Press, 2019. URL: https://doi.org/10.1017/9781108242066.
  21. Alexis Maciel, Toniann Pitassi, and Alan R. Woods. A new proof of the weak pigeonhole principle. Journal of Computer and System Sciences, 64(4):843-872, 2002. URL: https://doi.org/10.1006/jcss.2002.1830.
  22. Moritz Müller and Ján Pich. Feasibly constructive proofs of succinct weak circuit lower bounds. Annals of Pure and Applied Logic, 171(2), 2020. URL: https://doi.org/10.1016/j.apal.2019.102735.
  23. Igor C. Oliveira. Meta-mathematics of computational complexity theory. Preprint, 2024. Google Scholar
  24. Claude E. Shannon. The synthesis of two-terminal switching circuits. The Bell System Technical Journal, 28(1):59-98, 1949. URL: https://doi.org/10.1002/j.1538-7305.1949.tb03624.x.
  25. Bella A. Subbotovskaya. Realization of linear functions by formulas using +, ⋅, -. In Soviet Math. Dokl, 1961. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact