{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T11:03:53Z","timestamp":1725879833096},"publisher-location":"Cham","reference-count":53,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319418414"},{"type":"electronic","value":"9783319418421"}],"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"},{"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-41842-1_12","type":"book-chapter","created":{"date-parts":[[2017,2,1]],"date-time":"2017-02-01T17:01:15Z","timestamp":1485968475000},"page":"315-335","source":"Crossref","is-referenced-by-count":0,"title":["DPLL: The Core of Modern Satisfiability Solvers"],"prefix":"10.1007","author":[{"given":"Donald","family":"Loveland","sequence":"first","affiliation":[]},{"given":"Ashish","family":"Sabharwal","sequence":"additional","affiliation":[]},{"given":"Bart","family":"Selman","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,1,31]]},"reference":[{"key":"12_CR1","unstructured":"Audemard, G.,\u00a0&\u00a0Simon, L. (2009, July). Predicting learnt clauses quality in modern SAT solvers. In 21st IJCAI (pp. 399\u2013404), Pasadena, CA."},{"key":"12_CR2","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. (2004). Understanding and harnessing the potential of clause learning. JAIR, 22, 319\u2013351.","journal-title":"JAIR"},{"key":"12_CR3","unstructured":"\u00a0Biere, A. (2012). Plingeling: Solver description. In SAT Challenge 2012."},{"key":"12_CR4","unstructured":"Biere, A.,\u00a0Heule, M.,\u00a0van Maaren, H.,\u00a0&\u00a0Walsh, T. (Eds.) (2009). Handbook of satisfiability. IOS Press."},{"key":"12_CR5","unstructured":"Bloom, B.,\u00a0Grove, D.,\u00a0Herta, B.,\u00a0Sabharwal, A.,\u00a0Samulowitz, H., & Saraswat, V.\u00a0A. (2012). SatX10: A scalable plug&play parallel sat framework\u2014(tool presentation). In 15th SAT (pp. 463\u2013468)."},{"issue":"3\u20134","key":"12_CR6","doi-asserted-by":"crossref","first-page":"381","DOI":"10.1007\/BF02127976","volume":"17","author":"M B\u00f6hm","year":"1996","unstructured":"B\u00f6hm, M., & Speckenmeyer, E. (1996). A fast parallel SAT-solver\u2014efficient workload balancing. Annals of Mathematics and Artificial Intelligence, 17(3\u20134), 381\u2013400.","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"key":"12_CR7","doi-asserted-by":"crossref","unstructured":"Cook, S.\u00a0A. (1971, May). The complexity of theorem proving procedures. In Conference Record of 3rd STOC (pp. 151\u2013158), Shaker Heights, OH.","DOI":"10.1145\/800157.805047"},{"key":"12_CR8","doi-asserted-by":"crossref","unstructured":"Davis, M. (1983). A computer program for Presburger\u2019s algorithm. In J.\u00a0Siekmann and G.\u00a0Wrightson (Eds.) Automated reasoning: Classical papers on computational logic (pp. 41\u201348). Springer.","DOI":"10.1007\/978-3-642-81952-0_3"},{"key":"12_CR9","unstructured":"\u00a0Davis, M. (2014). Private communication."},{"key":"12_CR10","unstructured":"Davis, M. (2015). My life as a logician. In this volume. Springer."},{"key":"12_CR11","doi-asserted-by":"crossref","unstructured":"Davis, M.,\u00a0Logemann, G.,\u00a0&\u00a0Loveland, D. (1962) A machine program for theorem-proving. Communication of ACM, 5, 394\u2013397. ISSN: 0001-0782.","DOI":"10.1145\/368273.368557"},{"key":"12_CR12","doi-asserted-by":"crossref","unstructured":"Davis, M.,\u00a0&\u00a0Putnam, H. (1960). A computing procedure for quantification theory. Journal of the Association for Computing Machinery, 7, 201\u2013215. ISSN: 0004-5411.","DOI":"10.1145\/321033.321034"},{"key":"12_CR13","unstructured":"Dunham, B.,\u00a0Fridshal, R.,\u00a0&\u00a0Sward, G. (1959). A non-heuristic program for proving elementary logical theorems. In IFIP Congress (pp. 282\u2013284)."},{"key":"12_CR14","first-page":"19","volume":"2","author":"B Dunham","year":"1959","unstructured":"Dunham, B., Fridshal, R., & Sward, G. (1959). A non-heuristic program for proving elementary logical theorems (abstract). CACM, 2, 19\u201320.","journal-title":"CACM"},{"key":"12_CR15","unstructured":"E\u00e9n, N.,\u00a0&\u00a0S\u00f6rensson, N. (2005, June). MiniSat: A SAT solver with conflict-clause minimization. In 8th SAT, St. Andrews, U.K."},{"key":"12_CR16","unstructured":"Frost, D.,\u00a0Rish, I.,\u00a0&\u00a0Vila, L. (1997). Summarizing CSP hardness with continuous probability distributions. In Proceedings of the Fourteenth National Conference on Artificial Intelligence (AAAI-97) (pp. 327\u2013334). New Providence, RI: AAAI Press."},{"key":"12_CR17","unstructured":"\u00a0Gelernter, H. (1960). Realization of a geometry theorem proving machine. In Information processing (pp. 273\u2013282). UNESCO, Paris: R. Oldenbourg, Munich: Butterworths, London."},{"key":"12_CR18","doi-asserted-by":"crossref","unstructured":"Gelernter, H., Hansen, J.\u00a0R.,\u00a0 & Loveland, D.\u00a0W. (1960). Empirical explorations of the geometry theorem machine. In Papers presented at the May 3\u20135, 1960, Western Joint IRE-AIEE-ACM computer conference (pp. 143\u2013149). ACM.","DOI":"10.1145\/1460361.1460381"},{"key":"12_CR19","unstructured":"\u00a0Gelfond, M. (2008). Answer sets. In F.\u00a0van Harmelen, V.\u00a0Lifschitz and B.\u00a0Porter (Eds.), Handbook of knowledge representation. Foundations of artificial intelligence, Chapter\u00a07 (Vol.\u00a03, pp. 285\u2013316). Elsevier."},{"key":"12_CR20","unstructured":"\u00a0Gilmore, P. (1958). Private communication."},{"key":"12_CR21","unstructured":"Gilmore, P.\u00a0C. (1959). A program for the production of proofs of theorems derivable within the first order predicate calculus. In CACM (Vol.\u00a02, pp. 19\u201319). ACM."},{"key":"12_CR22","doi-asserted-by":"crossref","unstructured":"Gilmore, P.\u00a0C. (1960). A proof method for quantification theory: Its justification and realization. IBM Journal of Research and Development, 4, 28\u201335. ISSN: 0018-8646.","DOI":"10.1147\/rd.41.0028"},{"issue":"12","key":"12_CR23","doi-asserted-by":"crossref","first-page":"1549","DOI":"10.1016\/j.dam.2006.10.007","volume":"155","author":"E Goldberg","year":"2007","unstructured":"Goldberg, E., & Novikov, Y. (2007). BerkMin: A fast and robust SAT-solver. Discrete Applied Mathematics, 155(12), 1549\u20131561.","journal-title":"Discrete Applied Mathematics"},{"key":"12_CR24","doi-asserted-by":"crossref","unstructured":"Gomes, C.,\u00a0Kautz, H.,\u00a0Sabharwal, A.,\u00a0&\u00a0Selman, B. (2008). Satisfiability solvers. In F.\u00a0Van\u00a0Harmelen, V.\u00a0Lifschitz and B.\u00a0Porter (Eds.), Handbook of knowledge representation (pp. 89\u2013134). Elsevier.","DOI":"10.1016\/S1574-6526(07)03002-7"},{"key":"12_CR25","doi-asserted-by":"crossref","unstructured":"Gomes, C.,\u00a0Selman, B.,\u00a0&\u00a0Crato, N. (1997). Heavy-tailed distributions in combinatorial search. In 3rd CP (pp. 121\u2013135).","DOI":"10.1007\/BFb0017434"},{"key":"12_CR26","unstructured":"Gomes, C.\u00a0P.,\u00a0Selman, B.,\u00a0&\u00a0Kautz, H. (1998, July). Boosting combinatorial search through randomization. In 15th AAAI (pp. 431\u2013437), Madison, WI."},{"issue":"4","key":"12_CR27","first-page":"245","volume":"6","author":"Y Hamadi","year":"2009","unstructured":"Hamadi, Y., Jabbour, S., & Sais, L. (2009). Manysat: A parallel SAT solver. Journal on Satisfiability, 6(4), 245\u2013262.","journal-title":"Journal on Satisfiability"},{"key":"12_CR28","unstructured":"Hamadi, Y.,\u00a0 & Wintersteiger, C.\u00a0M. (2012). Seven challenges in parallel SAT solving. In 26th AAAI."},{"key":"12_CR29","unstructured":"Hogg, T.,\u00a0&\u00a0Williams, C. (1994). Expected gains from parallelizing constraint solving for hard problems. In Proceedings of the Twelfth National Conference on Artificial Intelligence (AAAI-94) (pp. 1310\u20131315). Seattle, WA: AAAI Press."},{"key":"12_CR30","doi-asserted-by":"crossref","unstructured":"Jeroslow, R.\u00a0G.,\u00a0&\u00a0Wang, J. (1990). Solving propositional satisfiability problems. Annals of Mathematics and Artificial Intelligence, 1(1-4), 167\u2013187.","DOI":"10.1007\/BF01531077"},{"key":"12_CR31","doi-asserted-by":"crossref","unstructured":"Katsirelos, G.,\u00a0Sabharwal, A.,\u00a0Samulowitz, H.,\u00a0&\u00a0Simon, L. (2013). Resolution and parallelizability: Barriers to the efficient parallelization of SAT solvers. In 27th AAAI.","DOI":"10.1609\/aaai.v27i1.8660"},{"key":"12_CR32","unstructured":"Kautz, H.,\u00a0&\u00a0Selman, B. (1996). Pushing the envelope: Planning, propositional logic, and stochastic search. In Proceedings of AAAI-96, Portland, OR."},{"key":"12_CR33","unstructured":"Levin, L.\u00a0A. (1973). Universal sequential search problems. Problems of Information Transmission, 9(3), 265\u2013266. Originally in Russian."},{"key":"12_CR34","doi-asserted-by":"crossref","unstructured":"Marques-Silva, J.\u00a0P. (1999, September). The impact of branching heuristics in propositional satisfiability algorithms. In 9th Portuguese Conference on AI. LNCS (Vol. 1695, pp. 62\u201374).","DOI":"10.1007\/3-540-48159-1_5"},{"key":"12_CR35","unstructured":"Marques-Silva, J.\u00a0P.,\u00a0 & Sakallah, K.\u00a0A. (1996, November). GRASP\u2014a new search algorithm for satisfiability. In ICCAD (pp. 220\u2013227), San Jose, CA."},{"issue":"1\u20132","key":"12_CR36","doi-asserted-by":"crossref","first-page":"111","DOI":"10.1016\/0004-3702(95)00049-6","volume":"81","author":"D Mitchell","year":"1996","unstructured":"Mitchell, D., & Levesque, H. (1996). Some pitfalls for experimenters with random SAT. Artificial Intelligence, 81(1\u20132), 111\u2013125.","journal-title":"Artificial Intelligence"},{"key":"12_CR37","doi-asserted-by":"crossref","unstructured":"Moskewicz, M.\u00a0W., Madigan, C.\u00a0F.,\u00a0Zhao, Y.,\u00a0Zhang, L.,\u00a0&\u00a0Malik, S. (2001, June). Chaff: Engineering an efficient SAT solver. In 38th DAC (pp. 530\u2013535), Las Vegas, NV.","DOI":"10.1145\/378239.379017"},{"key":"12_CR38","unstructured":"\u00a0Nadel, A. (2002). Backtrack search algorithms for propositional logic satisfiability: Review and innovations. Master\u2019s thesis, Hebrew University of Jerusalem."},{"key":"12_CR39","doi-asserted-by":"crossref","unstructured":"Newell, A., Shaw, J. C., & Simon, H. (1957). Empirical explorations with the logic theory machine: A case study in heuristics. Western Joint Comp. Conf., 1, 49\u201373.","DOI":"10.1145\/1455567.1455605"},{"issue":"6","key":"12_CR40","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. (2006). Solving SAT and SAT modulo theories: From an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T). Journal of Association for Computing Machinery, 53(6), 937\u2013977.","journal-title":"Journal of Association for Computing Machinery"},{"issue":"3","key":"12_CR41","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1080\/0952813X.2014.954274","volume":"27","author":"AD Pal\u00f9","year":"2015","unstructured":"Pal\u00f9, A. D., Dovier, A., Formisano, A., & Pontelli, E. (2015). CUD@SAT: SAT solving on GPUs. Journal of Experimental and Theoretical Artificial Intelligence, 27(3), 293\u2013316.","journal-title":"Journal of Experimental and Theoretical Artificial Intelligence"},{"key":"12_CR42","unstructured":"Pipatsrisawat, K.,\u00a0&\u00a0Darwiche, A. (2006). RSat 1.03: SAT solver description. Technical Report D-152, Automated Reasoning Group, Computer Science Department, UCLA."},{"issue":"2","key":"12_CR43","first-page":"512","volume":"175","author":"K Pipatsrisawat","year":"2011","unstructured":"Pipatsrisawat, K., & Darwiche, A. (2011). On the power of clause-learning SAT solvers as resolution engines. AI Journal, 175(2), 512\u2013525.","journal-title":"AI Journal"},{"key":"12_CR44","unstructured":"Selman, B.,\u00a0Kautz, H.,\u00a0&\u00a0Cohen, B. (1996). Local search strategies for satisfiability testing. In D.\u00a0S. Johnson and M.\u00a0A. Trick (Eds.), Cliques, coloring, and satisfiability: The second DIMACS implementation challenge. DIMACS Series in Discrete Mathematics and Theoretical Computer Science (Vol.\u00a026, pp. 521\u2013532). American Mathematical Society."},{"key":"12_CR45","unstructured":"\u00a0Selman, B., Levesque, H.\u00a0J., & Mitchell, D.\u00a0G. (1992, July). A new method for solving hard satisfiability problems. In 10th AAAI (pp. 440\u2013446), San Jose, CA."},{"key":"12_CR46","unstructured":"Siekmann, J., & Wrightson, G. (Eds.) (1983). Automation of Reasoning1: Classical Papers on Computational Logic 1957\u20131966. Springer Publishing Company Incorporated."},{"key":"12_CR47","first-page":"135","volume":"9","author":"RM Stallman","year":"1977","unstructured":"Stallman, R. M., & Sussman, G. J. (1977). Forward reasoning and dependency-directed backtracking in a system for computer-aided circuit analysis. AI Journal, 9, 135\u2013196.","journal-title":"AI Journal"},{"key":"12_CR48","unstructured":"Szeider, S. (2005). Backdoor sets for DLL subsolvers. Journal of Automated Reasoning, 35(1\u20133)."},{"key":"12_CR49","doi-asserted-by":"crossref","unstructured":"\u00a0Wang, H. (1960, April). Proving theorems by pattern recognition\u2014I. Communications of the ACM, 3(4), 220\u2013234. ISSN: 0001-0782.","DOI":"10.1145\/367177.367224"},{"key":"12_CR50","doi-asserted-by":"crossref","unstructured":"\u00a0Wang, H. (1960). Toward mechanical mathematics. IBM Journal of Research and Development, 4, 2\u201322. ISSN: 0018-8646.","DOI":"10.1147\/rd.41.0002"},{"key":"12_CR51","doi-asserted-by":"crossref","unstructured":"\u00a0Wang, H. (1961). Proving theorems by pattern recognition\u2014II. Bell System Technical Journal, 40(1), 1\u201341. ISSN: 1538-7305.","DOI":"10.1002\/j.1538-7305.1961.tb03975.x"},{"key":"12_CR52","unstructured":"Williams, R.,\u00a0Gomes, C.,\u00a0&\u00a0Selman, B. (2003). Backdoors to typical case complexity. In 18th IJCAI."},{"key":"12_CR53","doi-asserted-by":"crossref","unstructured":"Zhang, H. (1997, July). SATO: An efficient propositional prover. In 14th CADE. LNCS (Vol. 1249, pp. 272\u2013275), Townsville, Australia.","DOI":"10.1007\/3-540-63104-6_28"}],"container-title":["Outstanding Contributions to Logic","Martin Davis on Computability, Computational Logic, and Mathematical Foundations"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-41842-1_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,7,23]],"date-time":"2022-07-23T05:39:34Z","timestamp":1658554774000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-41842-1_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319418414","9783319418421"],"references-count":53,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-41842-1_12","relation":{},"ISSN":["2211-2758","2211-2766"],"issn-type":[{"type":"print","value":"2211-2758"},{"type":"electronic","value":"2211-2766"}],"subject":[],"published":{"date-parts":[[2016]]}}}