{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,29]],"date-time":"2025-11-29T07:44:16Z","timestamp":1764402256357,"version":"3.41.0"},"reference-count":19,"publisher":"Springer Science and Business Media LLC","issue":"1-2","license":[{"start":{"date-parts":[[2000,2,1]],"date-time":"2000-02-01T00:00:00Z","timestamp":949363200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2000,2,1]],"date-time":"2000-02-01T00:00:00Z","timestamp":949363200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Journal of Automated Reasoning"],"published-print":{"date-parts":[[2000,2]]},"DOI":"10.1023\/a:1006351428454","type":"journal-article","created":{"date-parts":[[2002,12,22]],"date-time":"2002-12-22T01:36:27Z","timestamp":1040520987000},"page":"277-296","source":"Crossref","is-referenced-by-count":45,"title":["Implementing the Davis\u2013Putnam Method"],"prefix":"10.1007","volume":"24","author":[{"given":"Hantao","family":"Zhang","sequence":"first","affiliation":[]},{"given":"Mark","family":"Stickel","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"255322_CR1","volume-title":"Contemporary Design Theory: A Collection of Surveys","author":"F. E. Bennett","year":"1992","unstructured":"Bennett, F. E. and Zhu, L.: Conjugate-orthogonal Latin squares and related structures, in J. H. Dinitz and D. R. Stinson (eds.), Contemporary Design Theory: A Collection of Surveys, Wiley, New York, 1992."},{"key":"255322_CR2","unstructured":"Crawford, J. M. and Auton, L. D.: Experimental results on the crossover point in satisfiability problems, in Proceedings of the Eleventh National Conference on Artificial Intelligence (AAAI-93), 1993, pp. 21\u201327."},{"issue":"3","key":"255322_CR3","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M. Davis","year":"1960","unstructured":"Davis, M. and Putnam, H.: A computing procedure for quantification theory, J. Assoc. Comput. Mach.\n7(3) (July 1960), 201\u2013215.","journal-title":"J. Assoc. Comput. Mach."},{"issue":"7","key":"255322_CR4","first-page":"394","volume":"5","author":"M. Davis","year":"1962","unstructured":"Davis, M., Logemann, G., and Loveland, D.: A machine program for theorem-proving, Comm. Assoc. Comput. Mach.\n5(7) (July 1962), 394\u2013397.","journal-title":"Comm. Assoc. Comput. Mach."},{"key":"255322_CR5","unstructured":"de Kleer, J.: An improved incremental algorithm for generating prime implicates, in Proceedings of the Tenth National Conference on Artificial Intelligence (AAAI-92), San Jose, California, July 1992, pp. 780\u2013785."},{"key":"255322_CR6","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1016\/0743-1066(84)90014-1","volume":"3","author":"W. F. Dowling","year":"1984","unstructured":"Dowling, W. F. and Gallier, J. H.: Linear-time algorithms for testing the satisfiability of propositional Horn formulae, J. Logic Programming\n3 (1984), 267\u2013284.","journal-title":"J. Logic Programming"},{"key":"255322_CR7","unstructured":"Freeman, J. W.: Improvements to propositional satisfiability search algorithms, Ph.D. Dissertation, Department of Computer and Information Science, University of Pennsylvania, May 1995."},{"key":"255322_CR8","unstructured":"Fujita, M., Slaney, J. and Bennett, F.: Automatic generation of some results in finite algebra, in Proceedings of the Thirteenth International Joint Conference on Artificial Intelligence, Chambery, France, 1993."},{"key":"255322_CR9","doi-asserted-by":"crossref","unstructured":"Gomes, C., Selman, B. and Crato, N.: Heavy-tailed distributions in combinatorial search, in Proceedings of the Third International Conference on Principles and Practice of Constraint Programming (CP97), Linz, Austria, 1997.","DOI":"10.1007\/BFb0017434"},{"issue":"4","key":"255322_CR10","doi-asserted-by":"crossref","first-page":"1108","DOI":"10.1109\/21.247892","volume":"23","author":"J. Gu","year":"1993","unstructured":"Gu, J.: Local search for satisfiability (SAT) problem, IEEE Trans. on Systems Man Cybernet.\n23(4) (1993), 1108\u20131129.","journal-title":"IEEE Trans. on Systems Man Cybernet."},{"key":"255322_CR11","doi-asserted-by":"crossref","unstructured":"Li, C. M. and Anbulagan: Look-ahead versus look-back for satisfiability problems, in Proceedings of International Conference on Principles and Practice of Constraint Programming, 1997.","DOI":"10.1007\/BFb0017450"},{"key":"255322_CR12","series-title":"Tech. memo MCS-TM-194","volume-title":"A Davis-Putnam program and its application to finite first-order model search: Quasigroup existence problems","author":"W. McCune","year":"1994","unstructured":"McCune, W.: A Davis-Putnam program and its application to finite first-order model search: Quasigroup existence problems, Tech. memo MCS-TM-194, Mathematics and Computer Science Division, Argonne National Laboratory, Argonne, Illinois, May 1994."},{"key":"255322_CR13","series-title":"Automated Reasoning Project","volume-title":"Stickel's Davis-Putnam engineered reversely, Available by anonymous FTP from arp.anu.edu.au","author":"G. Meglicki","year":"1993","unstructured":"Meglicki, G.: Stickel's Davis-Putnam engineered reversely, Available by anonymous FTP from arp.anu.edu.au, Automated Reasoning Project, Australian National University, Canberra, Australia, 1993."},{"key":"255322_CR14","unstructured":"Selman, B., Levesque, H., and Mitchell, D.: A new method for solving hard satisfiability problems, in Proceedings of the Tenth National Conference on Artificial Intelligence (AAAI-92), San Jose, California, July 1992, pp. 440\u2013446."},{"issue":"2","key":"255322_CR15","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1016\/0898-1221(94)00219-B","volume":"29","author":"J. Slaney","year":"1995","unstructured":"Slaney, J., Fujita,M., and Stickel, M.: Automated reasoning and exhaustive search: Quasigroup existence problems, Comput. Math. Appl.\n29(2) (May 1995), 115\u2013132.","journal-title":"Comput. Math. Appl."},{"key":"255322_CR16","first-page":"1","volume":"22","author":"H. Zhang","year":"1993","unstructured":"Zhang, H.: SATO: A decision procedure for propositional logic, Assoc. Automated Reasoning Newslett.\n22 (March 1993), 1\u20133.","journal-title":"Assoc. Automated Reasoning Newslett."},{"key":"255322_CR17","unstructured":"Zhang, H.: Specifying Latin squares in propositional logic, in R. Veroff (ed.), Automated Reasoning and Its Applications, Essays in Honor of Larry Wos, Chapter 6, MIT Press, 1997."},{"key":"255322_CR18","unstructured":"Zhang, H.: SATO: An efficient propositional prover, in Proc. of International Conference on Automated Deduction (CADE-97), Lecture Notes in Artif. Intell. 1104, Springer-Verlag, 1997, pp. 308\u2013312."},{"key":"255322_CR19","volume-title":"Search for idempotent models of quasigroup identities","author":"J. Zhang","year":"1991","unstructured":"Zhang, J.: Search for idempotent models of quasigroup identities, Typescript, Institute of Software, Academia Sinica, Beijing, 1991."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1006351428454.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1006351428454\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1006351428454.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:38:44Z","timestamp":1749123524000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1006351428454"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000,2]]},"references-count":19,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[2000,2]]}},"alternative-id":["255322"],"URL":"https:\/\/doi.org\/10.1023\/a:1006351428454","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2000,2]]}}}