{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:29:17Z","timestamp":1761611357363},"publisher-location":"Cham","reference-count":59,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319092836"},{"type":"electronic","value":"9783319092843"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-09284-3_13","type":"book-chapter","created":{"date-parts":[[2014,7,2]],"date-time":"2014-07-02T09:43:21Z","timestamp":1404294201000},"page":"170-187","source":"Crossref","is-referenced-by-count":5,"title":["Unified Characterisations of Resolution Hardness Measures"],"prefix":"10.1007","author":[{"given":"Olaf","family":"Beyersdorff","sequence":"first","affiliation":[]},{"given":"Oliver","family":"Kullmann","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"13_CR1","doi-asserted-by":"publisher","first-page":"238","DOI":"10.1016\/j.jcss.2003.07.011","volume":"68","author":"D. Achlioptas","year":"2004","unstructured":"Achlioptas, D., Beame, P., Molloy, M.: A sharp threshold in proof complexity yields lower bounds for satisfiability search. Journal of Computer and System Sciences\u00a068, 238\u2013268 (2004)","journal-title":"Journal of Computer and System Sciences"},{"issue":"4","key":"13_CR2","doi-asserted-by":"publisher","first-page":"1184","DOI":"10.1137\/S0097539700366735","volume":"31","author":"M. Alekhnovich","year":"2002","unstructured":"Alekhnovich, M., Ben-Sasson, E., Razborov, A.A., Wigderson, A.: Space complexity in propositional calculus. SIAM Journal on Computing\u00a031(4), 1184\u20131211 (2002)","journal-title":"SIAM Journal on Computing"},{"issue":"1-3","key":"13_CR3","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1007\/s10817-005-9006-x","volume":"35","author":"M. Alekhnovich","year":"2005","unstructured":"Alekhnovich, M., Hirsch, E.A., Itsykson, D.: Exponential lower bounds for the running time of DPLL algorithms on satisfiable formulas. Journal of Automated Reasoning\u00a035(1-3), 51\u201372 (2005)","journal-title":"Journal of Automated Reasoning"},{"key":"13_CR4","unstructured":"Ans\u00f3tegui, C., Bonet, M.L., Levy, J., Many\u00e0, F.: Measuring the hardness of SAT instances. In: Fox, D., Gomes, C. (eds.) Proceedings of the 23th AAAI Conference on Artificial Intelligence (AAAI 2008), pp. 222\u2013228 (2008)"},{"key":"13_CR5","doi-asserted-by":"publisher","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. Journal of Computer and System Sciences\u00a074, 323\u2013334 (2008)","journal-title":"Journal of Computer and System Sciences"},{"key":"13_CR6","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1016\/j.artint.2013.07.006","volume":"203","author":"M. Babka","year":"2013","unstructured":"Babka, M., Balyo, T., \u010cepek, O., Gursk\u00fd, \u0160., Ku\u010dera, P., Vl\u010dek, V.: Complexity issues related to propagation completeness. Artificial Intelligence\u00a0203, 19\u201334 (2013)","journal-title":"Artificial Intelligence"},{"key":"13_CR7","unstructured":"Balyo, T., Gursk\u00fd, \u0160., Ku\u010dera, P., Vl\u010dek, V.: On hierarchies over the SLUR class. In: Twelfth International Symposium on Artificial Intelligence and Mathematics, ISAIM 2012 (January 2012), http:\/\/www.cs.uic.edu\/bin\/view\/Isaim2012\/AcceptedPapers"},{"key":"13_CR8","doi-asserted-by":"crossref","unstructured":"Beame, P., Beck, C., Impagliazzo, R.: Time-space tradeoffs in resolution: superpolynomial lower bounds for superlinear space. In: STOC 2012 Proceedings of the 44th Symposium on Theory of Computing, pp. 213\u2013232 (2012)","DOI":"10.1145\/2213977.2213999"},{"key":"13_CR9","doi-asserted-by":"crossref","unstructured":"Beck, C., Nordstr\u00f6m, J., Tang, B.: Some trade-off results for polynomial calculus: extended abstract. In: Proceedings of the Forty-fifth Annual ACM Symposium on Theory of Computing (STOC 2013), pp. 813\u2013822 (2013)","DOI":"10.1145\/2488608.2488711"},{"key":"13_CR10","doi-asserted-by":"crossref","unstructured":"Ben-Sasson, E., Harsha, P.: Lower bounds for bounded depth Frege proofs via Buss-Pudl\u00e1k games. ACM Transactions on Computational Logic\u00a011(3) (2010)","DOI":"10.1145\/1740582.1740587"},{"key":"13_CR11","doi-asserted-by":"crossref","unstructured":"Ben-Sasson, E., Nordstr\u00f6m, J.: Short proofs may be spacious: An optimal separation of space and length in resolution. In: Proc. 49th IEEE Symposium on the Foundations of Computer Science, pp. 709\u2013718 (2008)","DOI":"10.1109\/FOCS.2008.42"},{"key":"13_CR12","unstructured":"Ben-Sasson, E., Nordstr\u00f6m, J.: Understanding space in proof complexity: Separations and trade-offs via substitutions. In: Innovations in Computer Science, ICS 2010, January 7-9, pp. 401\u2013416. Tsinghua University, Beijing (2011)"},{"issue":"2","key":"13_CR13","doi-asserted-by":"publisher","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. Journal of the ACM\u00a048(2), 149\u2013169 (2001)","journal-title":"Journal of the ACM"},{"issue":"23","key":"13_CR14","doi-asserted-by":"publisher","first-page":"1074","DOI":"10.1016\/j.ipl.2010.09.007","volume":"110","author":"O. Beyersdorff","year":"2010","unstructured":"Beyersdorff, O., Galesi, N., Lauria, M.: A lower bound for the pigeonhole principle in tree-like resolution by asymmetric prover-delayer games. Information Processing Letters\u00a0110(23), 1074\u20131077 (2010)","journal-title":"Information Processing Letters"},{"issue":"18","key":"13_CR15","doi-asserted-by":"publisher","first-page":"666","DOI":"10.1016\/j.ipl.2013.06.002","volume":"113","author":"O. Beyersdorff","year":"2013","unstructured":"Beyersdorff, O., Galesi, N., Lauria, M.: A characterization of tree-like resolution size. Information Processing Letters\u00a0113(18), 666\u2013671 (2013)","journal-title":"Information Processing Letters"},{"key":"13_CR16","doi-asserted-by":"crossref","unstructured":"Beyersdorff, O., Galesi, N., Lauria, M.: Parameterized complexity of DPLL search procedures. ACM Transactions on Computational Logic\u00a014(3) (2013)","DOI":"10.1145\/2499937.2499941"},{"key":"13_CR17","unstructured":"Beyersdorff, O., Kullmann, O.: Hardness measures and resolution lower bounds. Tech. Rep. arXiv:1310.7627v2 [cs.CC], arXiv (February 2014)"},{"issue":"2-4","key":"13_CR18","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/BF02127749","volume":"18","author":"M. Buro","year":"1996","unstructured":"Buro, M., Kleine B\u00fcning, H.: On resolution with short clauses. Annals of Mathematics and Artificial Intelligence\u00a018(2-4), 243\u2013260 (1996)","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"key":"13_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"177","DOI":"10.1007\/978-3-642-27660-6_15","volume-title":"SOFSEM 2012: Theory and Practice of Computer Science","author":"O. \u010cepek","year":"2012","unstructured":"\u010cepek, O., Ku\u010dera, P., Vl\u010dek, V.: Properties of SLUR formulae. In: Bielikov\u00e1, M., Friedrich, G., Gottlob, G., Katzenbeisser, S., Tur\u00e1n, G. (eds.) SOFSEM 2012. LNCS, vol.\u00a07147, pp. 177\u2013189. Springer, Heidelberg (2012)"},{"key":"13_CR20","doi-asserted-by":"crossref","unstructured":"Chan, S.M.: Just a pebble game. In: 2013 IEEE Conference on Computational Complexity (CCC), pp. 133\u2013143 (2013)","DOI":"10.1109\/CCC.2013.22"},{"key":"13_CR21","doi-asserted-by":"crossref","unstructured":"Chan, S.M.: Just a pebble game. Tech. Rep. TR13-042, Electronic Colloquium on Computational Complexity (ECCC), 41 pages (March 2013), http:\/\/eccc.hpi-web.de\/report\/2013\/042\/","DOI":"10.1109\/CCC.2013.22"},{"key":"13_CR22","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 ACM Symposium on Theory of Computation, pp. 174\u2013183 (1996)","DOI":"10.1145\/237814.237860"},{"key":"13_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-319-04921-2_1","volume-title":"Language and Automata Theory and Applications","author":"J. Esparza","year":"2014","unstructured":"Esparza, J., Luttenberger, M., Schlund, M.: A brief history of Strahler numbers. In: Dediu, A.-H., Mart\u00edn-Vide, C., Sierra-Rodr\u00edguez, J.-L., Truthe, B. (eds.) LATA 2014. LNCS, vol.\u00a08370, pp. 1\u201313. Springer, Heidelberg (2014)"},{"key":"13_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"551","DOI":"10.1007\/3-540-49116-3_52","volume-title":"STACS 99","author":"J.L. Esteban","year":"1999","unstructured":"Esteban, J.L., Tor\u00e1n, J.: Space bounds for resolution. In: Meinel, C., Tison, S. (eds.) STACS 1999. LNCS, vol.\u00a01563, pp. 551\u2013560. Springer, Heidelberg (1999)"},{"issue":"1","key":"13_CR25","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1006\/inco.2001.2921","volume":"171","author":"J.L. Esteban","year":"2001","unstructured":"Esteban, J.L., Tor\u00e1n, J.: Space bounds for resolution. Information and Computation\u00a0171(1), 84\u201397 (2001)","journal-title":"Information and Computation"},{"issue":"6","key":"13_CR26","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1016\/S0020-0190(03)00345-4","volume":"87","author":"J.L. Esteban","year":"2003","unstructured":"Esteban, J.L., Tor\u00e1n, J.: A combinatorial characterization of treelike resolution space. Information Processing Letters\u00a087(6), 295\u2013300 (2003)","journal-title":"Information Processing Letters"},{"key":"13_CR27","unstructured":"Groote, J.F., Warners, J.P.: The popositional formula checker HeerHugo. Tech. Rep. SEN-R9905, Centre for Mathematics and Computer Science (CWI), Amsterdam, The Netherlands (January 1999)"},{"issue":"1-2","key":"13_CR28","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1023\/A:1006366304347","volume":"24","author":"J.F. Groote","year":"2000","unstructured":"Groote, J.F., Warners, J.P.: The propositional formula checker HeerHugo. Journal of Automated Reasoning\u00a024(1-2), 101\u2013125 (2000)","journal-title":"Journal of Automated Reasoning"},{"key":"13_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"220","DOI":"10.1007\/978-3-642-35843-2_20","volume-title":"SOFSEM 2013: Theory and Practice of Computer Science","author":"M. Gwynne","year":"2013","unstructured":"Gwynne, M., Kullmann, O.: Generalising and unifying SLUR and unit-refutation completeness. In: van Emde Boas, P., Groen, F.C.A., Italiano, G.F., Nawrocki, J., Sack, H. (eds.) SOFSEM 2013. LNCS, vol.\u00a07741, pp. 220\u2013232. Springer, Heidelberg (2013)"},{"key":"13_CR30","doi-asserted-by":"crossref","unstructured":"Gwynne, M., Kullmann, O.: On SAT representations of XOR constraints. Tech. Rep. arXiv:1309.3060v4 [cs.CC], arXiv (December 2013)","DOI":"10.1007\/978-3-319-04921-2_33"},{"key":"13_CR31","unstructured":"Gwynne, M., Kullmann, O.: Trading inference effort versus size in CNF knowledge compilation. Tech. Rep. arXiv:1310.5746v2 [cs.CC], arXiv (November 2013)"},{"issue":"1","key":"13_CR32","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/s10817-013-9275-8","volume":"52","author":"M. Gwynne","year":"2014","unstructured":"Gwynne, M., Kullmann, O.: Generalising unit-refutation completeness and SLUR via nested input resolution. Journal of Automated Reasoning\u00a052(1), 31\u201365 (2014)","journal-title":"Journal of Automated Reasoning"},{"key":"13_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"409","DOI":"10.1007\/978-3-319-04921-2_33","volume-title":"Language and Automata Theory and Applications","author":"M. Gwynne","year":"2014","unstructured":"Gwynne, M., Kullmann, O.: On SAT representations of XOR constraints. In: Dediu, A.-H., Mart\u00edn-Vide, C., Sierra-Rodr\u00edguez, J.-L., Truthe, B. (eds.) LATA 2014. LNCS, vol.\u00a08370, pp. 409\u2013420. Springer, Heidelberg (2014)"},{"key":"13_CR34","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. Theoretical Computer Science\u00a039, 297\u2013308 (1985)","journal-title":"Theoretical Computer Science"},{"issue":"4","key":"13_CR35","doi-asserted-by":"publisher","first-page":"583","DOI":"10.1007\/s10817-011-9239-9","volume":"49","author":"M. J\u00e4rvisalo","year":"2012","unstructured":"J\u00e4rvisalo, M., Biere, A., Heule, M.: Simulating circuit-level simplifications on CNF. Journal of Automated Reasoning\u00a049(4), 583\u2013619 (2012)","journal-title":"Journal of Automated Reasoning"},{"key":"13_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"355","DOI":"10.1007\/978-3-642-31365-3_28","volume-title":"Automated Reasoning","author":"M. J\u00e4rvisalo","year":"2012","unstructured":"J\u00e4rvisalo, M., Heule, M.J.H., Biere, A.: Inprocessing rules. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol.\u00a07364, pp. 355\u2013370. Springer, Heidelberg (2012)"},{"key":"13_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"316","DOI":"10.1007\/978-3-642-33558-7_25","volume-title":"Principles and Practice of Constraint Programming","author":"M. J\u00e4rvisalo","year":"2012","unstructured":"J\u00e4rvisalo, M., Matsliah, A., Nordstr\u00f6m, J., \u017divn\u00fd, S.: Relating proof complexity measures and practical hardness of SAT. In: Milano, M. (ed.) CP 2012. LNCS, vol.\u00a07514, pp. 316\u2013331. Springer, Heidelberg (2012)"},{"key":"13_CR38","doi-asserted-by":"publisher","first-page":"405","DOI":"10.1016\/0304-3975(93)90331-M","volume":"116","author":"H. Kleine B\u00fcning","year":"1993","unstructured":"Kleine B\u00fcning, H.: On generalized Horn formulas and k-resolution. Theoretical Computer Science\u00a0116, 405\u2013413 (1993)","journal-title":"Theoretical Computer Science"},{"key":"13_CR39","unstructured":"Kleine B\u00fcning, H., Kullmann, O.: Minimal unsatisfiability and autarkies. In: Biere, A., Heule, M.J., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol.\u00a0185, ch.\u00a011, pp. 339\u2013401. IOS Press (February 2009)"},{"key":"13_CR40","doi-asserted-by":"crossref","unstructured":"Kleine B\u00fcning, H., Lettmann, T.: Aussagenlogik: Deduktion und Algorithmen. Leitf\u00e4den und Monographen der Informatik, B.G. Teubner Stuttgart (1994)","DOI":"10.1007\/978-3-322-84809-3"},{"key":"13_CR41","unstructured":"Kleine B\u00fcning, H., Lettmann, T.: Propositional Logic: Deduction and Algorithms. Cambridge University Press (1999)"},{"issue":"2","key":"13_CR42","doi-asserted-by":"publisher","first-page":"457","DOI":"10.2307\/2275541","volume":"62","author":"J. Kraj\u00ed\u010dek","year":"1997","unstructured":"Kraj\u00ed\u010dek, J.: Interpolation theorems, lower bounds for proof systems and independence results for bounded arithmetic. The Journal of Symbolic Logic\u00a062(2), 457\u2013486 (1997)","journal-title":"The Journal of Symbolic Logic"},{"key":"13_CR43","unstructured":"Kullmann, O.: Investigating a general hierarchy of polynomially decidable classes of CNF\u2019s based on short tree-like resolution proofs. Tech. Rep. TR99-041, Electronic Colloquium on Computational Complexity (ECCC) (October 1999), http:\/\/eccc.hpi-web.de\/report\/1999\/041\/"},{"issue":"1-2","key":"13_CR44","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/S0304-3975(98)00017-6","volume":"223","author":"O. Kullmann","year":"1999","unstructured":"Kullmann, O.: New methods for 3-SAT decision and worst-case analysis. Theoretical Computer Science\u00a0223(1-2), 1\u201372 (1999)","journal-title":"Theoretical Computer Science"},{"key":"13_CR45","doi-asserted-by":"crossref","unstructured":"Kullmann, O.: On a generalization of extended resolution. Discrete Applied Mathematics 96-97, 149\u2013176 (October 1999)","DOI":"10.1016\/S0166-218X(99)00037-2"},{"key":"13_CR46","unstructured":"Kullmann, O.: An improved version of width restricted resolution. In: Electronical Proceedings of Sixth International Symposium on Artificial Intelligence and Mathematics, 11 pages (January 2000), http:\/\/rutcor.rutgers.edu\/~amai\/aimath00\/AcceptedCont.htm"},{"issue":"3-4","key":"13_CR47","doi-asserted-by":"publisher","first-page":"303","DOI":"10.1023\/B:AMAI.0000012871.08577.0b","volume":"40","author":"O. Kullmann","year":"2004","unstructured":"Kullmann, O.: Upper and lower bounds on the complexity of generalised resolution and generalised constraint satisfaction problems. Annals of Mathematics and Artificial Intelligence\u00a040(3-4), 303\u2013352 (2004)","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"issue":"1","key":"13_CR48","doi-asserted-by":"crossref","first-page":"27","DOI":"10.3233\/FI-2011-428","volume":"109","author":"O. Kullmann","year":"2011","unstructured":"Kullmann, O.: Constraint satisfaction problems in clausal form I: Autarkies and deficiency. Fundamenta Informaticae\u00a0109(1), 27\u201381 (2011)","journal-title":"Fundamenta Informaticae"},{"issue":"3","key":"13_CR49","doi-asserted-by":"publisher","first-page":"1","DOI":"10.2168\/LMCS-9(3:15)2013","volume":"9","author":"J. Nordstr\u00f6m","year":"2013","unstructured":"Nordstr\u00f6m, J.: Pebble games, proof complexity, and time-space trade-offs. Logical Methods in Computer Science\u00a09(3), 1\u201363 (2013)","journal-title":"Logical Methods in Computer Science"},{"issue":"14","key":"13_CR50","doi-asserted-by":"publisher","first-page":"471","DOI":"10.4086\/toc.2013.v009a014","volume":"9","author":"J. Nordstr\u00f6m","year":"2013","unstructured":"Nordstr\u00f6m, J., H\u00e5stad, J.: Towards an optimal separation of space and length in resolution. Theory of Computing\u00a09(14), 471\u2013557 (2013)","journal-title":"Theory of Computing"},{"key":"13_CR51","doi-asserted-by":"crossref","unstructured":"Pudl\u00e1k, P.: Proofs as games. American Math. Monthly, 541\u2013550 (2000)","DOI":"10.1080\/00029890.2000.12005233"},{"key":"13_CR52","unstructured":"Pudl\u00e1k, P., Impagliazzo, R.: A lower bound for DLL algorithms for k-SAT (preliminary version). In: SODA, pp. 128\u2013136. ACM\/SIAM (2000)"},{"key":"13_CR53","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1016\/0020-0190(95)00019-9","volume":"54","author":"J.S. Schlipf","year":"1995","unstructured":"Schlipf, J.S., Annexstein, F.S., Franco, J.V., Swaminathan, R.: On finding solutions for extended Horn formulas. Information Processing Letters\u00a054, 133\u2013137 (1995)","journal-title":"Information Processing Letters"},{"key":"13_CR54","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"362","DOI":"10.1007\/3-540-48168-0_26","volume-title":"Computer Science Logic","author":"J. Tor\u00e1n","year":"1999","unstructured":"Tor\u00e1n, J.: Lower bounds for space in resolution. In: Flum, J., Rodr\u00edguez-Artalejo, M. (eds.) CSL 1999. LNCS, vol.\u00a01683, pp. 362\u2013373. Springer, Heidelberg (1999)"},{"key":"13_CR55","first-page":"86","volume":"83","author":"J. Tor\u00e1n","year":"2004","unstructured":"Tor\u00e1n, J.: Space and width in propositional resolution (Column: Computational Complexity). Bulletin of the European Association of Theoretical Computer Science (EATCS)\u00a083, 86\u2013104 (2004)","journal-title":"Bulletin of the European Association of Theoretical Computer Science (EATCS)"},{"key":"13_CR56","unstructured":"Tseitin, G.: On the complexity of derivation in propositional calculus. In: Seminars in Mathematics, vol. 8. V.A. Steklov Mathematical Institute, Leningrad (1968), English translation: Slisenko, A.O. (ed.) Studies in mathematics and mathematical logic, Part II, pp. 115\u2013125 (1970)"},{"key":"13_CR57","doi-asserted-by":"publisher","first-page":"349","DOI":"10.1007\/s11225-011-9356-9","volume":"99","author":"A. Urquhart","year":"2011","unstructured":"Urquhart, A.: The depth of resolution proofs. Studia Logica\u00a099, 349\u2013364 (2011)","journal-title":"Studia Logica"},{"key":"13_CR58","doi-asserted-by":"crossref","unstructured":"del Val, A.: Tractable databases: How to make propositional unit resolution complete through compilation. In: Proceedings of the 4th International Conference on Principles of Knowledge Representation and Reasoning (KR 1994), pp. 551\u2013561 (1994)","DOI":"10.1016\/B978-1-4832-1452-8.50146-9"},{"key":"13_CR59","doi-asserted-by":"crossref","unstructured":"Viennot, X.G.: Trees everywhere. In: Arnold, A. (ed.) CAAP 1990. LNCS, vol.\u00a0431, pp. 18\u201341. Springer, Heidelberg (1990)","DOI":"10.1007\/3-540-52590-4_38"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing \u2013 SAT 2014"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-09284-3_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,4,10]],"date-time":"2022-04-10T09:27:53Z","timestamp":1649582873000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-09284-3_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319092836","9783319092843"],"references-count":59,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-09284-3_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}