{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,12]],"date-time":"2025-06-12T04:13:24Z","timestamp":1749701604371,"version":"3.41.0"},"reference-count":30,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2016,10,19]],"date-time":"2016-10-19T00:00:00Z","timestamp":1476835200000},"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":["Algorithmica"],"published-print":{"date-parts":[[2017,9]]},"DOI":"10.1007\/s00453-016-0228-6","type":"journal-article","created":{"date-parts":[[2016,10,19]],"date-time":"2016-10-19T13:38:02Z","timestamp":1476884282000},"page":"29-41","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Strong ETH and Resolution via Games and the Multiplicity of Strategies"],"prefix":"10.1007","volume":"79","author":[{"given":"Ilario","family":"Bonacina","sequence":"first","affiliation":[]},{"given":"Navid","family":"Talebanfard","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,10,19]]},"reference":[{"key":"228_CR1","doi-asserted-by":"crossref","first-page":"323","DOI":"10.1016\/j.jcss.2007.06.025","volume":"74","author":"A Atserias","year":"2008","unstructured":"Atserias, A., Dalmau, V.: A combinatorial characterization of resolution width. J. Comput. Syst. Sci. 74, 323\u2013334 (2008)","journal-title":"J. Comput. Syst. Sci."},{"key":"228_CR2","doi-asserted-by":"crossref","first-page":"353","DOI":"10.1613\/jair.3152","volume":"40","author":"A Atserias","year":"2011","unstructured":"Atserias, A., Fichte, J.K., Thurley, M.: Clause-learning algorithms with many restarts and bounded-width resolution. J. Artif. Intell. Res. (JAIR) 40, 353\u2013373 (2011)","journal-title":"J. Artif. Intell. Res. (JAIR)"},{"key":"228_CR3","unstructured":"Bayardo Jr., R.J.B., Schrag, R.: Using CSP look-back techniques to solve real-world SAT instances. In: Kuipers, B., Webber, B.L. (eds.) Proceedings of the Fourteenth National Conference on Artificial Intelligence and Ninth Innovative Applications of Artificial Intelligence Conference, AAAI 97, IAAI 97, pp. 203\u2013208, AAAI Press\/The MIT Press, Providence 27\u201331 July 1997"},{"key":"228_CR4","doi-asserted-by":"crossref","unstructured":"Beame, P., Beck, C., Impagliazzo, R.: Time-space tradeoffs in resolution: superpolynomial lower bounds for superlinear space. In: Karloff, H.J., Pitassi, T. (eds.) Proceedings of the 44th Symposium on Theory of Computing Conference, STOC 2012, pp. 213\u2013232, ACM, New York, 19\u201322 May 2012","DOI":"10.1145\/2213977.2213999"},{"key":"228_CR5","doi-asserted-by":"crossref","unstructured":"Beck, C., Impagliazzo, R.: Strong ETH holds for regular resolution. In: Proceedings of the Forty-fifth Annual ACM Symposium on Theory of Computing, STOC \u201913, pp. 487\u2013494, ACM (2013)","DOI":"10.1145\/2488608.2488669"},{"key":"228_CR6","doi-asserted-by":"crossref","first-page":"149","DOI":"10.1145\/375827.375835","volume":"48","author":"E Ben-Sasson","year":"2001","unstructured":"Ben-Sasson, E., Wigderson, A.: Short proofs are narrow - resolution made simple. J. ACM 48, 149\u2013169 (2001)","journal-title":"J. ACM"},{"key":"228_CR7","unstructured":"Blake, A.: Canonical Expressions in Boolean Algebra, PhD thesis. University of Chicago (1937)"},{"key":"228_CR8","doi-asserted-by":"crossref","first-page":"120","DOI":"10.1016\/j.ipl.2015.09.013","volume":"116","author":"I Bonacina","year":"2015","unstructured":"Bonacina, I., Talebanfard, N.: Improving resolution width lower bounds for $$k$$ k -CNFs with applications to the strong exponential time hypothesis. Inf. Process. Lett. 116, 120\u2013124 (2015)","journal-title":"Inf. Process. Lett."},{"key":"228_CR9","doi-asserted-by":"crossref","unstructured":"Chen, R., Kabanets, V., Kolokolova, A., Shaltiel, R., Zuckerman, D.: Mining circuit lower bound proofs for meta-algorithms. In: IEEE 29th Conference on Computational Complexity, CCC, pp. 262\u2013273 (2014)","DOI":"10.1109\/CCC.2014.34"},{"key":"228_CR10","doi-asserted-by":"crossref","unstructured":"Chen, R., Kabanets, V., Saurabh, N.: An improved deterministic #SAT algorithm for small de morgan formulas. In: Mathematical Foundations of Computer Science 2014 - 39th International Symposium, MFCS, pp. 165\u2013176 (2014)","DOI":"10.1007\/978-3-662-44465-8_15"},{"key":"228_CR11","doi-asserted-by":"crossref","unstructured":"Chen, S., Scheder, D., Talebanfard, N., Tang, B.: Exponential lower bounds for the PPSZ $$k$$ k -SAT algorithm. In: SODA, pp. 1253\u20131263 (2013)","DOI":"10.1137\/1.9781611973105.91"},{"key":"228_CR12","doi-asserted-by":"crossref","unstructured":"Dantchev, S.S.: Relativisation provides natural separations for resolution-based proof systems. In: Proceedings of Computer Science - Theory and Applications, First International Computer Science Symposium in Russia, pp. 147\u2013158, CSR 2006, St. Petersburg, 8\u201312 June 2006","DOI":"10.1007\/11753728_17"},{"key":"228_CR13","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1016\/S0304-3975(01)00174-8","volume":"289","author":"E Dantsin","year":"2002","unstructured":"Dantsin, E., Goerdt, A., Hirsch, E.A., Kannan, R., Kleinberg, J.M., Papadimitriou, C.H., Raghavan, P., Sch\u00f6ning, U.: A deterministic (2\u20132\/ $$(k+1))^n$$ ( k + 1 ) ) n algorithm for $$k$$ k -SAT based on local search. Theor. Comput. Sci. 289, 69\u201383 (2002)","journal-title":"Theor. Comput. Sci."},{"key":"228_CR14","doi-asserted-by":"crossref","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M Davis","year":"1962","unstructured":"Davis, M., Logemann, G., Loveland, D.W.: A machine program for theorem-proving. Commun. ACM 5, 394\u2013397 (1962)","journal-title":"Commun. ACM"},{"key":"228_CR15","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M Davis","year":"1960","unstructured":"Davis, M., Putnam, H.: A computing procedure for quantification theory. J. ACM 7, 201\u2013215 (1960)","journal-title":"J. ACM"},{"key":"228_CR16","doi-asserted-by":"crossref","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. Theor. Comput. Sci. 39, 297\u2013308 (1985)","journal-title":"Theor. Comput. Sci."},{"key":"228_CR17","doi-asserted-by":"crossref","first-page":"367","DOI":"10.1006\/jcss.2000.1727","volume":"62","author":"R Impagliazzo","year":"2001","unstructured":"Impagliazzo, R., Paturi, R.: On the complexity of $$k$$ k -SAT. J. Comput. Syst. Sci. 62, 367\u2013375 (2001)","journal-title":"J. Comput. Syst. Sci."},{"key":"228_CR18","doi-asserted-by":"crossref","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient SAT solver. In: Proceedings of the 38th Design Automation Conference, DAC 2001, pp. 530\u2013535, ACM, Las Vegas, 18\u201322 June 2001","DOI":"10.1145\/378239.379017"},{"key":"228_CR19","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1145\/1066100.1066101","volume":"52","author":"R Paturi","year":"2005","unstructured":"Paturi, R., Pudl\u00e1k, P., Saks, M.E., Zane, F.: An improved exponential-time algorithm for $$k$$ k -SAT. J. ACM 52, 337\u2013364 (2005)","journal-title":"J. ACM"},{"key":"228_CR20","doi-asserted-by":"crossref","unstructured":"Paturi, R., Pudl\u00e1k, P., Zane, F.: Satisfiability coding lemma. In: 38th Annual Symposium on Foundations of Computer Science, FOCS, pp. 566\u2013574 (1997)","DOI":"10.1109\/SFCS.1997.646146"},{"key":"228_CR21","doi-asserted-by":"crossref","first-page":"512","DOI":"10.1016\/j.artint.2010.10.002","volume":"175","author":"K Pipatsrisawat","year":"2011","unstructured":"Pipatsrisawat, K., Darwiche, A.: On the power of clause-learning SAT solvers as resolution engines. Artif. Intell. 175, 512\u2013525 (2011)","journal-title":"Artif. Intell."},{"key":"228_CR22","doi-asserted-by":"crossref","first-page":"541","DOI":"10.2307\/2589349","volume":"107","author":"P Pudl\u00e1k","year":"2000","unstructured":"Pudl\u00e1k, P.: Proofs as games. Am. Math. Mon. 107, 541\u2013550 (2000)","journal-title":"Am. Math. Mon."},{"key":"228_CR23","unstructured":"Pudl\u00e1k, P., Impagliazzo, R.: A lower bound for DLL algorithms for $$k$$ k -SAT (preliminary version). In: Proceedings of the Eleventh Annual ACM-SIAM Symposium on Discrete Algorithms, SODA \u201900, pp. 128\u2013136 (2000)"},{"key":"228_CR24","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"JA Robinson","year":"1965","unstructured":"Robinson, J.A.: A machine-oriented logic based on the resolution principle. J. ACM 12, 23\u201341 (1965)","journal-title":"J. ACM"},{"key":"228_CR25","doi-asserted-by":"crossref","unstructured":"Santhanam, R.: Fighting perebor: new and improved algorithms for formula and QBF satisfiability. In: 51th Annual IEEE Symposium on Foundations of Computer Science. FOCS 2010, 183\u2013192 (2010)","DOI":"10.1109\/FOCS.2010.25"},{"key":"228_CR26","doi-asserted-by":"crossref","unstructured":"Sch\u00f6ning, U.: A probabilistic algorithm for $$k$$ k -SAT and constraint satisfaction problems. In: 40th Annual Symposium on Foundations of Computer Science, FOCS, pp. 410\u2013414 (1999)","DOI":"10.1109\/SFFCS.1999.814612"},{"key":"228_CR27","doi-asserted-by":"crossref","first-page":"506","DOI":"10.1109\/12.769433","volume":"48","author":"JPM Silva","year":"1999","unstructured":"Silva, J.P.M., Sakallah, K.A.: GRASP: a search algorithm for propositional satisfiability. IEEE Trans. Comput. 48, 506\u2013521 (1999)","journal-title":"IEEE Trans. Comput."},{"key":"228_CR28","doi-asserted-by":"crossref","first-page":"209","DOI":"10.1145\/7531.8928","volume":"34","author":"A Urquhart","year":"1987","unstructured":"Urquhart, A.: Hard examples for resolution. J. ACM 34, 209\u2013219 (1987)","journal-title":"J. ACM"},{"key":"228_CR29","doi-asserted-by":"crossref","unstructured":"Williams, R.: Improving exhaustive search implies superpolynomial lower bounds. In: Proceedings of the 42nd ACM Symposium on Theory of Computing, STOC, pp. 231\u2013240 (2010)","DOI":"10.1145\/1806689.1806723"},{"key":"228_CR30","doi-asserted-by":"crossref","unstructured":"Williams, R.: Non-uniform ACC circuit lower bounds. In: Proceedings of the 26th Annual IEEE Conference on Computational Complexity, CCC, pp. 115\u2013125 (2011)","DOI":"10.1109\/CCC.2011.36"}],"container-title":["Algorithmica"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00453-016-0228-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00453-016-0228-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00453-016-0228-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,11]],"date-time":"2025-06-11T17:41:16Z","timestamp":1749663676000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00453-016-0228-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,10,19]]},"references-count":30,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2017,9]]}},"alternative-id":["228"],"URL":"https:\/\/doi.org\/10.1007\/s00453-016-0228-6","relation":{},"ISSN":["0178-4617","1432-0541"],"issn-type":[{"type":"print","value":"0178-4617"},{"type":"electronic","value":"1432-0541"}],"subject":[],"published":{"date-parts":[[2016,10,19]]}}}