{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T00:51:44Z","timestamp":1740099104220,"version":"3.37.3"},"publisher-location":"Cham","reference-count":53,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319944173"},{"type":"electronic","value":"9783319944180"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-94418-0_26","type":"book-chapter","created":{"date-parts":[[2018,7,4]],"date-time":"2018-07-04T16:38:26Z","timestamp":1530722306000},"page":"254-263","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Algorithm Analysis Through Proof Complexity"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4003-3168","authenticated-orcid":false,"given":"Massimo","family":"Lauria","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,7,3]]},"reference":[{"issue":"2","key":"26_CR1","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/BF01204715","volume":"12","author":"N Alon","year":"1992","unstructured":"Alon, N., Tarsi, M.: Colorings and orientations of graphs. Combinatorica 12(2), 125\u2013134 (1992)","journal-title":"Combinatorica"},{"key":"26_CR2","doi-asserted-by":"crossref","unstructured":"Atserias, A., Bonacina, I., de Rezende, S.F., Lauria, M., Nordstr\u00f6m, J., Razborov, A.A.: Clique is hard on average for regular resolution. In: Proceedings of the 50th Annual ACM Symposium on Theory of Computing (STOC 2008) (2018, to appear)","DOI":"10.1145\/3188745.3188856"},{"key":"26_CR3","unstructured":"Atserias, A., Ochremiak, J.: Proof complexity meets algebra. In: ICALP 2017. Leibniz International Proceedings in Informatics (LIPIcs), vol. 80, pp. 110:1\u2013110:14. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Dagstuhl (2017)"},{"key":"26_CR4","unstructured":"Bayer, D.A.: The division algorithm and the Hilbert scheme. Ph.D. thesis, Harvard University, Cambridge, MA, USA, June 1982. https:\/\/www.math.columbia.edu\/~bayer\/papers\/Bayer-thesis.pdf"},{"issue":"1\u20133","key":"26_CR5","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1016\/j.dam.2005.05.004","volume":"153","author":"P Beame","year":"2005","unstructured":"Beame, P., Culberson, J.C., Mitchell, D.G., Moore, C.: The resolution complexity of random graph $$k$$-colorability. Discrete Appl. Math. 153(1\u20133), 25\u201347 (2005)","journal-title":"Discrete Appl. Math."},{"key":"26_CR6","doi-asserted-by":"crossref","unstructured":"Beame, P., Impagliazzo, R., Kraj\u00ed\u010dek, J., Pitassi, T., Pudl\u00e1k, P.: Lower bounds on Hilbert\u2019s Nullstellensatz and propositional proofs. In: Proceedings of the 35th Annual IEEE Symposium on Foundations of Computer Science (FOCS 1994), pp. 794\u2013806, November 1994","DOI":"10.1109\/SFCS.1994.365714"},{"issue":"3","key":"26_CR7","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/s00037-007-0230-0","volume":"16","author":"P Beame","year":"2007","unstructured":"Beame, P., Impagliazzo, R., Sabharwal, A.: The resolution complexity of independent sets and vertex covers in random graphs. Comput. Complex. 16(3), 245\u2013297 (2007)","journal-title":"Comput. Complex."},{"key":"26_CR8","unstructured":"Beame, P., Pitassi, T.: Propositional proof complexity: past, present, and future. In: Current Trends in Theoretical Computer Science, pp. 42\u201370. World Scientific Publishing (2001)"},{"issue":"2","key":"26_CR9","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1016\/j.jalgor.2004.06.008","volume":"54","author":"R Beigel","year":"2005","unstructured":"Beigel, R., Eppstein, D.: 3-coloring in time $$O(1. 3289^n)$$. J. Algorithms 54(2), 168\u2013204 (2005)","journal-title":"J. Algorithms"},{"issue":"3","key":"26_CR10","doi-asserted-by":"publisher","first-page":"20:1","DOI":"10.1145\/2499937.2499941","volume":"14","author":"O Beyersdorff","year":"2013","unstructured":"Beyersdorff, O., Galesi, N., Lauria, M.: Parameterized complexity of DPLL search procedures. ACM Trans. Comput. Log. 14(3), 20:1\u201320:21 (2013). Preliminary version in SAT 2011","journal-title":"ACM Trans. Comput. Log."},{"key":"26_CR11","doi-asserted-by":"crossref","unstructured":"Blake, A.: Canonical expressions in Boolean algebra. Ph.D. thesis, University of Chicago (1938)","DOI":"10.2307\/2267595"},{"issue":"9","key":"26_CR12","doi-asserted-by":"publisher","first-page":"575","DOI":"10.1145\/362342.362367","volume":"16","author":"C Bron","year":"1973","unstructured":"Bron, C., Kerbosch, J.: Algorithm 457: finding all cliques of an undirected graph. Commun. ACM 16(9), 575\u2013577 (1973)","journal-title":"Commun. ACM"},{"issue":"3\u20134","key":"26_CR13","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1007\/s00037-002-0171-6","volume":"11","author":"J Buresh-Oppenheim","year":"2002","unstructured":"Buresh-Oppenheim, J., Clegg, M., Impagliazzo, R., Pitassi, T.: Homogenization and the polynomial calculus. Comput. Complex. 11(3\u20134), 91\u2013108 (2002). Preliminary version in ICALP 2000","journal-title":"Comput. Complex."},{"issue":"4","key":"26_CR14","doi-asserted-by":"publisher","first-page":"643","DOI":"10.1137\/0206046","volume":"6","author":"V Chv\u00e1tal","year":"1977","unstructured":"Chv\u00e1tal, V.: Determining the stability number of a graph. SIAM J. Comput. 6(4), 643\u2013662 (1977)","journal-title":"SIAM J. Comput."},{"key":"26_CR15","doi-asserted-by":"crossref","unstructured":"Clegg, M., Edmonds, J., Impagliazzo, R.: Using the Groebner basis algorithm to find proofs of unsatisfiability. In: Proceedings of the 28th Annual ACM Symposium on Theory of Computing (STOC 1996), pp. 174\u2013183, May 1996","DOI":"10.1145\/237814.237860"},{"key":"26_CR16","doi-asserted-by":"crossref","unstructured":"Cook, S.A.: The complexity of theorem proving procedures. In: Proceedings of the 3rd Annual ACM Symposium on Theory of Computing (STOC 1971), pp. 151\u2013158 (1971)","DOI":"10.1145\/800157.805047"},{"key":"26_CR17","doi-asserted-by":"publisher","first-page":"36","DOI":"10.2307\/2273702","volume":"44","author":"SA Cook","year":"1979","unstructured":"Cook, S.A., Reckhow, R.A.: The relative efficiency of propositional proof systems. J. Symb. Log. 44, 36\u201350 (1979)","journal-title":"J. Symb. Log."},{"issue":"1","key":"26_CR18","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1016\/0166-218X(87)90039-4","volume":"18","author":"W Cook","year":"1987","unstructured":"Cook, W., Coullard, C.R., Tur\u00e1n, G.: On the complexity of cutting-plane proofs. Discrete Appl. Math. 18(1), 25\u201338 (1987)","journal-title":"Discrete Appl. Math."},{"key":"26_CR19","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-387-35651-8","volume-title":"Ideals, Varieties, and Algorithms: An Introduction to Computational Algebraic Geometry and Commutative Algebra","author":"D Cox","year":"2007","unstructured":"Cox, D., Little, J., O\u2019Shea, D.: Ideals, Varieties, and Algorithms: An Introduction to Computational Algebraic Geometry and Commutative Algebra, 3rd edn. Springer, New York (2007). https:\/\/doi.org\/10.1007\/978-0-387-35651-8","edition":"3"},{"issue":"1","key":"26_CR20","first-page":"89","volume":"36","author":"JA Loera De","year":"1995","unstructured":"De Loera, J.A.: Gr\u00f6bner bases and graph colorings. Beitr\u00e4ge zur Algebra und Geometrie 36(1), 89\u201396 (1995). https:\/\/www.emis.de\/journals\/BAG\/vol.36\/no.1\/","journal-title":"Beitr\u00e4ge zur Algebra und Geometrie"},{"key":"26_CR21","doi-asserted-by":"crossref","unstructured":"De Loera, J.A., Margulies, S., Pernpeintner, M., Riedl, E., Rolnick, D., Spencer, G., Stasi, D., Swenson, J.: Graph-coloring ideals: Nullstellensatz certificates, Gr\u00f6bner bases for chordal graphs, and hardness of Gr\u00f6bner bases. In: Proceedings of the 40th International Symposium on Symbolic and Algebraic Computation (ISSAC 2015), pp. 133\u2013140, July 2015","DOI":"10.1145\/2755996.2756639"},{"key":"26_CR22","doi-asserted-by":"crossref","unstructured":"De Loera, J.A., Lee, J., Malkin, P.N., Margulies, S.: Hilbert\u2019s Nullstellensatz and an algorithm for proving combinatorial infeasibility. In: Proceedings of the 21st International Symposium on Symbolic and Algebraic Computation (ISSAC 2008), pp. 197\u2013206, July 2008","DOI":"10.1145\/1390768.1390797"},{"issue":"11","key":"26_CR23","doi-asserted-by":"publisher","first-page":"1260","DOI":"10.1016\/j.jsc.2011.08.007","volume":"46","author":"JA Loera De","year":"2011","unstructured":"De Loera, J.A., Lee, J., Malkin, P.N., Margulies, S.: Computing infeasibility certificates for combinatorial problems through Hilbert\u2019s Nullstellensatz. J. Symb. Comput. 46(11), 1260\u20131283 (2011)","journal-title":"J. Symb. Comput."},{"issue":"04","key":"26_CR24","doi-asserted-by":"publisher","first-page":"551","DOI":"10.1017\/S0963548309009894","volume":"18","author":"JA Loera De","year":"2009","unstructured":"De Loera, J.A., Lee, J., Margulies, S., Onn, S.: Expressing combinatorial problems by systems of polynomial equations and Hilbert\u2019s Nullstellensatz. Comb. Probab. Comput. 18(04), 551\u2013582 (2009)","journal-title":"Comb. Probab. Comput."},{"issue":"2","key":"26_CR25","doi-asserted-by":"publisher","first-page":"491","DOI":"10.1007\/s00224-009-9195-5","volume":"47","author":"N Galesi","year":"2010","unstructured":"Galesi, N., Lauria, M.: On the automatizability of polynomial calculus. Theory Comput. Syst. 47(2), 491\u2013506 (2010)","journal-title":"Theory Comput. Syst."},{"issue":"1","key":"26_CR26","doi-asserted-by":"publisher","first-page":"4:1","DOI":"10.1145\/1838552.1838556","volume":"12","author":"N Galesi","year":"2010","unstructured":"Galesi, N., Lauria, M.: Optimality of size-degree trade-offs for polynomial calculus. ACM Trans. Comput. Log. 12(1), 4:1\u20134:22 (2010)","journal-title":"ACM Trans. Comput. Log."},{"key":"26_CR27","first-page":"7","volume-title":"Arithmetic, Proof Theory, and Computational Complexity","author":"K G\u00f6del","year":"1993","unstructured":"G\u00f6del, K.: Ein brief an Johann von Neumann, 20. M\u00e4rz, 1956. In: Clote, P., Kraj\u00ed\u010dek, J. (eds.) Arithmetic, Proof Theory, and Computational Complexity, pp. 7\u20139. Oxford University Press, Oxford (1993)"},{"key":"26_CR28","first-page":"116","volume":"10","author":"G Haj\u00f3s","year":"1961","unstructured":"Haj\u00f3s, G.: \u00dcver eine konstruktion nicht n-farbbarer graphen. Wissenschaftliche Zeitschrift der Martin-Luther-Universitat Halle-Wittenberg, A 10, 116\u2013117 (1961)","journal-title":"Wissenschaftliche Zeitschrift der Martin-Luther-Universitat Halle-Wittenberg, A"},{"key":"26_CR29","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1016\/0304-3975(85)90144-6","volume":"39","author":"A Haken","year":"1985","unstructured":"Haken, A.: The intractability of resolution. Theoret. Comput. Sci. 39, 297\u2013308 (1985)","journal-title":"Theoret. Comput. Sci."},{"issue":"2","key":"26_CR30","doi-asserted-by":"publisher","first-page":"400","DOI":"10.1016\/j.jctb.2007.08.004","volume":"98","author":"CJ Hillar","year":"2008","unstructured":"Hillar, C.J., Windfeldt, T.: Algebraic characterization of uniquely vertex colorable graphs. J. Comb. Theory Ser. B 98(2), 400\u2013414 (2008)","journal-title":"J. Comb. Theory Ser. B"},{"key":"26_CR31","doi-asserted-by":"crossref","unstructured":"Husfeldt, T.: Graph colouring algorithms. In: Beineke, L.W., Wilson, R.J. (eds.) Topics in Chromatic Graph Theory, Encyclopedia of Mathematics and its Applications, pp. 277\u2013303. Cambridge University Press, May 2015. Chap. 13","DOI":"10.1017\/CBO9781139519793.016"},{"key":"26_CR32","series-title":"Encyclopedia of Mathematics and its Applications","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511529948","volume-title":"Bounded Arithmetic, Propositional Logic, and Complexity Theory","author":"J Kraj\u00ed\u010dek","year":"1995","unstructured":"Kraj\u00ed\u010dek, J.: Bounded Arithmetic, Propositional Logic, and Complexity Theory. Encyclopedia of Mathematics and its Applications, vol. 60. Cambridge University Press, Cambridge (1995)"},{"key":"26_CR33","unstructured":"Lauria, M., Nordstr\u00f6m, J.: Graph colouring is hard for algorithms based on Hilbert\u2019s Nullstellensatz and Gr\u00f6bner bases. In: O\u2019Donnell, R. (ed.) 32nd Computational Complexity Conference (CCC 2017). Leibniz International Proceedings in Informatics (LIPIcs), vol. 79, pp. 2:1\u20132:20. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Dagstuhl (2017)"},{"key":"26_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"684","DOI":"10.1007\/978-3-642-39206-1_58","volume-title":"Automata, Languages, and Programming","author":"M Lauria","year":"2013","unstructured":"Lauria, M., Pudl\u00e1k, P., R\u00f6dl, V., Thapen, N.: The complexity of proving that a graph is Ramsey. In: Fomin, F.V., Freivalds, R., Kwiatkowska, M., Peleg, D. (eds.) ICALP 2013. LNCS, vol. 7965, pp. 684\u2013695. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39206-1_58"},{"issue":"2","key":"26_CR35","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1007\/s00493-015-3193-9","volume":"37","author":"M Lauria","year":"2017","unstructured":"Lauria, M., Pudl\u00e1k, P., R\u00f6dl, V., Thapen, N.: The complexity of proving that a graph is Ramsey. Combinatorica 37(2), 253\u2013268 (2017). Preliminary version in ICALP 2013","journal-title":"Combinatorica"},{"issue":"3","key":"26_CR36","first-page":"115","volume":"9","author":"LA Levin","year":"1973","unstructured":"Levin, L.A.: Universal sequential search problems. Probl. Peredachi Informatsii 9(3), 115\u2013116 (1973)","journal-title":"Probl. Peredachi Informatsii"},{"issue":"105","key":"26_CR37","first-page":"41","volume":"3","author":"D Lokshtanov","year":"2013","unstructured":"Lokshtanov, D., Marx, D., Saurabh, S., et al.: Lower bounds based on the exponential time hypothesis. Bull. EATCS 3(105), 41\u201372 (2013)","journal-title":"Bull. EATCS"},{"issue":"1\u20133","key":"26_CR38","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1016\/0012-365X(92)00057-X","volume":"124","author":"L Lov\u00e1sz","year":"1994","unstructured":"Lov\u00e1sz, L.: Stable sets and polynomials. Discrete Math. 124(1\u20133), 137\u2013153 (1994)","journal-title":"Discrete Math."},{"key":"26_CR39","first-page":"65","volume":"26","author":"YV Matiyasevich","year":"1974","unstructured":"Matiyasevich, Y.V.: A criterion for vertex colorability of a graph stated in terms of edge orientations. Diskretnyi Analiz 26, 65\u201371 (1974). http:\/\/logic.pdmi.ras.ru\/~yumat\/papers\/22paper\/ . English translation of the Russian original","journal-title":"Diskretnyi Analiz"},{"issue":"3","key":"26_CR40","doi-asserted-by":"publisher","first-page":"2401","DOI":"10.1023\/B:JOTH.0000024621.54839.40","volume":"121","author":"YV Matiyasevich","year":"2004","unstructured":"Matiyasevich, Y.V.: Some algebraic methods for calculating the number of colorings of a graph. J. Math. Sci. 121(3), 2401\u20132408 (2004)","journal-title":"J. Math. Sci."},{"key":"26_CR41","unstructured":"McCreesh, C.: Solving hard subgraph problems in parallel. Ph.D. thesis, University of Glasgow (2017)"},{"issue":"3","key":"26_CR42","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1007\/BF01874388","volume":"1","author":"C McDiarmid","year":"1984","unstructured":"McDiarmid, C.: Colouring random graphs. Ann. Oper. Res. 1(3), 183\u2013200 (1984)","journal-title":"Ann. Oper. Res."},{"key":"26_CR43","doi-asserted-by":"publisher","first-page":"431","DOI":"10.1007\/978-3-642-56666-0_33","volume-title":"Computer Algebra in Scientific Computing","author":"M Mnuk","year":"2001","unstructured":"Mnuk, M.: Representing graph properties by polynomial ideals. In: Ganzha, V.G., Mayr, E.W., Vorozhtsov, E.V. (eds.) CASC 2001, pp. 431\u2013444. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/978-3-642-56666-0_33"},{"key":"26_CR44","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-319-09284-3_1","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2014","author":"J Nordstr\u00f6m","year":"2014","unstructured":"Nordstr\u00f6m, J.: A (biased) proof complexity survey for SAT practitioners. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 1\u20136. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-09284-3_1"},{"issue":"3","key":"26_CR45","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1145\/2815493.2815497","volume":"2","author":"J Nordstr\u00f6m","year":"2015","unstructured":"Nordstr\u00f6m, J.: On the interplay between proof complexity and SAT solving. ACM SIGLOG News 2(3), 19\u201344 (2015)","journal-title":"ACM SIGLOG News"},{"issue":"1","key":"26_CR46","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1016\/S0166-218X(01)00290-6","volume":"120","author":"PRJ \u00d6sterg\u00e5rd","year":"2002","unstructured":"\u00d6sterg\u00e5rd, P.R.J.: A fast algorithm for the maximum clique problem. Discrete Appl. Math. 120(1), 197\u2013207 (2002)","journal-title":"Discrete Appl. Math."},{"key":"26_CR47","unstructured":"Pevzner, P.A., Sze, S.-H., et al.: Combinatorial approaches to finding subtle signals in DNA sequences. In: ISMB, vol. 8, pp. 269\u2013278 (2000)"},{"issue":"3","key":"26_CR48","doi-asserted-by":"publisher","first-page":"464","DOI":"10.1137\/S089548019224024X","volume":"8","author":"T Pitassi","year":"1995","unstructured":"Pitassi, T., Urquhart, A.: The complexity of the Haj\u00f3s calculus. SIAM J. Discrete Math. 8(3), 464\u2013483 (1995)","journal-title":"SIAM J. Discrete Math."},{"issue":"4","key":"26_CR49","doi-asserted-by":"publisher","first-page":"545","DOI":"10.3390\/a5040545","volume":"5","author":"P Prosser","year":"2012","unstructured":"Prosser, P.: Exact algorithms for maximum clique: a computational study. Algorithms 5(4), 545\u2013587 (2012)","journal-title":"Algorithms"},{"issue":"2","key":"26_CR50","first-page":"354","volume":"31","author":"AA Razborov","year":"1985","unstructured":"Razborov, A.A.: Lower bounds for the monotone complexity of some Boolean functions. Soviet Math. Dokl. 31(2), 354\u2013357 (1985). English translation of a paper in Doklady Akademii Nauk SSSR","journal-title":"Soviet Math. Dokl."},{"key":"26_CR51","doi-asserted-by":"crossref","unstructured":"Rossman, B.: On the constant-depth complexity of $$k$$-clique. In: Proceedings of the 40th Annual ACM Symposium on Theory of Computing, pp. 721\u2013730. ACM (2008)","DOI":"10.1145\/1374376.1374480"},{"key":"26_CR52","doi-asserted-by":"crossref","unstructured":"Rossman, B.: The monotone complexity of $$k$$-clique on random graphs. In: 51th Annual IEEE Symposium on Foundations of Computer Science, FOCS 2010, 23\u201326 October 2010, Las Vegas, Nevada, USA, pp. 193\u2013201. IEEE Computer Society (2010)","DOI":"10.1109\/FOCS.2010.26"},{"issue":"4","key":"26_CR53","doi-asserted-by":"publisher","first-page":"417","DOI":"10.2178\/bsl\/1203350879","volume":"13","author":"N Segerlind","year":"2007","unstructured":"Segerlind, N.: The complexity of propositional proofs. Bull. Symb. Log. 13(4), 417\u2013481 (2007)","journal-title":"Bull. Symb. Log."}],"container-title":["Lecture Notes in Computer Science","Sailing Routes in the World of Computation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-94418-0_26","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,5]],"date-time":"2020-11-05T03:22:28Z","timestamp":1604546548000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-94418-0_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319944173","9783319944180"],"references-count":53,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-94418-0_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}