{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T15:22:44Z","timestamp":1725895364756},"publisher-location":"Berlin, Heidelberg","reference-count":33,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642335570"},{"type":"electronic","value":"9783642335587"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-33558-7_25","type":"book-chapter","created":{"date-parts":[[2012,10,3]],"date-time":"2012-10-03T02:32:47Z","timestamp":1349231567000},"page":"316-331","source":"Crossref","is-referenced-by-count":10,"title":["Relating Proof Complexity Measures and Practical Hardness of SAT"],"prefix":"10.1007","author":[{"given":"Matti","family":"J\u00e4rvisalo","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Arie","family":"Matsliah","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jakob","family":"Nordstr\u00f6m","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stanislav","family":"\u017divn\u00fd","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"25_CR1","unstructured":"Biere, A., Heule, M.J.H., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol.\u00a0185. IOS Press (2009)"},{"issue":"5","key":"25_CR2","doi-asserted-by":"publisher","first-page":"506","DOI":"10.1109\/12.769433","volume":"48","author":"J.P. Marques-Silva","year":"1999","unstructured":"Marques-Silva, J.P., Sakallah, K.A.: GRASP: a search algorithm for propositional satisfiability. IEEE Trans. Computers\u00a048(5), 506\u2013521 (1999)","journal-title":"IEEE Trans. Computers"},{"key":"25_CR3","doi-asserted-by":"crossref","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient SAT solver. In: Proc. DAC, pp. 530\u2013535. ACM (2001)","DOI":"10.1145\/378239.379017"},{"key":"25_CR4","unstructured":"Marques-Silva, J.P., Lynce, I., Malik, S.: Conflict-driven clause learning SAT solvers. In: [1], pp. 131\u2013153"},{"issue":"7","key":"25_CR5","doi-asserted-by":"publisher","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. Communications of the ACM\u00a05(7), 394\u2013397 (1962)","journal-title":"Communications of the ACM"},{"issue":"3","key":"25_CR6","doi-asserted-by":"publisher","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. Journal of the ACM\u00a07(3), 201\u2013215 (1960)","journal-title":"Journal of the ACM"},{"key":"25_CR7","doi-asserted-by":"crossref","unstructured":"Buss, S.R., Hoffmann, J., Johannsen, J.: Resolution trees with lemmas: Resolution refinements that characterize DLL-algorithms with clause learning. Logical Methods in Computer Science 4(4:13) (2008)","DOI":"10.2168\/LMCS-4(4:13)2008"},{"key":"25_CR8","doi-asserted-by":"publisher","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. Artificial Intelligence\u00a0175, 512\u2013525 (2011)","journal-title":"Artificial Intelligence"},{"key":"25_CR9","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. Journal of Artificial Intelligence Research\u00a040, 353\u2013373 (2011)","journal-title":"Journal of Artificial Intelligence Research"},{"key":"25_CR10","doi-asserted-by":"crossref","unstructured":"Alekhnovich, M., Razborov, A.A.: Resolution is not automatizable unless W[P] is tractable. In: Proc. FOCS, pp. 210\u2013219. IEEE (2001)","DOI":"10.1109\/SFCS.2001.959895"},{"issue":"4","key":"25_CR11","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/s000370100000","volume":"10","author":"M.L. Bonet","year":"2001","unstructured":"Bonet, M.L., Galesi, N.: Optimality of size-width tradeoffs for resolution. Computational Complexity\u00a010(4), 261\u2013276 (2001)","journal-title":"Computational Complexity"},{"issue":"3","key":"25_CR12","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(3), 323\u2013334 (2008)","journal-title":"Journal of Computer and System Sciences"},{"key":"25_CR13","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. FOCS, pp. 709\u2013718. IEEE (2008)","DOI":"10.1109\/FOCS.2008.42"},{"key":"25_CR14","unstructured":"Ans\u00f3tegui, C., Bonet, M.L., Levy, J., Many\u00e0, F.: Measuring the hardness of SAT instances. In: Proc. AAAI, pp. 222\u2013228. AAAI Press (2008)"},{"issue":"1","key":"25_CR15","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. Inf. Comput.\u00a0171(1), 84\u201397 (2001)","journal-title":"Inf. Comput."},{"issue":"6","key":"25_CR16","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":"25_CR17","unstructured":"Williams, R., Gomes, C.P., Selman, B.: Backdoors to typical case complexity. In: Proc. IJCAI, pp. 1173\u20131178. Morgan Kaufmann (2003)"},{"key":"25_CR18","doi-asserted-by":"crossref","unstructured":"Nordstr\u00f6m, J.: Pebble games, proof complexity and time-space trade-offs. Logical Methods in Computer Science (to appear, 2012), \n                    \n                      http:\/\/www.csc.kth.se\/~jakobn\/research","DOI":"10.2168\/LMCS-9(3:15)2013"},{"issue":"2-3","key":"25_CR19","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. Comp. Sci.\u00a039(2-3), 297\u2013308 (1985)","journal-title":"Theoret. Comp. Sci."},{"issue":"1","key":"25_CR20","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1145\/7531.8928","volume":"34","author":"A. Urquhart","year":"1987","unstructured":"Urquhart, A.: Hard examples for resolution. Journal of the ACM\u00a034(1), 209\u2013219 (1987)","journal-title":"Journal of the ACM"},{"issue":"2","key":"25_CR21","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\u2014resolution made simple. Journal of the ACM\u00a048(2), 149\u2013169 (2001)","journal-title":"Journal of the ACM"},{"issue":"4","key":"25_CR22","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","key":"25_CR23","doi-asserted-by":"publisher","first-page":"92","DOI":"10.1002\/rsa.10089","volume":"23","author":"E. Ben-Sasson","year":"2003","unstructured":"Ben-Sasson, E., Galesi, N.: Space complexity of random formulae in resolution. Random Structures and Algorithms\u00a023(1), 92\u2013109 (2003)","journal-title":"Random Structures and Algorithms"},{"key":"25_CR24","unstructured":"Nordstr\u00f6m, J.: New wine into old wineskins: A survey of some pebbling classics with supplemental results. Foundations and Trends in Theoretical Computer Science (to appear, 2012), Draft version available at \n                    \n                      http:\/\/www.csc.kth.se\/~jakobn\/research\/"},{"key":"25_CR25","unstructured":"Ben-Sasson, E., Nordstr\u00f6m, J.: Understanding space in proof complexity: Separations and trade-offs via substitutions. In: Proc. ICS, pp. 401\u2013416 (2011)"},{"issue":"1","key":"25_CR26","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1137\/060668250","volume":"39","author":"J. Nordstr\u00f6m","year":"2009","unstructured":"Nordstr\u00f6m, J.: Narrow proofs may be spacious: Separating space and width in resolution. SIAM Journal on Computing\u00a039(1), 59\u2013121 (2009)","journal-title":"SIAM Journal on Computing"},{"key":"25_CR27","doi-asserted-by":"crossref","unstructured":"Nordstr\u00f6m, J., H\u00e5stad, J.: Towards an optimal separation of space and length in resolution (Extended abstract). In: Proc. STOC, pp. 701\u2013710 (2008)","DOI":"10.1145\/1374376.1374478"},{"key":"25_CR28","unstructured":"Gilbert, J.R., Tarjan, R.E.: Variations of a pebble game on graphs. Technical Report STAN-CS-78-661, Stanford University (1978)"},{"key":"25_CR29","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1613\/jair.1410","volume":"22","author":"P. Beame","year":"2004","unstructured":"Beame, P., Kautz, H., Sabharwal, A.: Towards understanding and harnessing the potential of clause learning. Journal of Artificial Intelligence Research\u00a022, 319\u2013351 (2004)","journal-title":"Journal of Artificial Intelligence Research"},{"key":"25_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"502","DOI":"10.1007\/978-3-540-24605-3_37","volume-title":"Theory and Applications of Satisfiability Testing","author":"N. E\u00e9n","year":"2004","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An Extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol.\u00a02919, pp. 502\u2013518. Springer, Heidelberg (2004)"},{"key":"25_CR31","unstructured":"Biere, A.: Lingeling, Plingeling, PicoSAT and PrecoSAT at SAT Race 2010. FMV Tech. Report 10\/1, Johannes Kepler University (2010)"},{"key":"25_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/978-3-642-02777-2_9","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2009","author":"B. Dilkina","year":"2009","unstructured":"Dilkina, B., Gomes, C.P., Sabharwal, A.: Backdoors in the Context of Learning. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol.\u00a05584, pp. 73\u201379. Springer, Heidelberg (2009)"},{"key":"25_CR33","doi-asserted-by":"crossref","unstructured":"Beame, P., Beck, C., Impagliazzo, R.: Time-space tradeoffs in resolution: Superpolynomial lower bounds for superlinear space. In: Proc. STOC, pp. 213\u2013232. ACM (2012)","DOI":"10.1145\/2213977.2213999"}],"container-title":["Lecture Notes in Computer Science","Principles and Practice of Constraint Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-33558-7_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,8]],"date-time":"2019-05-08T03:22:58Z","timestamp":1557285778000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-33558-7_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642335570","9783642335587"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-33558-7_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}