{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T18:35:41Z","timestamp":1725561341068},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540208518"},{"type":"electronic","value":"9783540246053"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-24605-3_22","type":"book-chapter","created":{"date-parts":[[2010,7,29]],"date-time":"2010-07-29T04:50:35Z","timestamp":1280379035000},"page":"287-298","source":"Crossref","is-referenced-by-count":15,"title":["Cache Performance of SAT Solvers: a Case Study for Efficient Implementation of Algorithms"],"prefix":"10.1007","author":[{"given":"Lintao","family":"Zhang","sequence":"first","affiliation":[]},{"given":"Sharad","family":"Malik","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"22_CR1","unstructured":"Biere, A.: Limmat sat solver, http:\/\/www.inf.ethz.ch\/personal\/biere\/projects\/limmat\/"},{"key":"22_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"A. Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol.\u00a01579, p. 193. Springer, Heidelberg (1999)"},{"key":"22_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"454","DOI":"10.1007\/3-540-44585-4_44","volume-title":"Computer Aided Verification","author":"P. Bjesse","year":"2001","unstructured":"Bjesse, P., Leonard, T., Mokkedem, A.: Finding bugs in an Alpha microprocessor using satisfiability solvers. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, p. 454. Springer, Heidelberg (2001)"},{"key":"22_CR4","unstructured":"Crawford, J.M., Auton, L.D.: Experimental results on the crossover point in satisfiability problems. In: Proceedings of the Eleventh National Conference on Artificial Intelligence (AAAI 1993), pp. 21\u201327 (1993)"},{"issue":"7","key":"22_CR5","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":"22_CR6","doi-asserted-by":"crossref","unstructured":"Goldberg, E., Novikov, Y.: BerkMin: A fast and robust SAT-solver. In: Proceedings of the IEEE\/ACM Design, Automation, and Test in Europe, DATE (2002)","DOI":"10.1109\/DATE.2002.998262"},{"key":"22_CR7","doi-asserted-by":"crossref","unstructured":"Bayardo Jr., R.J., Schrag, R.C.: Using CSP look-back techniques to solve real-world SAT instances. In: Proceedings of the National Conference on Artificial Intelligence, AAAI (1997)","DOI":"10.1007\/3-540-61551-2_65"},{"key":"22_CR8","unstructured":"Kautz, H.A., Selman, B.: Planning as satisfiability. In: Proceedings of the Tenth European Conference on Artificial Intelligence (ECAI 1992), pp. 359\u2013363 (1992)"},{"key":"22_CR9","doi-asserted-by":"crossref","unstructured":"LaMarca, A., Ladner, R.E.: The influence of caches on the performance of heaps. ACM Journal of Experimental Algorithmics\u00a01 (1996)","DOI":"10.1145\/235141.235145"},{"key":"22_CR10","unstructured":"Li, C.-M., Anbulagan: Heuristics based on unit propagation for satisfiability problems. In: Proceedings of the Fifteenth International Joint Conference on Artificial Intelligence, IJCAI 1997 (1997)"},{"issue":"5","key":"22_CR11","doi-asserted-by":"publisher","first-page":"506","DOI":"10.1109\/12.769433","volume":"48","author":"J.P. Marques-Silva","year":"1999","unstructured":"Marques-Silva, J.P., Sakallah, K.A.: GRASP - a search algorithm for propositional satisfiability. IEEE Transactions in Computers\u00a048(5), 506\u2013521 (1999)","journal-title":"IEEE Transactions in Computers"},{"key":"22_CR12","doi-asserted-by":"crossref","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient SAT solver. In: Proceedings of the Design Automation Conference (DAC) (June 2001)","DOI":"10.1145\/378239.379017"},{"key":"22_CR13","unstructured":"Nadel, A.: Jerusat sat solver (2002), http:\/\/www.geocities.com\/alikn78\/"},{"key":"22_CR14","doi-asserted-by":"crossref","unstructured":"Nam, G., Sakallah, K.A., Rutenbar, R.A.: Satisfiability-based layout revisited: Routing complex FPGAs via search-based Boolean SAT. In: Proceedings of International Symposium on FPGAs (Feburary 1999)","DOI":"10.1145\/296399.296450"},{"key":"22_CR15","unstructured":"Seward, J.: Valgrind, a open-source memory debugger and cache simulator (2002), http:\/\/developer.kde.org\/~sewardj\/"},{"key":"22_CR16","unstructured":"Simon, L., Le Berre, D., Hirsch, E.A.: SAT 2002 solver competition report (2002), http:\/\/www.satlive.org\/SATCompetition\/onlinereport.pdf"},{"key":"22_CR17","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"O. Strichman","year":"2000","unstructured":"Strichman, O.: Tuning SAT checkers for bounded model-checking. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855. Springer, Heidelberg (2000)"},{"key":"22_CR18","doi-asserted-by":"crossref","unstructured":"Velev, M.N., Bryant, R.E.: Effective use of Boolean satisfiability procedures in the formal verification of superscalar and VLIW microprocessors. In: Proceedings of the Design Automation Conference (DAC) (June 2001)","DOI":"10.1109\/DAC.2001.935509"},{"key":"22_CR19","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/351827.351829","volume":"5","author":"L. Xiao","year":"2000","unstructured":"Xiao, L., Zhang, X., Kubricht, S.A.: Improving memory performance of sorting algorithms. ACM Journal of Experimental Algorithmics\u00a05, 1\u201323 (2000)","journal-title":"ACM Journal of Experimental Algorithmics"},{"key":"22_CR20","unstructured":"Zhang, H., Stickel, M.E.: An efficient algorithm for unit propagation. In: Proceedings of the Fourth International Symposium on Artificial Intelligence and Mathematics (AI-MATH 1996), Fort Lauderdale, Florida USA (1996)"},{"key":"22_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"272","DOI":"10.1007\/3-540-63104-6_28","volume-title":"Automated Deduction - CADE-14","author":"H. Zhang","year":"1997","unstructured":"Zhang, H.: SATO: an efficient propositional prover. In: McCune, W. (ed.) CADE 1997. LNCS, vol.\u00a01249, pp. 272\u2013275. Springer, Heidelberg (1997)"},{"key":"22_CR22","unstructured":"Zhang, L.: Zchaff SAT solver, http:\/\/www.ee.princeton.edu\/~chaff\/zchaff.php"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-24605-3_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,31]],"date-time":"2019-05-31T19:54:27Z","timestamp":1559332467000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-24605-3_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540208518","9783540246053"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-24605-3_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}