{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,16]],"date-time":"2026-01-16T01:34:49Z","timestamp":1768527289225,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540631040","type":"print"},{"value":"9783540691402","type":"electronic"}],"license":[{"start":{"date-parts":[[1997,1,1]],"date-time":"1997-01-01T00:00:00Z","timestamp":852076800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1997]]},"DOI":"10.1007\/3-540-63104-6_28","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T18:04:34Z","timestamp":1330279474000},"page":"272-275","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":197,"title":["SATO: An efficient propositional prover"],"prefix":"10.1007","author":[{"given":"Hantao","family":"Zhang","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,8]]},"reference":[{"key":"28_CR1","unstructured":"Barth, P., A Davis-Putnam based enumeration algorithm for linear pseudo-Boolean optimization, Technical Report MPI-I-95-2-003, Max-Plank-Institut fur Informatik, 1995."},{"key":"28_CR2","unstructured":"Crawford, J., Auton, L., (1993) Experimental results on the cross-over point in satisfiability problems. In Proc. of the 11th National Conference on Artificial Intelligence (AAAI-93), pp. 22\u201328."},{"issue":"7","key":"28_CR3","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M. Davis","year":"1962","unstructured":"Davis, M., G. Logemann, and D. Loveland. A machine program for theorem-proving. Communications of the Association for Computing Machinery 5, 7 (July 1962), 394\u2013397.","journal-title":"Communications of the Association for Computing Machinery"},{"key":"28_CR4","unstructured":"Dubois, O, Andre, P., Boufkhan, Y., Carlier, J., SAT versus UNSAT, see [6]."},{"key":"28_CR5","unstructured":"(1995) Freeman, J.W., Improvements to propositional satisfiability search algorithms. Ph.D. Dissertation, Dept. of Computer Science, University of Pennsylvania."},{"key":"28_CR6","unstructured":"Johnson, D.S., Trick, M.A., (eds.) The second DIMACS implementation challenge, DIMACS Series in Discrete Mathematics and Theoretical Computer Science (see http:\/\/dimacs.rutgers.edu\/challenges\/)"},{"key":"28_CR7","unstructured":"(1980) McAllester, D.A., An outlook on truth maintenance, AI Memo 551, MIT AI laboratory."},{"key":"28_CR8","unstructured":"Pretolani, D., Efficiency and stability of hypergraph SAT algorithms, see [6]."},{"key":"28_CR9","volume-title":"Technical Reports","author":"J.P.M. Silva","year":"1996","unstructured":"Silva, J.P.M., Sakallah, K.A., Conflict analysis in search algorithms for propositional satisfiability. Technical Reports, Cadence European Laboraties, ALGOS, INESC, Lisboa, Portugal, May 1996."},{"key":"28_CR10","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1016\/0004-3702(77)90029-7","volume":"9","author":"R.M. 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. Artificial Intelligence, vol. 9, 135\u2013196","journal-title":"Artificial Intelligence"},{"key":"28_CR11","volume-title":"Memo no. UCS\/ERL M92\/112","author":"P.R. Stephan","year":"1992","unstructured":"Stephan, P.R., Brayton, R.K., Sangiovanni-Binventelli, Combinational test generation using satisfiability, Memo no. UCS\/ERL M92\/112, Dept. of Electrical Engineering and Computer Science, University of California at Berkeley, Oct. 1992."},{"key":"28_CR12","first-page":"1","volume":"22","author":"H. Zhang","year":"1993","unstructured":"Zhang, H., SATO: A decision procedure for propositional logic. Association for Automated Reasoning Newsletter, 22, 1\u20133, March 1993.","journal-title":"Association for Automated Reasoning Newsletter"},{"key":"28_CR13","doi-asserted-by":"crossref","unstructured":"Zhang, H., Bonacina, M.P., Hsiang, H.: (1996) PSATO: a distributed propositional prover and its application to quasigroup problems. To appear in Journal of Symbolic Computation.","DOI":"10.1006\/jsco.1996.0030"},{"key":"28_CR14","unstructured":"Zhang, H., Stickel, M. (1994) Implementing the Davis-Putnam algorithm by tries. Technical Report, Dept. of Computer Science, The University of Iowa."}],"updated-by":[{"DOI":"10.1007\/3-540-63104-6_45","type":"correction","label":"Correction","source":"publisher","updated":{"date-parts":[[2005,6,8]],"date-time":"2005-06-08T00:00:00Z","timestamp":1118188800000}}],"container-title":["Lecture Notes in Computer Science","Automated Deduction\u2014CADE-14"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-63104-6_28","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T08:44:21Z","timestamp":1558255461000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-63104-6_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540631040","9783540691402"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/3-540-63104-6_28","relation":{"correction":[{"id-type":"doi","id":"10.1007\/3-540-63104-6_45","asserted-by":"object"}]},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1997]]},"assertion":[{"value":"8 June 2005","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}