{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,19]],"date-time":"2025-02-19T22:40:10Z","timestamp":1740004810557,"version":"3.37.3"},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642122507"},{"type":"electronic","value":"9783642122514"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-12251-4_13","type":"book-chapter","created":{"date-parts":[[2010,4,9]],"date-time":"2010-04-09T23:32:42Z","timestamp":1270855962000},"page":"165-174","source":"Crossref","is-referenced-by-count":8,"title":["A Pearl on SAT Solving in Prolog"],"prefix":"10.1007","author":[{"given":"Jacob M.","family":"Howe","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andy","family":"King","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"3","key":"13_CR1","doi-asserted-by":"publisher","first-page":"371","DOI":"10.1017\/S1471068403001893","volume":"4","author":"M. Bruynooghe","year":"2004","unstructured":"Bruynooghe, M.: Enhancing a Search Algorithm to Perform Intelligent Backtracking. Theory and Practice of Logic Programming\u00a04(3), 371\u2013380 (2004)","journal-title":"Theory and Practice of Logic Programming"},{"issue":"1","key":"13_CR2","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1017\/S1471068407003146","volume":"8","author":"M. Codish","year":"2008","unstructured":"Codish, M., Lagoon, V., Stuckey, P.J.: Logic Programming with Satisfiability. Theory and Practice of Logic Programming\u00a08(1), 121\u2013128 (2008)","journal-title":"Theory and Practice of Logic Programming"},{"issue":"7","key":"13_CR3","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"},{"key":"13_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1007\/11499107_5","volume-title":"Theory and Applications of Satisfiability Testing","author":"N. E\u00e9n","year":"2005","unstructured":"E\u00e9n, N., Biere, A.: Effective preprocessing in SAT through variable and clause elimination. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol.\u00a03569, pp. 61\u201375. Springer, Heidelberg (2005)"},{"key":"13_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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":"13_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1007\/11889205_15","volume-title":"Principles and Practice of Constraint Programming - CP 2006","author":"I.P. Gent","year":"2006","unstructured":"Gent, I.P., Jefferson, C., Miguel, I.: Watched Literals for Constraint Propagation in Minion. In: Benhamou, F. (ed.) CP 2006. LNCS, vol.\u00a04204, pp. 182\u2013197. Springer, Heidelberg (2006)"},{"key":"13_CR7","first-page":"283","volume-title":"SAT 2000","author":"H.H. Hoos","year":"2000","unstructured":"Hoos, H.H., St\u00fctzle, T.: SATLIB: An Online Resource for Research on SAT. In: SAT 2000, pp. 283\u2013292. IOS Press, Amsterdam (2000)"},{"key":"13_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"120","DOI":"10.1007\/3-540-45635-X_16","volume-title":"Logic Programming","author":"J.M. Howe","year":"2001","unstructured":"Howe, J.M., King, A.: Positive Boolean Functions as Multiheaded Clauses. In: Codognet, P. (ed.) ICLP 2001. LNCS, vol.\u00a02237, pp. 120\u2013134. Springer, Heidelberg (2001)"},{"issue":"1","key":"13_CR9","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1017\/S1471068402001485","volume":"3","author":"J.M. Howe","year":"2003","unstructured":"Howe, J.M., King, A.: Efficient Groundness Analysis in Prolog. Theory and Practice of Logic Programming\u00a03(1), 95\u2013124 (2003)","journal-title":"Theory and Practice of Logic Programming"},{"issue":"1-2","key":"13_CR10","first-page":"179","volume":"69","author":"A. King","year":"2006","unstructured":"King, A., Martin, J.C.: Control Generation by Program Transformation. Fundamenta Informaticae\u00a069(1-2), 179\u2013218 (2006)","journal-title":"Fundamenta Informaticae"},{"issue":"7","key":"13_CR11","doi-asserted-by":"publisher","first-page":"424","DOI":"10.1145\/359131.359136","volume":"22","author":"R.A. Kowalski","year":"1979","unstructured":"Kowalski, R.A.: Algorithm = Logic + Control. Communication of the ACM\u00a022(7), 424\u2013436 (1979)","journal-title":"Communication of the ACM"},{"key":"13_CR12","unstructured":"Le Berre, D., Roussel, O., Simon, L.: The International SAT Competitions Webpage (2009), http:\/\/www.satcompetition.org\/"},{"key":"13_CR13","doi-asserted-by":"crossref","unstructured":"Marques-Silva, J.P., Sakallah, K.A.: GRASP \u2013 a New Search Algorithm for Satisfiability. In: International Conference on Computer-Aided Design, pp. 220\u2013227. ACM and IEEE Computer Society (1996)","DOI":"10.1109\/ICCAD.1996.569607"},{"key":"13_CR14","first-page":"530","volume-title":"Design Automation Conference","author":"M.W. Moskewicz","year":"2001","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an Efficient SAT Solver. In: Design Automation Conference, pp. 530\u2013535. ACM Press, New York (2001)"},{"key":"13_CR15","volume-title":"Negation and Control in Logic Programs","author":"L. Naish","year":"1986","unstructured":"Naish, L.: Negation and Control in Logic Programs. Springer, Heidelberg (1986)"},{"key":"13_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/3-540-45657-0_2","volume-title":"Computer Aided Verification","author":"L. Zhang","year":"2002","unstructured":"Zhang, L., Malik, S.: The Quest for Efficient Boolean Satisfiability Solvers. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 17\u201336. Springer, Heidelberg (2002)"}],"container-title":["Lecture Notes in Computer Science","Functional and Logic Programming"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-12251-4_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,19]],"date-time":"2025-02-19T22:22:58Z","timestamp":1740003778000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-12251-4_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642122507","9783642122514"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-12251-4_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}