{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T11:16:41Z","timestamp":1725880601200},"publisher-location":"Cham","reference-count":17,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319539249"},{"type":"electronic","value":"9783319539256"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-53925-6_28","type":"book-chapter","created":{"date-parts":[[2017,2,19]],"date-time":"2017-02-19T20:12:36Z","timestamp":1487535156000},"page":"359-369","source":"Crossref","is-referenced-by-count":0,"title":["An Upper Bound for Resolution Size: Characterization of Tractable SAT Instances"],"prefix":"10.1007","author":[{"given":"Kensuke","family":"Imanishi","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,2,21]]},"reference":[{"issue":"1","key":"28_CR1","doi-asserted-by":"crossref","first-page":"171","DOI":"10.2307\/2694916","volume":"66","author":"M Alekhnovich","year":"2001","unstructured":"Alekhnovich, M., Buss, S., Moran, S., Pitassi, T.: Minimum propositional proof length is NP-hard to linearly approximate. J. Symb. Log. 66(1), 171\u2013191 (2001)","journal-title":"J. Symb. Log."},{"key":"28_CR2","doi-asserted-by":"crossref","unstructured":"Alekhnovich, M., Razborov, A.A.: Resolution is not automatizable unless W[P] is tractable. In: Proceedings of the 42nd Annual IEEE Symposium on Foundations of Computer Science (FOCS 2001), pp. 210\u2013219. IEEE (2001)","DOI":"10.1109\/SFCS.2001.959895"},{"key":"28_CR3","doi-asserted-by":"crossref","unstructured":"Alekhnovich, M., Razborov, A.A.: Satisfiability, branch-width and Tseitin tautologies. In: Proceedings of the 43rd Annual IEEE Symposium on Foundations of Computer Science (FOCS 2002), pp. 593\u2013603. IEEE (2002)","DOI":"10.1109\/SFCS.2002.1181983"},{"key":"28_CR4","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. 40, 353\u2013373 (2011)","journal-title":"J. Artif. Intell. Res."},{"key":"28_CR5","doi-asserted-by":"crossref","unstructured":"Atserias, A., Lauria, M., Nordstr\u00f6m, J.: Narrow proofs may be maximally long. In: Proceedings of the 29th Annual IEEE Conference on Computational Complexity (CCC 2014), pp. 287\u2013297. IEEE (2014)","DOI":"10.1109\/CCC.2014.36"},{"key":"28_CR6","unstructured":"Beame, P., Kautz, H., Sabharwal, A.: Understanding the power of clause learning. In: International Joint Conference on Artificial Intelligence (IJCAI), pp. 1194\u20131201 (2003)"},{"key":"28_CR7","doi-asserted-by":"crossref","unstructured":"Ben-Sasson, E., Wigderson, A.: Short proofs are narrow - resolution made simple. In: Proceedings of the 31st Annual ACM Symposium on Theory of Computing (STOC 1999), pp. 517\u2013526 (1999)","DOI":"10.1145\/301250.301392"},{"key":"28_CR8","doi-asserted-by":"crossref","unstructured":"Bodlaender, H.L.: A linear time algorithm for finding tree-decompositions of small treewidth. In: Proceedings of the 25th Annual ACM Symposium on Theory of Computing (STOC 1993), pp. 226\u2013234. ACM (1993)","DOI":"10.1145\/167088.167161"},{"key":"28_CR9","doi-asserted-by":"crossref","first-page":"358","DOI":"10.1006\/jagm.1996.0049","volume":"21","author":"HL Bodlaender","year":"1996","unstructured":"Bodlaender, H.L., Kloks, T.: Efficient and constructive algorithms for the pathwidth and treewidth of graphs. J. Algorithms 21, 358\u2013402 (1996)","journal-title":"J. Algorithms"},{"issue":"7","key":"28_CR10","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.: A machine program for theorem-proving. Commun. ACM 5(7), 394\u2013397 (1962)","journal-title":"Commun. ACM"},{"issue":"3","key":"28_CR11","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(3), 201\u2013215 (1960)","journal-title":"J. ACM"},{"key":"28_CR12","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. Theoret. Comput. Sci. 39, 297\u2013308 (1985)","journal-title":"Theoret. Comput. Sci."},{"key":"28_CR13","doi-asserted-by":"crossref","unstructured":"Kolaitis, P.G., Vardi, M.Y.: Conjunctive-query containment and constraint satisfaction. In: Proceedings of the 17th ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems (PODS 1998), pp. 205\u2013213 (1998)","DOI":"10.1145\/275487.275511"},{"key":"28_CR14","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1016\/0166-218X(93)90171-J","volume":"43","author":"E Korach","year":"1993","unstructured":"Korach, E., Solel, N.: Tree-width, path-width, and cutwidth. Discret. Appl. Math. 43, 97\u2013101 (1993)","journal-title":"Discret. Appl. Math."},{"issue":"1","key":"28_CR15","doi-asserted-by":"crossref","first-page":"50","DOI":"10.1016\/j.jda.2009.06.002","volume":"8","author":"M Samer","year":"2010","unstructured":"Samer, M., Szeider, S.: Algorithms for propositional model counting. J. Discret. Algorithms 8(1), 50\u201364 (2010)","journal-title":"J. Discret. Algorithms"},{"key":"28_CR16","unstructured":"Silva, J.P.M., Sakallah, K.A.: GRASP - a new search algorithm for satisfiability. In: Proceedings of the 1996 IEEE\/ACM International Conference on Computer-Aided Design, pp. 220\u2013227 (1996)"},{"key":"28_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"627","DOI":"10.1007\/3-540-63165-8_217","volume-title":"Automata, Languages and Programming","author":"HL Bodlaender","year":"1997","unstructured":"Bodlaender, H.L., Thilikos, D.M.: Constructive linear time algorithms for branchwidth. In: Degano, P., Gorrieri, R., Marchetti-Spaccamela, A. (eds.) ICALP 1997. LNCS, vol. 1256, pp. 627\u2013637. Springer, Heidelberg (1997). doi: 10.1007\/3-540-63165-8_217"}],"container-title":["Lecture Notes in Computer Science","WALCOM: Algorithms and Computation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-53925-6_28","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,18]],"date-time":"2019-09-18T17:30:45Z","timestamp":1568827845000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-53925-6_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319539249","9783319539256"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-53925-6_28","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}