{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T04:46:50Z","timestamp":1725857210051},"publisher-location":"Cham","reference-count":33,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319409696"},{"type":"electronic","value":"9783319409702"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"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":[[2016]]},"DOI":"10.1007\/978-3-319-40970-2_11","type":"book-chapter","created":{"date-parts":[[2016,6,10]],"date-time":"2016-06-10T11:14:55Z","timestamp":1465557295000},"page":"160-176","source":"Crossref","is-referenced-by-count":6,"title":["Trade-offs Between Time and Memory in a Tighter Model of CDCL SAT Solvers"],"prefix":"10.1007","author":[{"given":"Jan","family":"Elffers","sequence":"first","affiliation":[]},{"given":"Jan","family":"Johannsen","sequence":"additional","affiliation":[]},{"given":"Massimo","family":"Lauria","sequence":"additional","affiliation":[]},{"given":"Thomas","family":"Magnard","sequence":"additional","affiliation":[]},{"given":"Jakob","family":"Nordstr\u00f6m","sequence":"additional","affiliation":[]},{"given":"Marc","family":"Vinyals","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,6,11]]},"reference":[{"issue":"4","key":"11_CR1","doi-asserted-by":"crossref","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 J. Comput. 31(4), 1184\u20131211 (2002). Preliminary version in STOC 2000","journal-title":"SIAM J. Comput."},{"issue":"4","key":"11_CR2","doi-asserted-by":"crossref","first-page":"1347","DOI":"10.1137\/06066850X","volume":"38","author":"M Alekhnovich","year":"2008","unstructured":"Alekhnovich, M., Razborov, A.A.: Resolution is not automatizable unless W[P] is tractable. SIAM J. Comput. 38(4), 1347\u20131363 (2008). Preliminary version in FOCS 2001","journal-title":"SIAM J. Comput."},{"key":"11_CR3","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). Preliminary version in SAT 2009","journal-title":"J. Artif. Intell. Res."},{"key":"11_CR4","unstructured":"Audemard, G., Simon, L.: Predicting learnt clauses quality in modern SAT solvers. In: Proceedings of the 21st International Joint Conference on Artificial Intelligence (IJCAI 2009), pp. 399\u2013404, July 2009"},{"key":"11_CR5","unstructured":"Bayardo Jr., R.J., Schrag, R.: Using CSP look-back techniques to solve real-world SAT instances. In: Proceedings of the 14th National Conference on Artificial Intelligence (AAAI 1997), pp. 203\u2013208, July 1997"},{"key":"11_CR6","doi-asserted-by":"crossref","unstructured":"Beame, P., Beck, C., Impagliazzo, R.: Time-space tradeoffs in resolution: superpolynomial lower bounds for superlinear space. In: Proceedings of the 44th Annual ACM Symposium on Theory of Computing (STOC 2012), pp. 213\u2013232, May 2012","DOI":"10.1145\/2213977.2213999"},{"key":"11_CR7","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. J. Artif. Intell. Res. 22, 319\u2013351 (2004). Preliminary version in IJCAI 2003","journal-title":"J. Artif. Intell. Res."},{"key":"11_CR8","doi-asserted-by":"crossref","unstructured":"Beame, P., Sabharwal, A.: Non-restarting SAT solvers with simple preprocessing can efficiently simulate resolution. In: Proceedings of the 28th National Conference on Artificial Intelligence (AAAI 2014), pp. 2608\u20132615. AAAI Press, July 2014","DOI":"10.1609\/aaai.v28i1.9121"},{"key":"11_CR9","doi-asserted-by":"crossref","unstructured":"Beck, C., Nordstr\u00f6m, J., Tang, B.: Some trade-off results for polynomial calculus. In: Proceedings of the 45th Annual ACM Symposium on Theory of Computing (STOC 2013), pp. 813\u2013822, May 2013","DOI":"10.1145\/2488608.2488711"},{"issue":"1","key":"11_CR10","doi-asserted-by":"crossref","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 Struct. Algorithms 23(1), 92\u2013109 (2003). Preliminary version in CCC 2001","journal-title":"Random Struct. Algorithms"},{"key":"11_CR11","unstructured":"Ben-Sasson, E., Nordstr\u00f6m, J.: Understanding space in proof complexity: separations and trade-offs via substitutions. In: Proceedings of the 2nd Symposium on Innovations in Computer Science (ICS 2011). pp. 401\u2013416, January 2011"},{"issue":"2","key":"11_CR12","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\u2013resolution madesimple. J. ACM 48(2), 149\u2013169 (2001). Preliminary version in STOC 1999","journal-title":"J. ACM"},{"key":"11_CR13","unstructured":"Bennett, P., Bonacina, I., Galesi, N., Huynh, T., Molloy, M., Wollan, P.: Space proof complexity for random 3-CNFs. Technical report arXiv.org:1503.01613 , April 2015"},{"key":"11_CR14","unstructured":"Blake, A.: Canonical Expressions in Boolean Algebra. Ph.D. thesis, University of Chicago (1937)"},{"key":"11_CR15","unstructured":"Bonacina, I.: Total space in resolution is at least width squared. In: Proceedings of the 43rd International Colloquium on Automata, Languages and Programming (ICALP 2016), (to appear, July 2016)"},{"key":"11_CR16","doi-asserted-by":"crossref","unstructured":"Bonacina, I., Galesi, N., Thapen, N.: Total space in resolution. In: Proceedings of the 55th Annual IEEE Symposium on Foundations of Computer Science (FOCS 2014), pp. 641\u2013650, October 2014","DOI":"10.1109\/FOCS.2014.74"},{"key":"11_CR17","doi-asserted-by":"crossref","first-page":"669","DOI":"10.1613\/jair.4260","volume":"49","author":"ML Bonet","year":"2014","unstructured":"Bonet, M.L., Buss, S., Johannsen, J.: Improved separations of regular resolution from clause learning proof systems. J. Artif. Intell. Res. 49, 669\u2013703 (2014)","journal-title":"J. Artif. Intell. Res."},{"issue":"4:13","key":"11_CR18","first-page":"1","volume":"4","author":"SR Buss","year":"2008","unstructured":"Buss, S.R., Hoffmann, J., Johannsen, J.: Resolution trees with lemmas: resolution refinements that characterize DLL-algorithms with clause learning. Logical Meth. Comput. Sci. 4(4:13), 1\u201328 (2008)","journal-title":"Logical Meth. Comput. Sci."},{"key":"11_CR19","first-page":"1","volume":"10","author":"SR Buss","year":"2014","unstructured":"Buss, S.R., Ko\u0142odziejczyk, L.: Small stone in pool. Logical Meth. Comput. Sci. 10, 1\u201322 (2014)","journal-title":"Logical Meth. Comput. Sci."},{"issue":"4","key":"11_CR20","doi-asserted-by":"crossref","first-page":"759","DOI":"10.1145\/48014.48016","volume":"35","author":"V Chv\u00e1tal","year":"1988","unstructured":"Chv\u00e1tal, V., Szemer\u00e9di, E.: Many hard examples for resolution. J. ACM 35(4), 759\u2013768 (1988)","journal-title":"J. ACM"},{"issue":"1","key":"11_CR21","doi-asserted-by":"crossref","first-page":"36","DOI":"10.2307\/2273702","volume":"44","author":"SA Cook","year":"1979","unstructured":"Cook, S.A., Reckhow, R.: The relative efficiency of propositional proof systems. J. Symbolic Logic 44(1), 36\u201350 (1979)","journal-title":"J. Symbolic Logic"},{"issue":"7","key":"11_CR22","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":"11_CR23","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"},{"issue":"1","key":"11_CR24","doi-asserted-by":"crossref","first-page":"84","DOI":"10.1006\/inco.2001.2921","volume":"171","author":"JL Esteban","year":"2001","unstructured":"Esteban, J.L., Tor\u00e1n, J.: Space bounds for resolution. Inf. Comput. 171(1), 84\u201397 (2001). Preliminary versions of these results appeared in STACS 1999 and CSL 1999","journal-title":"Inf. Comput."},{"issue":"2\u20133","key":"11_CR25","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(2\u20133), 297\u2013308 (1985)","journal-title":"Theor. Comput. Sci."},{"key":"11_CR26","unstructured":"Hertel, P., Bacchus, F., Pitassi, T., Van Gelder, A.: Clause learning can effectively P-simulate general propositional resolution. In: Proceedings of the 23rd National Conference on Artificial Intelligence (AAAI 2008), pp. 283\u2013290, July 2008"},{"issue":"5","key":"11_CR27","doi-asserted-by":"crossref","first-page":"506","DOI":"10.1109\/12.769433","volume":"48","author":"JP Marques-Silva","year":"1999","unstructured":"Marques-Silva, J.P., Sakallah, K.A.: GRASP: a search algorithm for propositional satisfiability. IEEE Trans. Comput. 48(5), 506\u2013521 (1999). Preliminary version in ICCAD 1996","journal-title":"IEEE Trans. Comput."},{"key":"11_CR28","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, June 2001","DOI":"10.1145\/378239.379017"},{"issue":"6","key":"11_CR29","doi-asserted-by":"crossref","first-page":"937","DOI":"10.1145\/1217856.1217859","volume":"53","author":"R Nieuwenhuis","year":"2006","unstructured":"Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT modulo theories: from an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T). J. ACM 53(6), 937\u2013977 (2006)","journal-title":"J. ACM"},{"key":"11_CR30","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). Preliminary version in CP 2009","journal-title":"Artif. Intell."},{"issue":"1","key":"11_CR31","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(1), 209\u2013219 (1987)","journal-title":"J. ACM"},{"key":"11_CR32","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"crossref","first-page":"580","DOI":"10.1007\/11591191_40","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"A Gelder Van","year":"2005","unstructured":"Van Gelder, A.: Pool resolution and its relation to regular resolution and DPLL with clause learning. In: Sutcliffe, G., Voronkov, A. (eds.) LPAR 2005. LNCS (LNAI), vol. 3835, pp. 580\u2013594. Springer, Heidelberg (2005)"},{"key":"11_CR33","unstructured":"Zhang, L., Madigan, C.F., Moskewicz, M.W., Malik, S.: Efficient conflict driven learning in boolean satisfiability solver. In: Proceedings of the IEEE\/ACM International Conference on Computer-Aided Design (ICCAD 2001), pp. 279\u2013285, November 2001"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing \u2013 SAT 2016"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-40970-2_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,7,1]],"date-time":"2022-07-01T12:13:49Z","timestamp":1656677629000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-40970-2_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319409696","9783319409702"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-40970-2_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}