{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,22]],"date-time":"2026-09-22T11:58:01Z","timestamp":1790078281392,"version":"4.0.1"},"publisher-location":"Cham","reference-count":33,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319409696","type":"print"},{"value":"9783319409702","type":"electronic"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"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":[[2016]]},"DOI":"10.1007\/978-3-319-40970-2_9","type":"book-chapter","created":{"date-parts":[[2016,6,10]],"date-time":"2016-06-10T11:14:55Z","timestamp":1465557295000},"page":"123-140","source":"Crossref","is-referenced-by-count":88,"title":["Learning Rate Based Branching Heuristic for SAT Solvers"],"prefix":"10.1007","author":[{"given":"Jia Hui","family":"Liang","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Vijay","family":"Ganesh","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Pascal","family":"Poupart","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Krzysztof","family":"Czarnecki","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2016,6,11]]},"reference":[{"key":"9_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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":"9_CR2","unstructured":"Audemard, G., Simon, L.: Predicting learnt clauses quality in modern SAT solvers. In: Proceedings of the 21st International Jont Conference on Artifical Intelligence, IJCAI 2009, pp. 399\u2013404. Morgan Kaufmann Publishers Inc., San Francisco (2009)"},{"key":"9_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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":"9_CR4","unstructured":"Audemard, G., Simon, L.: Glucose 2.3 in the SAT 2013 Competition. In: Proceedings of SAT Competition 2013, pp. 42\u201343 (2013)"},{"key":"9_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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":"9_CR6","unstructured":"Biere, A.: Lingeling, Plingeling, PicoSAT and PrecoSAT at SAT Race 2010. FMV Report Series Technical report 10(1) (2010)"},{"key":"9_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"405","DOI":"10.1007\/978-3-319-24318-4_29","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2015","author":"A Biere","year":"2015","unstructured":"Biere, A., Fr\u00f6hlich, A.: Evaluating CDCL variable scoring schemes. In: Heule, M., Weaver, S. (eds.) SAT 2015. LNCS, vol. 9340, pp. 405\u2013422. Springer, Heidelberg (2015). doi: 10.1007\/978-3-319-24318-4_29"},{"key":"9_CR8","doi-asserted-by":"crossref","first-page":"145","DOI":"10.1287\/opre.5.1.63","volume":"5","author":"RG Brown","year":"1957","unstructured":"Brown, R.G.: Exponential smoothing for predicting demand. Oper. Res. 5, 145\u2013145 (1957)","journal-title":"Oper. Res."},{"key":"9_CR9","doi-asserted-by":"crossref","unstructured":"Cadar, C., Ganesh, V., Pawlowski, P.M., Dill, D.L., Engler, D.R.: EXE: automatically generating inputs of death. In: Proceedings of the 13th ACM Conference on Computer and Communications Security, CCS 2006, pp. 322\u2013335. ACM, New York (2006)","DOI":"10.1145\/1180405.1180445"},{"key":"9_CR10","unstructured":"Carvalho, E., Marques-Silva, J.P.: Using rewarding mechanisms for improving branching heuristics. In: Proceedings of the Seventh International Conference on Theory and Applications of Satisfiability Testing (2004)"},{"issue":"1","key":"9_CR11","doi-asserted-by":"crossref","first-page":"7","DOI":"10.1023\/A:1011276507260","volume":"19","author":"E Clarke","year":"2001","unstructured":"Clarke, E., Biere, A., Raimi, R., Zhu, Y.: Bounded model checking using satisfiability solving. Form. Methods Syst. Des. 19(1), 7\u201334 (2001)","journal-title":"Form. Methods Syst. Des."},{"key":"9_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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)"},{"issue":"4","key":"9_CR13","first-page":"848","volume":"88","author":"I Erev","year":"1998","unstructured":"Erev, I., Roth, A.E.: Predicting how people play games: reinforcement learning in experimental games with unique, mixed strategy equilibria. Am. Econ. Rev. 88(4), 848\u2013881 (1998)","journal-title":"Am. Econ. Rev."},{"key":"9_CR14","doi-asserted-by":"crossref","unstructured":"Fr\u00f6hlich, A., Biere, A., Wintersteiger, C., Hamadi, Y.: Stochastic local search for satisfiability modulo theories. In: Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence, AAAI 2015, pp. 1136\u20131143. AAAI Press (2015)","DOI":"10.1609\/aaai.v29i1.9372"},{"key":"9_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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.) HVC 2005. LNCS, vol. 3875, pp. 76\u201389. Springer, Heidelberg (2006)"},{"issue":"12","key":"9_CR16","doi-asserted-by":"crossref","first-page":"1549","DOI":"10.1016\/j.dam.2006.10.007","volume":"155","author":"E Goldberg","year":"2007","unstructured":"Goldberg, E., Novikov, Y.: BerkMin: a fast and robust sat-solver. Discrete Appl. Math. 155(12), 1549\u20131561 (2007)","journal-title":"Discrete Appl. Math."},{"issue":"1\u20134","key":"9_CR17","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1007\/BF01531077","volume":"1","author":"RG Jeroslow","year":"1990","unstructured":"Jeroslow, R.G., Wang, J.: Solving propositional satisfiability problems. Ann. Math. Artif. Intell. 1(1\u20134), 167\u2013187 (1990)","journal-title":"Ann. Math. Artif. Intell."},{"key":"9_CR18","doi-asserted-by":"crossref","first-page":"344","DOI":"10.1016\/S1571-0653(04)00332-4","volume":"9","author":"MG Lagoudakis","year":"2001","unstructured":"Lagoudakis, M.G., Littman, M.L.: Learning to select branching rules in the DPLL procedure for satisfiability. Electron. Notes Discrete Math. 9, 344\u2013359 (2001)","journal-title":"Electron. Notes Discrete Math."},{"key":"9_CR19","doi-asserted-by":"crossref","unstructured":"Liang, J.H., Ganesh, V., Poupart, P., Czarnecki, K.: Exponential recency weighted average branching heuristic for SAT solvers. In: Proceedings of AAAI 2016 (2016)","DOI":"10.1007\/978-3-319-40970-2_9"},{"key":"9_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1007\/978-3-319-26287-1_14","volume-title":"Hardware and Software: Verification and Testing","author":"JH Liang","year":"2015","unstructured":"Liang, J.H., Ganesh, V., Zulkoski, E., Zaman, A., Czarnecki, K.: Understanding VSIDS branching heuristics in\u00a0conflict-driven clause-learning SAT solvers. In: Liang, J.H., Ganesh, V., Zulkoski, E., Zaman, A., Czarnecki, K. (eds.) HVC 2015. LNCS, vol. 9434, pp. 225\u2013241. Springer, Heidelberg (2015). doi: 10.1007\/978-3-319-26287-1_14"},{"key":"9_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"464","DOI":"10.1007\/978-3-642-40627-0_36","volume-title":"Principles and Practice of Constraint Programming","author":"M Loth","year":"2013","unstructured":"Loth, M., Sebag, M., Hamadi, Y., Schoenauer, M.: Bandit-based search for constraint programming. In: Schulte, C. (ed.) CP 2013. LNCS, vol. 8124, pp. 464\u2013480. Springer, Heidelberg (2013)"},{"key":"9_CR22","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"crossref","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":"9_CR23","doi-asserted-by":"crossref","unstructured":"Marques-Silva, J.P., Sakallah, K.A.: GRASP-a new search algorithm for satisfiability. In: Proceedings of the 1996 IEEE\/ACM International Conference on Computer-aided Design, ICCAD 1996, pp. 220\u2013227. IEEE Computer Society, Washington, DC (1996)","DOI":"10.1109\/ICCAD.1996.569607"},{"key":"9_CR24","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 Annual Design Automation Conference, DAC 2001, pp. 530\u2013535. ACM, New York (2001)","DOI":"10.1145\/378239.379017"},{"key":"9_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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":"9_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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":"9_CR27","first-page":"483","volume-title":"Handbook of Satisfiability","author":"J Rintanen","year":"2009","unstructured":"Rintanen, J.: Planning and SAT. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, vol. 185, pp. 483\u2013504. IOS Press, Amsterdam (2009)"},{"key":"9_CR28","unstructured":"Ryan, L.: Efficient Algorithms for Clause-Learning SAT Solvers. Master\u2019s thesis, Simon Fraser University (2004)"},{"key":"9_CR29","unstructured":"Soos, M.: CryptoMiniSat v4. In: SAT Competition, p. 23 (2014)"},{"key":"9_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"367","DOI":"10.1007\/978-3-319-08587-6_28","volume-title":"Automated Reasoning","author":"A Stump","year":"2014","unstructured":"Stump, A., Sutcliffe, G., Tinelli, C.: StarExec: a cross-community infrastructure for logic solving. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS, vol. 8562, pp. 367\u2013373. Springer, Heidelberg (2014)"},{"key":"9_CR31","volume-title":"Reinforcement Learning: An Introduction","author":"RS Sutton","year":"1998","unstructured":"Sutton, R.S., Barto, A.G.: Reinforcement Learning: An Introduction, vol. 1. MIT Press Cambridge, Massachusetts (1998)"},{"issue":"3","key":"9_CR32","doi-asserted-by":"crossref","first-page":"387","DOI":"10.3758\/BF03193783","volume":"12","author":"E Yechiam","year":"2005","unstructured":"Yechiam, E., Busemeyer, J.R.: Comparison of basic assumptions embedded in learning models for experience-based decision making. Psychon. Bull. Rev. 12(3), 387\u2013402 (2005)","journal-title":"Psychon. Bull. Rev."},{"key":"9_CR33","unstructured":"Zhang, L., Madigan, C.F., Moskewicz, M.H., Malik, S.: Efficient conflict driven learning in a boolean satisfiability solver. In: Proceedings of the 2001 IEEE\/ACM International Conference on Computer-aided Design, ICCAD 2001, pp. 279\u2013285. IEEE Press, Piscataway (2001)"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing \u2013 SAT 2016"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-40970-2_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,7,1]],"date-time":"2022-07-01T12:13:49Z","timestamp":1656677629000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-40970-2_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319409696","9783319409702"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-40970-2_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016]]}}}