{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,10]],"date-time":"2026-06-10T07:58:11Z","timestamp":1781078291082,"version":"3.54.1"},"publisher-location":"New York, NY, USA","reference-count":37,"publisher":"ACM","license":[{"start":{"date-parts":[[2023,6,2]],"date-time":"2023-06-02T00:00:00Z","timestamp":1685664000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100011033","name":"Agencia Estatal de Investigación","doi-asserted-by":"publisher","award":["PID2019-109137GB-C22 (PROOFS), CEX2020-001084-M"],"award-info":[{"award-number":["PID2019-109137GB-C22 (PROOFS), CEX2020-001084-M"]}],"id":[{"id":"10.13039\/501100011033","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2023,6,2]]},"DOI":"10.1145\/3564246.3585253","type":"proceedings-article","created":{"date-parts":[[2023,5,16]],"date-time":"2023-05-16T17:34:20Z","timestamp":1684258460000},"page":"1257-1270","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["On the Consistency of Circuit Lower Bounds for Non-deterministic Time"],"prefix":"10.1145","author":[{"given":"Albert","family":"Atserias","sequence":"first","affiliation":[{"name":"Universitat Polit\u00e8cnica de Catalunya, Spain \/ Centre de Recerca Matem\u00e0tica, Spain"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Sam","family":"Buss","sequence":"additional","affiliation":[{"name":"University of California at San Diego, San Diego, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Moritz","family":"M\u00fcller","sequence":"additional","affiliation":[{"name":"University of Passau, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2023,6,2]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1988.21951"},{"key":"e_1_3_2_1_2_1","volume-title":"Partially definable forcing and bounded arithmetic. Archive for Mathematical Logic 54 ( 1 ): 1-33","author":"Atserias A.","year":"2015","unstructured":"A. Atserias , M. M\u00fcller . Partially definable forcing and bounded arithmetic. Archive for Mathematical Logic 54 ( 1 ): 1-33 , 2015 . A. Atserias, M. M\u00fcller. Partially definable forcing and bounded arithmetic. Archive for Mathematical Logic 54 ( 1 ): 1-33, 2015."},{"key":"e_1_3_2_1_3_1","first-page":"200","volume-title":"Proceedings of the ACM Symposium on Theory of Computing (STOC'92)","author":"Beame P.","year":"1992","unstructured":"P. Beame , R. Impagliazzo , J. Kraj\u00ed\u010dek , T. Pitassi , P. Pudl\u00e1k , A. Woods . Exponential lower bound for the pigeonhole principle (extended abstract) . Proceedings of the ACM Symposium on Theory of Computing (STOC'92) , ACM Press , pp. 200 - 220 , 1992 . P. Beame, R. Impagliazzo, J. Kraj\u00ed\u010dek, T. Pitassi, P. Pudl\u00e1k, A. Woods. Exponential lower bound for the pigeonhole principle (extended abstract). Proceedings of the ACM Symposium on Theory of Computing (STOC'92), ACM Press, pp. 200-220, 1992."},{"key":"e_1_3_2_1_4_1","first-page":"2","author":"Beckmann A.","year":"2014","unstructured":"A. Beckmann , S. R. Buss . Improved witnessing and local improvement principles for second-order bounded arithmetic. ACM Transactions on Computational Logic 15 ( 1 ) : Article 2 , 2014 . A. Beckmann, S. R. Buss. Improved witnessing and local improvement principles for second-order bounded arithmetic. ACM Transactions on Computational Logic 15 ( 1 ): Article 2, 2014.","journal-title":"Article"},{"key":"e_1_3_2_1_5_1","unstructured":"S. R. Buss. Bounded Arithmetic. Bibliopolis Naples 1986. \t\t\t\t  S. R. Buss. Bounded Arithmetic. Bibliopolis Naples 1986."},{"key":"e_1_3_2_1_6_1","volume-title":"Polynomial time ultrapowers and the consistency of circuit lower bounds. Archive for Mathematical Logic 59 ( 1 ): 127-147","author":"Bydzovsky J.","year":"2020","unstructured":"J. Bydzovsky , M. M\u00fcller . Polynomial time ultrapowers and the consistency of circuit lower bounds. Archive for Mathematical Logic 59 ( 1 ): 127-147 , 2020 . J. Bydzovsky, M. M\u00fcller. Polynomial time ultrapowers and the consistency of circuit lower bounds. Archive for Mathematical Logic 59 ( 1 ): 127-147, 2020."},{"key":"e_1_3_2_1_7_1","volume-title":"Consistency of circuit lower bounds with bounded theories. Logical Methods in Computer Science 16 ( 2 )","author":"Bydzovsky J.","year":"2020","unstructured":"J. Bydzovsky , J. Kraj\u00ed\u010dek , I. C. Oliveira . Consistency of circuit lower bounds with bounded theories. Logical Methods in Computer Science 16 ( 2 ) , 2020 . J. Bydzovsky, J. Kraj\u00ed\u010dek, I. C. Oliveira. Consistency of circuit lower bounds with bounded theories. Logical Methods in Computer Science 16 ( 2 ), 2020."},{"key":"e_1_3_2_1_8_1","first-page":"770","volume-title":"Proceedings of the 62nd Annual Symposium on Foundations of Computer Science (FOCS'21)","author":"Carmosino M.","year":"2021","unstructured":"M. Carmosino , V. Kabanets , A. Kolokolova , I. C. Oliveira . LEARN-uniform circuit lower bounds and provability in bounded arithmetic . Proceedings of the 62nd Annual Symposium on Foundations of Computer Science (FOCS'21) , pp. 770 - 780 , 2021 . M. Carmosino, V. Kabanets, A. Kolokolova, I. C. Oliveira. LEARN-uniform circuit lower bounds and provability in bounded arithmetic. Proceedings of the 62nd Annual Symposium on Foundations of Computer Science (FOCS'21), pp. 770-780, 2021."},{"key":"e_1_3_2_1_9_1","first-page":"1","volume":"151","author":"Chen L.","year":"2020","unstructured":"L. Chen , S. Hirahara , I. C. Oliveira , J. Pich , N. Rajgopal , R. Santhanam . Beyond natural proofs: hardness magnification and locality. Proceedings of the 11th Innovations in Theoretical Computer Science (ITCS'20) , LIPIcs 151 , pp. 70 : 1 - 70 : 48, 2020 . L. Chen, S. Hirahara, I. C. Oliveira, J. Pich, N. Rajgopal, R. Santhanam. Beyond natural proofs: hardness magnification and locality. Proceedings of the 11th Innovations in Theoretical Computer Science (ITCS'20), LIPIcs 151, pp. 70 : 1-70 : 48, 2020.","journal-title":"LIPIcs"},{"key":"e_1_3_2_1_10_1","volume-title":"Consequences of the Provability of NP \u2286 P\/poly. Journal of Symbolic Logic 72 ( 4 ): 1353-1371","author":"Cook S. A.","year":"2007","unstructured":"S. A. Cook , J. Kraj\u00ed\u010dek . Consequences of the Provability of NP \u2286 P\/poly. Journal of Symbolic Logic 72 ( 4 ): 1353-1371 , 2007 . S. A. Cook, J. Kraj\u00ed\u010dek. Consequences of the Provability of NP \u2286 P\/poly. Journal of Symbolic Logic 72 ( 4 ): 1353-1371, 2007."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.5555\/1734064"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01744431"},{"key":"e_1_3_2_1_13_1","volume-title":"Metamathematics of First-Order Arithmetic. Perspectives in Mathematical Logic","author":"H\u00e1jek P.","year":"1998","unstructured":"P. H\u00e1jek , P. Pudl\u00e1k . Metamathematics of First-Order Arithmetic. Perspectives in Mathematical Logic , Springer , 1998 . P. H\u00e1jek, P. Pudl\u00e1k. Metamathematics of First-Order Arithmetic. Perspectives in Mathematical Logic, Springer, 1998."},{"key":"e_1_3_2_1_14_1","volume-title":"search of an easy witness: exponential time vs. probabilistic polynomial time. Journal of Computer and System Sciences 65 ( 4 ): 672-694","author":"Impagliazzo R.","year":"2002","unstructured":"R. Impagliazzo , V. Kabanets , A. Wigderson . In search of an easy witness: exponential time vs. probabilistic polynomial time. Journal of Computer and System Sciences 65 ( 4 ): 672-694 , 2002 . R. Impagliazzo, V. Kabanets, A. Wigderson. In search of an easy witness: exponential time vs. probabilistic polynomial time. Journal of Computer and System Sciences 65 ( 4 ): 672-694, 2002."},{"key":"e_1_3_2_1_15_1","volume-title":"Boolean complexity, and derandomization. Annals of Pure and Applied Logic 129 : 1-37","author":"Je\u0159\u00e1bek E.","year":"2004","unstructured":"E. Je\u0159\u00e1bek . Dual weak pigeonhole principle , Boolean complexity, and derandomization. Annals of Pure and Applied Logic 129 : 1-37 , 2004 . E. Je\u0159\u00e1bek. Dual weak pigeonhole principle, Boolean complexity, and derandomization. Annals of Pure and Applied Logic 129 : 1-37, 2004."},{"key":"e_1_3_2_1_17_1","volume-title":"Approximate counting in bounded arithmetic. Journal of Symbolic Logic 72 ( 3 ): 959-993","author":"Je\u0159\u00e1bek E.","year":"2007","unstructured":"E. Je\u0159\u00e1bek . Approximate counting in bounded arithmetic. Journal of Symbolic Logic 72 ( 3 ): 959-993 , 2007 . E. Je\u0159\u00e1bek. Approximate counting in bounded arithmetic. Journal of Symbolic Logic 72 ( 3 ): 959-993, 2007."},{"key":"e_1_3_2_1_18_1","volume-title":"Circuit-size lower bounds and non-reducibility to sparse sets. Information and Control 55 ( 1-3 ): 40-56","author":"Kannan R.","year":"1982","unstructured":"R. Kannan . Circuit-size lower bounds and non-reducibility to sparse sets. Information and Control 55 ( 1-3 ): 40-56 , 1982 . R. Kannan. Circuit-size lower bounds and non-reducibility to sparse sets. Information and Control 55 ( 1-3 ): 40-56, 1982."},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/800141.804678"},{"key":"e_1_3_2_1_20_1","volume-title":"Exponentiation and second order bounded arithmetic. Annals of Pure and Applied Logic 48 ( 3 ): 261-276","author":"Kraj\u00ed\u010dek J.","year":"1990","unstructured":"J. Kraj\u00ed\u010dek . Exponentiation and second order bounded arithmetic. Annals of Pure and Applied Logic 48 ( 3 ): 261-276 , 1990 . J. Kraj\u00ed\u010dek. Exponentiation and second order bounded arithmetic. Annals of Pure and Applied Logic 48 ( 3 ): 261-276, 1990."},{"key":"e_1_3_2_1_21_1","first-page":"287","volume":"21","author":"Kraj\u00ed\u010dek J.","year":"1992","unstructured":"J. Kraj\u00ed\u010dek . No counter-example interpretation and interactive computation. In: Logic from Computer Science , ed. Y. N. Moschovakis , Mathematical Sciences Research Institute Publ. 21 , Springer, pp. 287 - 293 , 1992 . J. Kraj\u00ed\u010dek. No counter-example interpretation and interactive computation. In: Logic from Computer Science, ed. Y. N. Moschovakis, Mathematical Sciences Research Institute Publ. 21, Springer, pp. 287-293, 1992.","journal-title":"Publ."},{"key":"e_1_3_2_1_22_1","volume-title":"Propositional Logic, and Complexity Theory. Encyclopedia of Mathematics and Its Applications 60","author":"Kraj\u00ed\u010dek J.","year":"1995","unstructured":"J. Kraj\u00ed\u010dek . Bounded Arithmetic , Propositional Logic, and Complexity Theory. Encyclopedia of Mathematics and Its Applications 60 , Cambridge University Press , 1995 . J. Kraj\u00ed\u010dek. Bounded Arithmetic, Propositional Logic, and Complexity Theory. Encyclopedia of Mathematics and Its Applications 60, Cambridge University Press, 1995."},{"key":"e_1_3_2_1_23_1","volume-title":"Forcing with random variables and proof complexity","author":"Kraj\u00ed\u010dek J.","year":"2011","unstructured":"J. Kraj\u00ed\u010dek . Forcing with random variables and proof complexity , London Mathematical Society Lecture Note Series, No .382, Cambridge University Press , 2011 . J. Kraj\u00ed\u010dek. Forcing with random variables and proof complexity, London Mathematical Society Lecture Note Series, No.382, Cambridge University Press, 2011."},{"key":"e_1_3_2_1_24_1","volume-title":"Unprovability of circuit upper bounds in Cook's theory PV. Logical Methods in Computer Science 13 ( 1 )","author":"Kraj\u00ed\u010dek J.","year":"2017","unstructured":"J. Kraj\u00ed\u010dek , I. C. Oliveira . Unprovability of circuit upper bounds in Cook's theory PV. Logical Methods in Computer Science 13 ( 1 ) , 2017 . J. Kraj\u00ed\u010dek, I. C. Oliveira. Unprovability of circuit upper bounds in Cook's theory PV. Logical Methods in Computer Science 13 ( 1 ), 2017."},{"key":"e_1_3_2_1_25_1","volume-title":"NP search problems and an extension of a theorem of Riis. Annals of Pure and Applied Logic 172 ( 4 ): 102930","author":"M\u00fcller M.","year":"2021","unstructured":"M. M\u00fcller . Typical forcing , NP search problems and an extension of a theorem of Riis. Annals of Pure and Applied Logic 172 ( 4 ): 102930 , 2021 . M. M\u00fcller. Typical forcing, NP search problems and an extension of a theorem of Riis. Annals of Pure and Applied Logic 172 ( 4 ): 102930, 2021."},{"key":"e_1_3_2_1_26_1","first-page":"102735","volume":"172","author":"M\u00fcller M.","year":"2020","unstructured":"M. M\u00fcller , J. Pich. Feasibly constructive proofs of succinct weak circuit lower bounds. Annals of Pure and Applied Logic 172 ( 2 ): Article 102735 , 2020 . M. M\u00fcller, J. Pich. Feasibly constructive proofs of succinct weak circuit lower bounds. Annals of Pure and Applied Logic 172 ( 2 ): Article 102735, 2020.","journal-title":"J. Pich. Feasibly constructive proofs of succinct weak circuit lower bounds. Annals of Pure and Applied Logic"},{"key":"e_1_3_2_1_27_1","first-page":"65","volume-title":"Proceedings of the 59th Symposium on Foundations of Computer Science (FOCS'18)","author":"Oliveira I. C.","year":"2018","unstructured":"I. C. Oliveira , R. Santhanam . Hardness magnification for natural problems . Proceedings of the 59th Symposium on Foundations of Computer Science (FOCS'18) , pp. 65 - 76 , 2018 . I. C. Oliveira, R. Santhanam. Hardness magnification for natural problems. Proceedings of the 59th Symposium on Foundations of Computer Science (FOCS'18), pp. 65-76, 2018."},{"key":"e_1_3_2_1_28_1","volume-title":"Annals of Pure and Applied Logic 166 ( 1 ): 29-45","author":"Pich J.","year":"2015","unstructured":"J. Pich . Circuit lower bounds in bounded arithmetics. Annals of Pure and Applied Logic 166 ( 1 ): 29-45 , 2015 . J. Pich. Circuit lower bounds in bounded arithmetics. Annals of Pure and Applied Logic 166 ( 1 ): 29-45, 2015."},{"key":"e_1_3_2_1_29_1","volume-title":"Logical Methods in Computer Science 11 ( 2 )","author":"Pich J.","year":"2015","unstructured":"J. Pich . Logical strength of complexity theory and a formalization of the PCP theorem in bounded arithmetic. Logical Methods in Computer Science 11 ( 2 ) , 2015 . J. Pich. Logical strength of complexity theory and a formalization of the PCP theorem in bounded arithmetic. Logical Methods in Computer Science 11 ( 2 ), 2015."},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3406325.3451117"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-2566-9_12"},{"key":"e_1_3_2_1_32_1","volume-title":"Unprovability of lower bounds on the circuit size in certain fragments of bounded arithmetic. Izvestiya of the Russian Academy of Science 59 : 201-224","author":"Razborov A. A.","year":"1995","unstructured":"A. A. Razborov . Unprovability of lower bounds on the circuit size in certain fragments of bounded arithmetic. Izvestiya of the Russian Academy of Science 59 : 201-224 , 1995 . A. A. Razborov. Unprovability of lower bounds on the circuit size in certain fragments of bounded arithmetic. Izvestiya of the Russian Academy of Science 59 : 201-224, 1995."},{"key":"e_1_3_2_1_33_1","volume-title":"Pseudorandom generators hard for k-DNF resolution and polynomial calculus. Annals of Mathematics 181 ( 2 ): 415-472","author":"Razborov A. A.","year":"2015","unstructured":"A. A. Razborov . Pseudorandom generators hard for k-DNF resolution and polynomial calculus. Annals of Mathematics 181 ( 2 ): 415-472 , 2015 . A. A. Razborov. Pseudorandom generators hard for k-DNF resolution and polynomial calculus. Annals of Mathematics 181 ( 2 ): 415-472, 2015."},{"key":"e_1_3_2_1_34_1","volume-title":"BRICS Report Series, RS-94-23","author":"Riis S.","year":"1994","unstructured":"S. Riis . Finitization in bounded arithmetic. Basic Research in Computer Science , BRICS Report Series, RS-94-23 , 1994 . S. Riis. Finitization in bounded arithmetic. Basic Research in Computer Science, BRICS Report Series, RS-94-23, 1994."},{"key":"e_1_3_2_1_35_1","volume-title":"On uniformity and circuit lower bounds. Computational Complexity 23 ( 2 ): 177-205","author":"Santhanam R.","year":"2014","unstructured":"R. Santhanam , R. Williams . On uniformity and circuit lower bounds. Computational Complexity 23 ( 2 ): 177-205 , 2014 . R. Santhanam, R. Williams. On uniformity and circuit lower bounds. Computational Complexity 23 ( 2 ): 177-205, 2014."},{"key":"e_1_3_2_1_36_1","volume-title":"Bounded arithmetic and truth definition. Annals of Pure and Applied Logic 39 : 75-104","author":"Takeuti G.","year":"1988","unstructured":"G. Takeuti . Bounded arithmetic and truth definition. Annals of Pure and Applied Logic 39 : 75-104 , 1988 . G. Takeuti. Bounded arithmetic and truth definition. Annals of Pure and Applied Logic 39 : 75-104, 1988."},{"key":"e_1_3_2_1_37_1","series-title":"SIAM Journal on Computing 42 ( 3 ): 1218-1244","volume-title":"Improving exhaustive search implies superpolynomial lower bounds","author":"Williams R.","year":"2013","unstructured":"R. Williams . Improving exhaustive search implies superpolynomial lower bounds . SIAM Journal on Computing 42 ( 3 ): 1218-1244 , 2013 . R. Williams. Improving exhaustive search implies superpolynomial lower bounds. SIAM Journal on Computing 42 ( 3 ): 1218-1244, 2013."},{"key":"e_1_3_2_1_38_1","series-title":"SIAM Journal on Computing 45 ( 2 ): 497-529","volume-title":"Natural proofs versus derandomization","author":"Williams R.","year":"2016","unstructured":"R. Williams . Natural proofs versus derandomization . SIAM Journal on Computing 45 ( 2 ): 497-529 , 2016 . R. Williams. Natural proofs versus derandomization. SIAM Journal on Computing 45 ( 2 ): 497-529, 2016."}],"event":{"name":"STOC '23: 55th Annual ACM Symposium on Theory of Computing","location":"Orlando FL USA","acronym":"STOC '23","sponsor":["SIGACT ACM Special Interest Group on Algorithms and Computation Theory"]},"container-title":["Proceedings of the 55th Annual ACM Symposium on Theory of Computing"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3564246.3585253","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3564246.3585253","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:47:02Z","timestamp":1750178822000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3564246.3585253"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,6,2]]},"references-count":37,"alternative-id":["10.1145\/3564246.3585253","10.1145\/3564246"],"URL":"https:\/\/doi.org\/10.1145\/3564246.3585253","relation":{},"subject":[],"published":{"date-parts":[[2023,6,2]]},"assertion":[{"value":"2023-06-02","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}