{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,23]],"date-time":"2026-10-23T11:59:44Z","timestamp":1792756784829,"version":"4.5.0"},"publisher-location":"Cham","reference-count":41,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319243177","type":"print"},{"value":"9783319243184","type":"electronic"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"unspecified","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":[[2015]]},"DOI":"10.1007\/978-3-319-24318-4_29","type":"book-chapter","created":{"date-parts":[[2015,9,11]],"date-time":"2015-09-11T01:42:56Z","timestamp":1441935776000},"page":"405-422","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":44,"title":["Evaluating CDCL Variable Scoring Schemes"],"prefix":"10.1007","author":[{"given":"Armin","family":"Biere","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Andreas","family":"Fr\u00f6hlich","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2015,10,27]]},"reference":[{"key":"29_CR1","unstructured":"Balint, A., Belov, A., Heule, M.J.H., J\u00e4rvisalo, M. (eds.): Proceedings of SAT Competition 2013. Volume B-2013-1 of Department of Computer Science Series of Publications B. University of Helsinki (2013)"},{"key":"29_CR2","unstructured":"Belov, A., Heule, M.J.H., J\u00e4rvisalo, M. (eds.): Proceedings of SAT Competition 2014. Volume B-2014-2 of Department of Computer Science Series of Publications B. University of Helsinki (2014)"},{"key":"29_CR3","unstructured":"Marques-Silva, J.P., Lynce, I., Malik, S.: Conflict-driven clause learning SAT solvers. [41], 131\u2013153"},{"issue":"5","key":"29_CR4","doi-asserted-by":"publisher","first-page":"506","DOI":"10.1109\/12.769433","volume":"48","author":"JP Marques-Silva","year":"1999","unstructured":"Marques-Silva, J.P., Sakallah, K.A.: GRASP: A search algorithm for propositional satisfiability. IEEE Trans. Computers 48(5), 506\u2013521 (1999)","journal-title":"IEEE Trans. Computers"},{"key":"29_CR5","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 38th Design Automation Conference, DAC 2001, pp. 530\u2013535. ACM, Las Vegas, June 18\u201322, 2001","DOI":"10.1145\/378239.379017"},{"key":"29_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. 4996, pp. 28\u201333. Springer, Heidelberg (2008)"},{"key":"29_CR7","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. 2919, pp. 502\u2013518. Springer, Heidelberg (2004)"},{"key":"29_CR8","unstructured":"Ryan, L.: Efficient algorithms for clause-learning SAT solvers. Master\u2019s thesis, Simon Fraser University (2004)"},{"key":"29_CR9","doi-asserted-by":"crossref","unstructured":"Goldberg, E.I., Novikov, Y.: Berkmin: a fast and robust sat-solver. In: 2002 Design, Automation and Test in Europe Conference and Exposition (DATE 2002), pp. 142\u2013149. IEEE Computer Society, Paris, March 4\u20138, 2002","DOI":"10.1109\/DATE.2002.998262"},{"key":"29_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1007\/11678779_6","volume-title":"Hardware and Software Verification and Testing","author":"R Gershman","year":"2006","unstructured":"Gershman, R., Strichman, O.: Haifasat: A new robust SAT solver. In: Ur, S., Bin, E., Wolfsthal, Y. (eds.) Hardware and Software Verification and Testing. LNCS, vol. 3875, pp. 76\u201389. Springer, Heidelberg (2006)"},{"key":"29_CR11","unstructured":"Biere, A.: P$$\\{$$re, i$$\\}$$coSAT@SC 2009. In: SAT 2009 Competitive Event Booklet, pp. 42\u201343 (2009)"},{"key":"29_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1007\/978-3-642-34188-5_8","volume-title":"Hardware and Software: Verification and Testing","author":"MJH Heule","year":"2012","unstructured":"Heule, M.J.H., Kullmann, O., Wieringa, S., Biere, A.: Cube and conquer: guiding CDCL SAT solvers by lookaheads. In: Eder, K., Louren\u00e7o, J., Shehory, O. (eds.) HVC 2011. LNCS, vol. 7261, pp. 50\u201365. Springer, Heidelberg (2012)"},{"key":"29_CR13","unstructured":"Heule, M., van Maaren, H.: Look-ahead based SAT solvers. [41], 155\u2013184"},{"key":"29_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"410","DOI":"10.1007\/978-3-642-31612-8_31","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2012","author":"C Ans\u00f3tegui","year":"2012","unstructured":"Ans\u00f3tegui, C., Gir\u00e1ldez-Cru, J., Levy, J.: The community structure of SAT formulas. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 410\u2013423. Springer, Heidelberg (2012)"},{"key":"29_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"252","DOI":"10.1007\/978-3-319-09284-3_20","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2014","author":"Z Newsham","year":"2014","unstructured":"Newsham, Z., Ganesh, V., Fischmeister, S., Audemard, G., Simon, L.: Impact of community structure on SAT solver performance. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 252\u2013268. Springer, Heidelberg (2014)"},{"key":"29_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/978-3-319-08587-6_8","volume-title":"Automated Reasoning","author":"C Ans\u00f3tegui","year":"2014","unstructured":"Ans\u00f3tegui, C., Bonet, M.L., Gir\u00e1ldez-Cru, J., Levy, J.: The fractal dimension of SAT formulas. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS, vol. 8562, pp. 107\u2013121. Springer, Heidelberg (2014)"},{"issue":"7","key":"29_CR17","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.W.: A machine program for theorem-proving. Commun. ACM 5(7), 394\u2013397 (1962)","journal-title":"Commun. ACM"},{"issue":"8","key":"29_CR18","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"RE Bryant","year":"1986","unstructured":"Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Trans. Computers 35(8), 677\u2013691 (1986)","journal-title":"IEEE Trans. Computers"},{"key":"29_CR19","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., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, p. 193. Springer, Heidelberg (1999)"},{"issue":"1\u20134","key":"29_CR20","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/BF01531077","volume":"1","author":"RG Jeroslow","year":"1990","unstructured":"Jeroslow, R.G., Wang, J.: Solving propositional satisfiability problems. Annals of Mathematics and Artificial Intelligence 1(1\u20134), 167\u2013187 (1990)","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"key":"29_CR21","series-title":"Lecture Notes in Computer Science (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. 1695, pp. 62\u201374. Springer, Heidelberg (1999)"},{"key":"29_CR22","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. 4501, pp. 294\u2013299. Springer, Heidelberg (2007)"},{"key":"29_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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, William (ed.) CADE 1997. LNCS, vol. 1249, pp. 272\u2013275. Springer, Heidelberg (1997)"},{"issue":"2\u20134","key":"29_CR24","first-page":"75","volume":"4","author":"A Biere","year":"2008","unstructured":"Biere, A.: PicoSAT essentials. JSAT 4(2\u20134), 75\u201397 (2008)","journal-title":"JSAT"},{"key":"29_CR25","doi-asserted-by":"publisher","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. J. Artif. Intell. Res. (JAIR) 22, 319\u2013351 (2004)","journal-title":"J. Artif. Intell. Res. (JAIR)"},{"key":"29_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/978-3-642-02777-2_21","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2009","author":"H Han","year":"2009","unstructured":"Han, H., Somenzi, F.: On-the-fly clause improvement. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 209\u2013222. Springer, Heidelberg (2009)"},{"key":"29_CR27","doi-asserted-by":"crossref","unstructured":"Hamadi, Y., Jabbour, S., Sais, L.: Learning for dynamic subsumption. In: 21st IEEE International Conference on Tools with Artificial Intelligence, Newark, New Jersey, USA, ICTAI 2009, pp. 328\u2013335. IEEE Computer Society, November 2\u20134, 2009","DOI":"10.1109\/ICTAI.2009.22"},{"issue":"4","key":"29_CR28","first-page":"133","volume":"7","author":"P van der Tak","year":"2011","unstructured":"van der Tak, P., Ramos, A., Heule, M.J.H.: Reusing the assignment trail in CDCL solvers. JSAT 7(4), 133\u2013138 (2011)","journal-title":"JSAT"},{"key":"29_CR29","unstructured":"Nadel, A.: Backtrack search algorithms for propositional logic satisfiability: Review and innovations. Master\u2019s thesis, Hebrew University (2002)"},{"issue":"2","key":"29_CR30","doi-asserted-by":"publisher","first-page":"202","DOI":"10.1145\/2786.2793","volume":"28","author":"DD Sleator","year":"1985","unstructured":"Sleator, D.D., Tarjan, R.E.: Amortized efficiency of list update and paging rules. Commun. ACM 28(2), 202\u2013208 (1985)","journal-title":"Commun. ACM"},{"key":"29_CR31","unstructured":"Biere, A.: Lingeling and friends entering the SAT challenge 2012. In: Balint, A., Belov, A., Diepold, D., Gerber, S., J\u00e4rvisalo, M., Sinz, C. (eds.) Proceedings SAT Challenge 2012: Solver and Benchmark Descriptions. Volume B-2012-2 of Department of Computer Science Series of Publications B., University of Helsinki, pp. 33\u201334 (2012)"},{"key":"29_CR32","unstructured":"Biere, A.: Yet another local search solver and Lingeling and friends entering the SAT Competition 2014. [2], 39\u201340"},{"key":"29_CR33","unstructured":"Audemard, G., Simon, L.: Predicting learnt clauses quality in modern SAT solvers. In: Boutilier, C. (ed.) Proceedings of the 21st International Joint Conference on Artificial Intelligence, IJCAI 2009, Pasadena, California, USA, pp. 399\u2013404, July 11\u201317, 2009"},{"key":"29_CR34","unstructured":"Audemard, G., Simon, L.: Glucose 2.3 in the SAT 2013 Competition. [1], 42\u201343"},{"key":"29_CR35","unstructured":"Oh, C.: MiniSat HACK 999ED, MiniSat HACK 1430ED and SWDiA5BY. [2], 46\u201347"},{"key":"29_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"355","DOI":"10.1007\/978-3-642-31365-3_28","volume-title":"Automated Reasoning","author":"M J\u00e4rvisalo","year":"2012","unstructured":"J\u00e4rvisalo, M., Heule, M.J.H., Biere, A.: Inprocessing rules. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol. 7364, pp. 355\u2013370. Springer, Heidelberg (2012)"},{"key":"29_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"118","DOI":"10.1007\/978-3-642-33558-7_11","volume-title":"Principles and Practice of Constraint Programming","author":"G Audemard","year":"2012","unstructured":"Audemard, G., Simon, L.: Refining restarts strategies for SAT and UNSAT. In: Milano, M. (ed.) CP 2012. LNCS, vol. 7514, pp. 118\u2013126. Springer, Heidelberg (2012)"},{"key":"29_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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. 3569, pp. 61\u201375. Springer, Heidelberg (2005)"},{"key":"29_CR39","unstructured":"Wallner, J.P.: Benchmark for complete and stable semantics for argumentation frameworks. [2], 84\u201385"},{"key":"29_CR40","unstructured":"Biere, A., Heule, M.J.H., J\u00e4rvisalo, M., Manthey, N.: Equivalence checking of HWMCC 2012 circuits. [1], 104"},{"key":"29_CR41","unstructured":"Biere, A., Heule, M.J.H., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability. Volume 185 of Frontiers in Artificial Intelligence and Applications. IOS Press (2009)"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing -- SAT 2015"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-24318-4_29","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,6,25]],"date-time":"2026-06-25T05:09:17Z","timestamp":1782364157000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-24318-4_29"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319243177","9783319243184"],"references-count":41,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-24318-4_29","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"27 October 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}