{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:24:46Z","timestamp":1750307086813,"version":"3.41.0"},"reference-count":26,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2012,9,1]],"date-time":"2012-09-01T00:00:00Z","timestamp":1346457600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Theory"],"published-print":{"date-parts":[[2012,9]]},"abstract":"<jats:p>A general framework for parameterized proof complexity was introduced by Dantchev et al. [2007]. There, the authors show important results on tree-like Parameterized Resolution---a parameterized version of classical Resolution---and their gap complexity theorem implies lower bounds for that system.<\/jats:p>\n          <jats:p>\n            The main result of this article significantly improves upon this by showing optimal lower bounds for a parameterized version of bounded-depth Frege. More precisely, we prove that the pigeonhole principle requires proofs of size\n            <jats:italic>n<\/jats:italic>\n            <jats:sup>\u03a9(k)<\/jats:sup>\n            in parameterized bounded-depth Frege, and, as a special case, in dag-like Parameterized Resolution. This answers an open question posed in Dantchev et al. [2007]. In the opposite direction, we interpret a well-known technique for FPT algorithms as a DPLL procedure for Parameterized Resolution. Its generalization leads to a proof search algorithm for Parameterized Resolution that in particular shows that tree-like Parameterized Resolution allows short refutations of all parameterized contradictions given as bounded-width CNFs.\n          <\/jats:p>","DOI":"10.1145\/2355580.2355582","type":"journal-article","created":{"date-parts":[[2012,10,2]],"date-time":"2012-10-02T13:50:00Z","timestamp":1349185800000},"page":"1-16","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":14,"title":["Parameterized Bounded-Depth Frege Is not Optimal"],"prefix":"10.1145","volume":"4","author":[{"given":"Olaf","family":"Beyersdorff","sequence":"first","affiliation":[{"name":"University of Leeds"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nicola","family":"Galesi","sequence":"additional","affiliation":[{"name":"Sapienza University Rome"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Massimo","family":"Lauria","sequence":"additional","affiliation":[{"name":"Sapienza University Rome"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alexander A.","family":"Razborov","sequence":"additional","affiliation":[{"name":"University of Chicago"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2012,9]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1137\/06066850X"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539700369156"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00037-007-0230-0"},{"key":"e_1_2_1_4_1","volume-title":"Proceedings of the 14th International Conference on Theory and Applications of Satisfiability Testing. Lecture Notes in Computer Science","volume":"6695","author":"Beyersdorff O.","unstructured":"Beyersdorff , O. , Galesi , N. , and Lauria , M . 2011a. Parameterized complexity of DPLL search procedures . In Proceedings of the 14th International Conference on Theory and Applications of Satisfiability Testing. Lecture Notes in Computer Science , vol. 6695 , Springer-Verlag, Berlin, 5--18. Beyersdorff, O., Galesi, N., and Lauria, M. 2011a. Parameterized complexity of DPLL search procedures. In Proceedings of the 14th International Conference on Theory and Applications of Satisfiability Testing. Lecture Notes in Computer Science, vol. 6695, Springer-Verlag, Berlin, 5--18."},{"key":"e_1_2_1_5_1","volume-title":"Proceedings of the 38th International Colloquium on Automata, Languages, and Programming. Lecture Notes in Computer Science","volume":"6755","author":"Beyersdorff O.","unstructured":"Beyersdorff , O. , Galesi , N. , Lauria , M. , and Razborov , A . 2011b. Parameterized bounded-depth Frege is not optimal . In Proceedings of the 38th International Colloquium on Automata, Languages, and Programming. Lecture Notes in Computer Science , vol. 6755 , Springer-Verlag, Berlin, 630--641. Beyersdorff, O., Galesi, N., Lauria, M., and Razborov, A. 2011b. Parameterized bounded-depth Frege is not optimal. In Proceedings of the 38th International Colloquium on Automata, Languages, and Programming. Lecture Notes in Computer Science, vol. 6755, Springer-Verlag, Berlin, 630--641."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/s000370100000"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.2307\/2275569"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.2307\/2273826"},{"key":"e_1_2_1_9_1","doi-asserted-by":"crossref","unstructured":"Buss S. R. and Pitassi T. 1997. Resolution and the weak pigeonhole principle. Comput. Sci. Logic. 149--156. Buss S. R. and Pitassi T. 1997. Resolution and the weak pigeonhole principle. Comput. Sci. Logic . 149--156.","DOI":"10.1007\/BFb0028012"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2007.09.003"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.2307\/2273702"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/FOCS.2007.52"},{"key":"e_1_2_1_13_1","doi-asserted-by":"crossref","unstructured":"Downey R. G. and Fellows M. R. 1999. Parameterized Complexity. Springer-Verlag Berlin. Downey R. G. and Fellows M. R. 1999. Parameterized Complexity . Springer-Verlag Berlin.","DOI":"10.1007\/978-1-4612-0515-9"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/CCC.2008.24"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00161-5"},{"key":"e_1_2_1_16_1","unstructured":"Flum J. and Grohe M. 2006. Parameterized Complexity Theory. Springer-Verlag Berlin Heidelberg. Flum J. and Grohe M. 2006. Parameterized Complexity Theory . Springer-Verlag Berlin Heidelberg."},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.artint.2009.06.005"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(85)90144-6"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1002\/rsa.3240070103"},{"volume-title":"Invitation to Fixed-Parameter Algorithms. Oxford Lecture Series in Mathematics and Its Applications","author":"Niedermeier R.","key":"e_1_2_1_20_1","unstructured":"Niedermeier , R. 2006. Invitation to Fixed-Parameter Algorithms. Oxford Lecture Series in Mathematics and Its Applications , Oxford University Press . Niedermeier, R. 2006. Invitation to Fixed-Parameter Algorithms. Oxford Lecture Series in Mathematics and Its Applications, Oxford University Press."},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01200117"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.2307\/2275583"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/972639.972640"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00493-002-0007-7"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jcss.2004.01.004"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00037-001-8194-y"}],"container-title":["ACM Transactions on Computation Theory"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2355580.2355582","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2355580.2355582","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T09:34:24Z","timestamp":1750239264000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2355580.2355582"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,9]]},"references-count":26,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2012,9]]}},"alternative-id":["10.1145\/2355580.2355582"],"URL":"https:\/\/doi.org\/10.1145\/2355580.2355582","relation":{},"ISSN":["1942-3454","1942-3462"],"issn-type":[{"type":"print","value":"1942-3454"},{"type":"electronic","value":"1942-3462"}],"subject":[],"published":{"date-parts":[[2012,9]]},"assertion":[{"value":"2011-09-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2012-07-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2012-09-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}