{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,19]],"date-time":"2026-03-19T04:41:33Z","timestamp":1773895293797,"version":"3.50.1"},"publisher-location":"Cham","reference-count":21,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319961415","type":"print"},{"value":"9783319961422","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-96142-2_18","type":"book-chapter","created":{"date-parts":[[2018,7,20]],"date-time":"2018-07-20T19:55:08Z","timestamp":1532116508000},"page":"275-293","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":12,"title":["The Proof Complexity of SMT Solvers"],"prefix":"10.1007","author":[{"given":"Robert","family":"Robere","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Antonina","family":"Kolokolova","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Vijay","family":"Ganesh","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,7,18]]},"reference":[{"key":"18_CR1","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":"18_CR2","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."},{"key":"18_CR3","unstructured":"Bj\u00f8rner, N., Dutertre, B., de Moura, L.: Accelerating lemma learning using joins - DPLL(Join). In: 15th International Conference on Logic for Programming Artificial Intelligence and Reasoning, LPAR 2008 (2008)"},{"key":"18_CR4","doi-asserted-by":"crossref","unstructured":"Balyo, T., Heule, M.J.H., J\u00e4rvisalo, M.: SAT competition 2016: recent developments. In: Singh, S.P., Markovitch, S. (eds.) Proceedings of the Thirty-First AAAI Conference on Artificial Intelligence, 4\u20139 February 2017, San Francisco, California, USA, pp. 5061\u20135063. AAAI Press (2017)","DOI":"10.1609\/aaai.v31i1.10641"},{"key":"18_CR5","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1613\/jair.1410","volume":"22","author":"P Beame","year":"2004","unstructured":"Beame, P., Kautz, H.A., Sabharwal, A.: Towards understanding and harnessing the potential of clause learning. J. Artif. Intell. Res. 22, 319\u2013351 (2004)","journal-title":"J. Artif. Intell. Res."},{"key":"18_CR6","doi-asserted-by":"crossref","unstructured":"Bj\u00f8rner, N., de Moura, L.: Tractability and modern SMT solvers. In: Bordeaux, L., Hamadi, Y., Kohli, P. (eds.) Tractability: Practical Approaches to Hard Problems, pp. 350\u2013377. Cambridge University Press (2014)","DOI":"10.1017\/CBO9781139177801.014"},{"issue":"1","key":"18_CR7","doi-asserted-by":"crossref","first-page":"36","DOI":"10.2307\/2273702","volume":"44","author":"SA Cook","year":"1979","unstructured":"Cook, S.A., Reckhow, R.A.: The relative efficiency of propositional proof systems. J. Symb. Log. 44(1), 36\u201350 (1979)","journal-title":"J. Symb. Log."},{"issue":"4","key":"18_CR8","doi-asserted-by":"crossref","first-page":"758","DOI":"10.1145\/322217.322228","volume":"27","author":"PJ Downey","year":"1980","unstructured":"Downey, P.J., Sethi, R., Tarjan, R.E.: Variations on the common subexpression problem. J. ACM (JACM) 27(4), 758\u2013771 (1980)","journal-title":"J. ACM (JACM)"},{"key":"18_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"519","DOI":"10.1007\/978-3-540-73368-3_52","volume-title":"Computer Aided Verification","author":"V Ganesh","year":"2007","unstructured":"Ganesh, V., Dill, D.L.: A Decision procedure for bit-vectors and arrays. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 519\u2013531. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-73368-3_52"},{"key":"18_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/978-3-540-27813-9_14","volume-title":"Computer Aided Verification","author":"H Ganzinger","year":"2004","unstructured":"Ganzinger, H., Hagen, G., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: DPLL(T): fast decision procedures. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 175\u2013188. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-27813-9_14"},{"key":"18_CR11","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-24508-4","volume-title":"Boolean Function Complexity: Advances and Frontiers","author":"S Jukna","year":"2012","unstructured":"Jukna, S.: Boolean Function Complexity: Advances and Frontiers. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-24508-4"},{"issue":"04","key":"18_CR12","doi-asserted-by":"crossref","first-page":"1582","DOI":"10.2307\/2586668","volume":"63","author":"J Kraj\u00ed\u010dek","year":"1998","unstructured":"Kraj\u00ed\u010dek, J.: Discretely ordered modules as a first-order extension of the cutting planes proof system. J. Symb. Log. 63(04), 1582\u20131596 (1998)","journal-title":"J. Symb. Log."},{"issue":"6","key":"18_CR13","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. J. ACM 53(6), 937\u2013977 (2006)","journal-title":"J. ACM"},{"key":"18_CR14","unstructured":"Oliveras, A., Rodr1guez-Carbonell, E.: Combining decision procedures: the Nelson-Oppen approach. Techniques (2009)"},{"issue":"2","key":"18_CR15","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(2), 512\u2013525 (2011)","journal-title":"Artif. Intell."},{"issue":"3","key":"18_CR16","doi-asserted-by":"crossref","first-page":"194","DOI":"10.1016\/j.apal.2008.04.001","volume":"155","author":"R Raz","year":"2008","unstructured":"Raz, R., Tzameret, I.: Resolution over linear equations and multilinear proofs. Annals Pure Appl. Log. 155(3), 194\u2013224 (2008)","journal-title":"Annals Pure Appl. Log."},{"key":"18_CR17","unstructured":"The Annual SMTCOMP Competition Website. http:\/\/www.smtcomp.org"},{"key":"18_CR18","unstructured":"Tinelli, C.: Foundations of Lazy SMT and DPLL(T) (2012)"},{"key":"18_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"190","DOI":"10.1007\/978-3-540-79723-4_18","volume-title":"Parameterized and Exact Computation","author":"P Traxler","year":"2008","unstructured":"Traxler, P.: The time complexity of constraint satisfaction. In: Grohe, M., Niedermeier, R. (eds.) IWPEC 2008. LNCS, vol. 5018, pp. 190\u2013201. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-79723-4_18"},{"key":"18_CR20","unstructured":"The Yices SMT Solver. http:\/\/yices.csl.sri.com\/"},{"key":"18_CR21","unstructured":"The Z3 Theorem Prover. https:\/\/github.com\/Z3Prover"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-96142-2_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,8,28]],"date-time":"2022-08-28T00:26:45Z","timestamp":1661646405000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-96142-2_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319961415","9783319961422"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-96142-2_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018]]}}}