{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,26]],"date-time":"2026-02-26T05:11:45Z","timestamp":1772082705276,"version":"3.50.1"},"reference-count":25,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2011,11,25]],"date-time":"2011-11-25T00:00:00Z","timestamp":1322179200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["comput. complex."],"published-print":{"date-parts":[[2011,12]]},"DOI":"10.1007\/s00037-011-0033-1","type":"journal-article","created":{"date-parts":[[2011,11,24]],"date-time":"2011-11-24T10:05:41Z","timestamp":1322129141000},"page":"649-678","source":"Crossref","is-referenced-by-count":18,"title":["Satisfiability, Branch-Width and Tseitin tautologies"],"prefix":"10.1007","volume":"20","author":[{"given":"Michael","family":"Alekhnovich","sequence":"first","affiliation":[]},{"given":"Alexander","family":"Razborov","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2011,11,25]]},"reference":[{"key":"33_CR1","doi-asserted-by":"crossref","unstructured":"M. Alekhnovich (2004). Mutilated chessboard problem is exponentially hard for resolution. Theoretical Computer Science 310(1-3), 513\u2013525.","DOI":"10.1016\/S0304-3975(03)00395-5"},{"issue":"1","key":"33_CR2","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1137\/S0097539701389944","volume":"34","author":"M. Alekhnovich","year":"2004","unstructured":"Alekhnovich M., Ben-Sasson E., Razborov A., Wigderson A. (2004) Pseudorandom generators in propositional proof complexity. SIAM Journal on Computing 34(1): 67\u201388","journal-title":"SIAM Journal on Computing"},{"key":"33_CR3","unstructured":"M. Alekhnovich & A. Razborov (2003). Lower bounds for the polynomial calculus: non-binomial case. Proceedings of the Steklov Institute of Mathematics 242, 18-35."},{"issue":"4","key":"33_CR4","doi-asserted-by":"crossref","first-page":"1347","DOI":"10.1137\/06066850X","volume":"38","author":"M. Alekhnovich","year":"2008","unstructured":"Alekhnovich M., Razborov A. (2008) Resolution is not automatizable unless W[P] is tractable. SIAM Journal on Computing 38(4): 1347\u20131363","journal-title":"SIAM Journal on Computing"},{"issue":"1","key":"33_CR5","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/BF02579196","volume":"7","author":"N. Alon","year":"1987","unstructured":"Alon N., Boppana R. (1987) The monotone circuit complexity of Boolean functions. Combinatorica 7(1): 1\u201322","journal-title":"Combinatorica"},{"key":"33_CR6","unstructured":"E. Amir & S. McIlraith (2001). Solving Satisfiability using Decomposition and the Most Constrained Subproblem. In LICS workshop on Theory and Applications of Satisfiability Testing (SAT 2001)."},{"issue":"2","key":"33_CR7","doi-asserted-by":"crossref","first-page":"182","DOI":"10.1016\/j.ic.2003.10.004","volume":"189","author":"A. Atserias","year":"2004","unstructured":"Atserias A., Bonet M. (2004) On the Automatizability of Resolution and Related Propositional Proof Systems. Information and Computation 189(2): 182\u2013201","journal-title":"Information and Computation"},{"key":"33_CR8","unstructured":"P. Beame & T. Pitassi (1996). Simplified and improved resolution lower bounds. In Proceedings of the 37th IEEE FOCS, 274\u2013282."},{"key":"33_CR9","unstructured":"E. Ben-Sasson & R. Impagliazzo (1999). Random CNF\u2019 s are Hard for the Polynomial Calculus. In Proceedings of the 40th IEEE FOCS, 415\u2013421."},{"issue":"2","key":"33_CR10","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. (2001) Short Proofs are Narrow - Resolution made Simple. Journal of the ACM 48(2): 149\u2013169","journal-title":"Journal of the ACM"},{"key":"33_CR11","first-page":"1","volume":"11","author":"H.L. Bodlaender","year":"1993","unstructured":"Bodlaender H.L. (1993) A Tourist Guide through Treewidth. Acta Cybernetica 11: 1\u201321","journal-title":"Acta Cybernetica"},{"key":"33_CR12","unstructured":"M. Bonet & N. Galesi (1999). A study of proof search algorithms for Resolution and Polynomial Calculus. In Proceedings of the 40th IEEE FOCS, 422\u2013431."},{"issue":"6","key":"33_CR13","doi-asserted-by":"crossref","first-page":"1939","DOI":"10.1137\/S0097539798353230","volume":"29","author":"M. Bonet","year":"2000","unstructured":"Bonet M., Pitassi T., Raz R. (2000) On Interpolation and Automatization for Frege Systems. SIAM Journal on Computing 29(6): 1939\u20131967","journal-title":"SIAM Journal on Computing"},{"key":"33_CR14","unstructured":"S. Chen, T. Lou, P. Papakonstantinou & B. Tang (2011). Width-parameterized SAT: Time-Space Tradeoffs. Technical Report cs.CC\/1108.2385, arXiv e-print."},{"key":"33_CR15","doi-asserted-by":"crossref","unstructured":"B. Courcelle, J. A. Makowsky & U. Rotics (2001). On the Fixed Parameter Complexity of Graph Enumeration Problems Definable in Monadic Second Order Logic. Discrete Applied Mathematics 108(1-2), 23\u201352.","DOI":"10.1016\/S0166-218X(00)00221-3"},{"key":"33_CR16","first-page":"8","volume":"12","author":"E. Dantsin","year":"1979","unstructured":"Dantsin E. (1979) Parameters defining the time of tautology recognition by the splitting method. Semiotics and information science 12: 8\u201317 In Russian","journal-title":"Semiotics and information science"},{"key":"33_CR17","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1112\/jlms\/s1-35.1.85","volume":"35","author":"P. Erd\u00f6s","year":"1960","unstructured":"Erd\u00f6s P., Rado R. (1960) Intersection theorems for systems of sets. Journal of the London Math. Society 35: 85\u201390","journal-title":"Journal of the London Math. Society"},{"key":"33_CR18","unstructured":"S. Khanna & R. Motwani (1996). Towards a Syntactic Characterization of PTAS. In Proceedings of the 28th ACM Symposium on the Theory of Computing, 329\u2013337."},{"key":"33_CR19","doi-asserted-by":"crossref","unstructured":"J. Kraj\u00ed\u010dek (1992). No counter-example interpretation and interactive computation. In Logic from Computer Science, Y. N. Moschovakis, editor, 287\u2013293. Springer-Verlag.","DOI":"10.1007\/978-1-4612-2822-6_11"},{"key":"33_CR20","doi-asserted-by":"crossref","first-page":"177","DOI":"10.1137\/0136016","volume":"36","author":"R. Lipton","year":"1979","unstructured":"Lipton R., Tarjan R. (1979) A Separator Theorem for Planar Graphs. SIAM Journal on Applied Mathematics 36: 177\u2013189","journal-title":"SIAM Journal on Applied Mathematics"},{"key":"33_CR21","doi-asserted-by":"crossref","first-page":"615","DOI":"10.1137\/0209046","volume":"9","author":"R. Lipton","year":"1980","unstructured":"Lipton R., Tarjan R. (1980) Applications of a Planar Separator Theorem. SIAM Journal on Computing 9: 615\u2013627","journal-title":"SIAM Journal on Computing"},{"key":"33_CR22","unstructured":"A. A. Razborov (1985). Lower bounds for the monotone complexity of some Boolean functions. Doklady Academii Nauk SSSR 281(4), 798\u2013801. English Translation in Soviet Math. Dokl., 31:354-357, 1985."},{"key":"33_CR23","unstructured":"N. Robertson & P. D. Seymour (1991). Graph minors. X. Obstructions to tree decomposition. Journal of Combinatorial Theory Series B 52, 153\u2013190."},{"key":"33_CR24","doi-asserted-by":"crossref","first-page":"65","DOI":"10.1006\/jctb.1995.1006","volume":"63","author":"N. Robertson","year":"1995","unstructured":"Robertson N., Seymour P.D. (1995) Graph minors. XIII. The disjoint paths problem. Journal of Combinatorial Theory Series B 63: 65\u2013110","journal-title":"Journal of Combinatorial Theory Series B"},{"key":"33_CR25","unstructured":"G. S. Tseitin (1968). On the complexity of derivations in propositional calculus. In Studies in constructive mathematics and mathematical logic, Part II. Consultants Bureau, New-York-London."}],"container-title":["computational complexity"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00037-011-0033-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00037-011-0033-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00037-011-0033-1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,20]],"date-time":"2019-06-20T00:57:27Z","timestamp":1560992247000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00037-011-0033-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,11,25]]},"references-count":25,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2011,12]]}},"alternative-id":["33"],"URL":"https:\/\/doi.org\/10.1007\/s00037-011-0033-1","relation":{},"ISSN":["1016-3328","1420-8954"],"issn-type":[{"value":"1016-3328","type":"print"},{"value":"1420-8954","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011,11,25]]}}}