{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,25]],"date-time":"2026-04-25T14:01:58Z","timestamp":1777125718603,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":37,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642215803","type":"print"},{"value":"9783642215810","type":"electronic"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"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":[[2011]]},"DOI":"10.1007\/978-3-642-21581-0_27","type":"book-chapter","created":{"date-parts":[[2011,6,10]],"date-time":"2011-06-10T13:30:19Z","timestamp":1307712619000},"page":"343-356","source":"Crossref","is-referenced-by-count":30,"title":["Empirical Study of the Anatomy of Modern Sat Solvers"],"prefix":"10.1007","author":[{"given":"Hadi","family":"Katebi","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Karem A.","family":"Sakallah","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jo\u00e3o P.","family":"Marques-Silva","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"27_CR1","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1016\/0020-0190(93)90029-9","volume":"47","author":"M.L. Alistair","year":"1993","unstructured":"Alistair, M.L., Sinclair, A., Zuckerman, D.: Optimal speedup of las vegas algorithms. Information Processing Letters\u00a047, 173\u2013180 (1993)","journal-title":"Information Processing Letters"},{"issue":"5","key":"27_CR2","doi-asserted-by":"publisher","first-page":"549","DOI":"10.1109\/TC.2006.75","volume":"55","author":"F. Aloul","year":"2006","unstructured":"Aloul, F., Sakallah, K., Markov, I.: Efficient symmetry breaking for boolean satisfiability. IEEE Transactions on Computers\u00a055(5), 549\u2013558 (2006)","journal-title":"IEEE Transactions on Computers"},{"key":"27_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/978-3-642-04244-7_13","volume-title":"Principles and Practice of Constraint Programming - CP 2009","author":"C. Ans\u00f3tegui","year":"2009","unstructured":"Ans\u00f3tegui, C., Bonet, M.L., Levy, J.: On the structure of industrial SAT instances. In: Gent, I.P. (ed.) CP 2009. LNCS, vol.\u00a05732, pp. 127\u2013141. Springer, Heidelberg (2009)"},{"key":"27_CR4","doi-asserted-by":"crossref","unstructured":"Babic, D., Hu, A.J.: Calysto: scalable and precise extended static checking. In: International Conference on Software Engineering, pp. 211\u2013220 (2008)","DOI":"10.1145\/1368088.1368118"},{"key":"27_CR5","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1613\/jair.1410","volume":"22","author":"P. Beame","year":"2004","unstructured":"Beame, P., Kautz, H.A., Sabharwal, A.: Towards understanding and harnessing the potential of clause learning. Journal of Artificial Intelligence Research\u00a022, 319\u2013351 (2004)","journal-title":"Journal of Artificial Intelligence Research"},{"key":"27_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1007\/978-3-540-79719-7_4","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2008","author":"A. Biere","year":"2008","unstructured":"Biere, A.: Adaptive restart strategies for conflict driven SAT solvers. In: Kleine B\u00fcning, H., Zhao, X. (eds.) SAT 2008. LNCS, vol.\u00a04996, pp. 28\u201333. Springer, Heidelberg (2008)"},{"key":"27_CR7","volume-title":"Advances in Computers","author":"A. Biere","year":"2003","unstructured":"Biere, A., Cimatti, A., Clarke, E., Strichman, O., Zhu, Y.: Bounded Model Checking. In: Advances in Computers. Academic Press, London (2003)"},{"key":"27_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1007\/978-3-642-02777-2_3","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2009","author":"M.L. Bonet","year":"2009","unstructured":"Bonet, M.L., John, K.S.: Efficiently calculating evolutionary tree measures using SAT. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol.\u00a05584, pp. 4\u201317. Springer, Heidelberg (2009)"},{"key":"27_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/978-3-540-24605-3_13","volume-title":"Theory and Applications of Satisfiability Testing","author":"E. Broering","year":"2004","unstructured":"Broering, E., Lokam, S.V.: Width-based algorithms for SAT and CIRCUIT-SAT. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol.\u00a02919, pp. 162\u2013171. Springer, Heidelberg (2004)"},{"key":"27_CR10","volume-title":"Hybrid Optimization: the 10 years of CPAIOR","author":"F. Corblin","year":"2010","unstructured":"Corblin, F., Bordeaux, L., Fanchon, E., Hamadi, Y., Trilling, L.: Connections and integration with SAT solvers: A survey and a case study in computational biology. In: Hybrid Optimization: the 10 years of CPAIOR. Springer, Heidelberg (2010)"},{"key":"27_CR11","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, 394\u2013397 (1962)","journal-title":"Communications of the ACM"},{"key":"27_CR12","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M. Davis","year":"1960","unstructured":"Davis, M., Putnam, H.: A computing procedure for quantification theory. Journal of the ACM\u00a07, 201\u2013215 (1960)","journal-title":"Journal of the ACM"},{"key":"27_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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":"27_CR14","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: MiniSAT, version 2.2.0 (2010), http:\/\/minisat.se\/downloads\/minisat-2.2.0.tar.gz"},{"key":"27_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"340","DOI":"10.1007\/978-3-540-72788-0_33","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2007","author":"C. Fuhs","year":"2007","unstructured":"Fuhs, C., Giesl, J., Middeldorp, A., Schneider-Kamp, P., Thiemann, R., Zankl, H.: SAT solving for termination analysis with polynomial interpretations. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol.\u00a04501, pp. 340\u2013354. Springer, Heidelberg (2007)"},{"key":"27_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/BFb0017434","volume-title":"Principles and Practice of Constraint Programming - CP97","author":"C.P. Gomes","year":"1997","unstructured":"Gomes, C.P., Selman, B., Crato, N.: Heavy-tailed distributions in combinatorial search. In: Smolka, G. (ed.) CP 1997. LNCS, vol.\u00a01330, pp. 121\u2013135. Springer, Heidelberg (1997)"},{"key":"27_CR17","unstructured":"Gomes, C.P., Selman, B., Kautz, H.: Boosting combinatorial search through randomization. In: National Conference on Artificial Intelligence, pp. 431\u2013437 (July 1998)"},{"key":"27_CR18","first-page":"2318","volume-title":"Proceedings of the 20th International Joint Conference on Artifical Intelligence","author":"J. Huang","year":"2007","unstructured":"Huang, J.: The effect of restarts on the efficiency of clause learning. In: Proceedings of the 20th International Joint Conference on Artifical Intelligence, pp. 2318\u20132323. Morgan Kaufmann Publishers Inc., San Francisco (2007)"},{"issue":"1","key":"27_CR19","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1109\/43.108614","volume":"11","author":"T. Larrabee","year":"1992","unstructured":"Larrabee, T.: Test pattern generation using Boolean satisfiability. IEEE Transactions on Computer-Aided Design\u00a011(1), 4\u201315 (1992)","journal-title":"IEEE Transactions on Computer-Aided Design"},{"key":"27_CR20","first-page":"166","volume-title":"Proceedings of the 15th Eureopean Conference on Artificial Intelligence (ECAI 2002)","author":"I. Lynce","year":"2002","unstructured":"Lynce, I., Marques-Silva, J.: Building state-of-the-art sat solvers. In: Proceedings of the 15th Eureopean Conference on Artificial Intelligence (ECAI 2002), pp. 166\u2013170. IOS Press, Amsterdam (2002)"},{"key":"27_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/11560548_32","volume-title":"Correct Hardware Design and Verification Methods","author":"P. Manolios","year":"2005","unstructured":"Manolios, P., Srinivasan, S.K.: A parameterized benchmark suite of hard pipelined-machine-verification problems. In: Borrione, D., Paul, W. (eds.) CHARME 2005. LNCS, vol.\u00a03725, pp. 363\u2013366. Springer, Heidelberg (2005)"},{"key":"27_CR22","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"62","DOI":"10.1007\/3-540-48159-1_5","volume-title":"Progress in Artificial Intelligence","author":"J. Marques-Silva","year":"1999","unstructured":"Marques-Silva, J.: The impact of branching heuristics in propositional satisfiability algorithms. In: Barahona, P., Alferes, J.J. (eds.) EPIA 1999. LNCS (LNAI), vol.\u00a01695, pp. 62\u201374. Springer, Heidelberg (1999)"},{"key":"27_CR23","series-title":"Lecture Notes in Computer Science","first-page":"220","volume-title":"Formal Methods in Computer-Aided Design","author":"J. Marques-Silva","year":"1996","unstructured":"Marques-Silva, J., Sakallah, K.A.: GRASP: A new search algorithm for satisfiability. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol.\u00a01166, pp. 220\u2013227. Springer, Heidelberg (1996)"},{"issue":"5","key":"27_CR24","doi-asserted-by":"publisher","first-page":"506","DOI":"10.1109\/12.769433","volume":"48","author":"J. Marques-Silva","year":"1999","unstructured":"Marques-Silva, J., Sakallah, K.A.: GRASP-A search algorithm for propositional satisfiability. IEEE Transactions on Computers\u00a048(5), 506\u2013521 (1999)","journal-title":"IEEE Transactions on Computers"},{"key":"27_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1007\/11814948_13","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2006","author":"I. Mironov","year":"2006","unstructured":"Mironov, I., Zhang, L.: Applications of SAT solvers to cryptanalysis of hash functions. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol.\u00a04121, pp. 102\u2013115. Springer, Heidelberg (2006)"},{"key":"27_CR26","unstructured":"Mitchell, D., Selman, B., Levesque, H.: Hard and easy distributions of sat problems. In: National Conference on Artificial Intelligence, pp. 459\u2013465 (1992)"},{"key":"27_CR27","doi-asserted-by":"crossref","unstructured":"Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Engineering an efficient SAT solver. In: Design Automation Conference, pp. 530\u2013535 (June 2001)","DOI":"10.1145\/378239.379017"},{"key":"27_CR28","doi-asserted-by":"crossref","unstructured":"Nam, G.-J., Sakallah, K.A., Rutenbar, R.A.: Satisfiability-based layout revisited: Detailed routing of complex FPGA s via search-based boolean SAT. In: International Symposium on Field-Programmable Gate Arrays (February 1999)","DOI":"10.1145\/296399.296450"},{"key":"27_CR29","unstructured":"Narain, S.: Network configuration management via model finding. In: Conference on Systems Administration, pp. 155\u2013168 (2005)"},{"key":"27_CR30","unstructured":"Pipatsrisawat, K., Darwiche, A.: Rsat 1.03: Sat solver description. Technical Report D\u2013152, Automated Reasoning Group, Computer Science Department, UCLA (2006)"},{"key":"27_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"294","DOI":"10.1007\/978-3-540-72788-0_28","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2007","author":"K. Pipatsrisawat","year":"2007","unstructured":"Pipatsrisawat, K., Darwiche, A.: A lightweight component caching scheme for satisfiability solvers. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol.\u00a04501, pp. 294\u2013299. Springer, Heidelberg (2007)"},{"key":"27_CR32","volume-title":"Mathematical Statistics and Data Analysis","author":"J.A. Rice","year":"2006","unstructured":"Rice, J.A.: Mathematical Statistics and Data Analysis. Duxbury Press, Boston (2006)"},{"key":"27_CR33","unstructured":"Selman, B., Kautz, H.: Planning as satisfiability. In: European Conference on Artificial Intelligence, pp. 359\u2013363 (1992)"},{"key":"27_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1007\/978-3-642-02777-2_33","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2009","author":"C. Sinz","year":"2009","unstructured":"Sinz, C., Iser, M.: Problem-sensitive restart heuristics for the DPLL procedure. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol.\u00a05584, pp. 356\u2013362. Springer, Heidelberg (2009)"},{"issue":"1","key":"27_CR35","first-page":"75","volume":"17","author":"C. Sinz","year":"2003","unstructured":"Sinz, C., Kaiser, A., K\u00fcchlin, W.: Formal methods for the validation of automotive product configuration data. AI EDAM\u00a017(1), 75\u201397 (2003)","journal-title":"AI EDAM"},{"key":"27_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1007\/978-3-642-02777-2_23","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2009","author":"N. S\u00f6rensson","year":"2009","unstructured":"S\u00f6rensson, N., Biere, A.: Minimizing learned clauses. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol.\u00a05584, pp. 237\u2013243. Springer, Heidelberg (2009)"},{"issue":"2","key":"27_CR37","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1016\/S0747-7171(02)00091-3","volume":"35","author":"M.N. Velev","year":"2003","unstructured":"Velev, M.N., Bryant, R.E.: Effective use of boolean satisfiability procedures in the formal verification of superscalar and vliw microprocessors. J. Symb. Comput.\u00a035(2), 73\u2013106 (2003)","journal-title":"J. Symb. Comput."}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing - SAT 2011"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-21581-0_27","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,6]],"date-time":"2025-03-06T02:49:32Z","timestamp":1741229372000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-21581-0_27"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642215803","9783642215810"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-21581-0_27","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011]]}}}