{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,16]],"date-time":"2025-10-16T06:56:07Z","timestamp":1760597767138,"version":"3.40.3"},"publisher-location":"Cham","reference-count":28,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319662626"},{"type":"electronic","value":"9783319662633"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"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":[[2017]]},"DOI":"10.1007\/978-3-319-66263-3_8","type":"book-chapter","created":{"date-parts":[[2017,8,8]],"date-time":"2017-08-08T08:05:11Z","timestamp":1502179511000},"page":"119-135","source":"Crossref","is-referenced-by-count":16,"title":["An Empirical Study of Branching Heuristics Through the Lens of Global Learning Rate"],"prefix":"10.1007","author":[{"given":"Jia Hui","family":"Liang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hari Govind","family":"V.K.","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pascal","family":"Poupart","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Krzysztof","family":"Czarnecki","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Vijay","family":"Ganesh","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,8,9]]},"reference":[{"key":"8_CR1","unstructured":"https:\/\/sites.google.com\/a\/gsd.uwaterloo.ca\/maplesat\/"},{"key":"8_CR2","unstructured":"https:\/\/sites.google.com\/a\/gsd.uwaterloo.ca\/maplesat\/sgd"},{"key":"8_CR3","unstructured":"Audemard, G., Simon, L.: Predicting learnt clauses quality in modern SAT solvers. In: Proceedings of the 21st International Joint Conference on Artificial Intelligence, IJCAI 2009, pp. 399\u2013404. Morgan Kaufmann Publishers Inc., San Francisco (2009)"},{"key":"8_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":"8_CR5","unstructured":"Biere, A.: Lingeling, Plingeling, PicoSAT and PrecoSAT at SAT Race 2010. FMV Report Series Technical Report 10(1) (2010)"},{"key":"8_CR6","doi-asserted-by":"crossref","unstructured":"Bottou, L.: On-line Learning in Neural Networks. On-line Learning and Stochastic Approximations, pp. 9\u201342. Cambridge University Press, New York (1998)","DOI":"10.1017\/CBO9780511569920.003"},{"key":"8_CR7","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":"8_CR8","unstructured":"Carvalho, E., Silva, J.P.M.: Using rewarding mechanisms for improving branching heuristics. In: Online Proceedings of The Seventh International Conference on Theory and Applications of Satisfiability Testing, SAT 2004, 10\u201313 May 2004, Vancouver, BC, Canada, (2004)"},{"issue":"1","key":"8_CR9","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. Formal Meth. Syst. Des. 19(1), 7\u201334 (2001)","journal-title":"Formal Meth. Syst. Des."},{"issue":"2","key":"8_CR10","doi-asserted-by":"crossref","first-page":"215","DOI":"10.1111\/j.2517-6161.1958.tb00292.x","volume":"20","author":"DR Cox","year":"1958","unstructured":"Cox, D.R.: The regression analysis of binary sequences. J. Roy. Stat. Soc.: Ser. B (Methodol.) 20(2), 215\u2013242 (1958)","journal-title":"J. Roy. Stat. Soc.: Ser. B (Methodol.)"},{"key":"8_CR11","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). doi: 10.1007\/978-3-540-24605-3_37"},{"issue":"4","key":"8_CR12","first-page":"507","volume":"10","author":"RA Fisher","year":"1915","unstructured":"Fisher, R.A.: Frequency distribution of the values of the correlation coefficient in samples from an indefinitely large population. Biometrika 10(4), 507\u2013521 (1915)","journal-title":"Biometrika"},{"issue":"12","key":"8_CR13","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":"8_CR14","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":"8_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1007\/978-3-642-21581-0_27","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2011","author":"H Katebi","year":"2011","unstructured":"Katebi, H., Sakallah, K.A., Marques-Silva, J.P.: Empirical study of the anatomy of modern SAT solvers. In: Sakallah, K.A., Simon, L. (eds.) SAT 2011. LNCS, vol. 6695, pp. 343\u2013356. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-21581-0_27"},{"key":"8_CR16","unstructured":"Kautz, H., Selman, B.: Planning as satisfiability. In: Proceedings of the 10th European Conference on Artificial Intelligence, ECAI 1992, pp. 359\u2013363. Wiley Inc., New York (1992)"},{"key":"8_CR17","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":"8_CR18","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 the Thirtieth AAAI Conference on Artificial Intelligence, AAAI 2016, pp. 3434\u20133440. AAAI Press (2016)","DOI":"10.1007\/978-3-319-40970-2_9"},{"key":"8_CR19","doi-asserted-by":"crossref","unstructured":"Liang, J.H., Ganesh, V., Poupart, P., Czarnecki, K.: Learning rate based branching heuristic for SAT solvers. In: Proceedings of the 19th International Conference on Theory and Applications of Satisfiability Testing, SAT 2016, Bordeaux, France, 5\u20138 July 2016, pp. 123\u2013140 (2016)","DOI":"10.1007\/978-3-319-40970-2_9"},{"issue":"4","key":"8_CR20","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1016\/0020-0190(93)90029-9","volume":"47","author":"M Luby","year":"1993","unstructured":"Luby, M., Sinclair, A., Zuckerman, D.: Optimal speedup of Las Vegas algorithms. Inf. Process. Lett. 47(4), 173\u2013180 (1993)","journal-title":"Inf. Process. Lett."},{"key":"8_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"62","DOI":"10.1007\/3-540-48159-1_5","volume-title":"Progress in Artificial Intelligence","author":"JP Marques-Silva","year":"1999","unstructured":"Marques-Silva, J.P.: The impact of branching heuristics in propositional satisfiability algorithms. In: Barahona, P., Alferes, J.J. (eds.) EPIA 1999. LNCS, vol. 1695, pp. 62\u201374. Springer, Heidelberg (1999). doi: 10.1007\/3-540-48159-1_5"},{"key":"8_CR22","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, D.C. (1996)","DOI":"10.1109\/ICCAD.1996.569607"},{"key":"8_CR23","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":"8_CR24","volume-title":"Machine Learning: A Probabilistic Perspective","author":"KP Murphy","year":"2012","unstructured":"Murphy, K.P.: Machine Learning: A Probabilistic Perspective. The MIT Press, Cambridge (2012)"},{"key":"8_CR25","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). doi: 10.1007\/978-3-540-72788-0_28"},{"key":"8_CR26","unstructured":"Soos, M.: CryptoMiniSat v4. SAT Competition, p. 23 (2014)"},{"issue":"1","key":"8_CR27","doi-asserted-by":"crossref","first-page":"72","DOI":"10.2307\/1412159","volume":"15","author":"C Spearman","year":"1904","unstructured":"Spearman, C.: The proof and measurement of association between two things. Am. J. Psychol. 15(1), 72\u2013101 (1904)","journal-title":"Am. J. Psychol."},{"key":"8_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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, Cham (2014). doi: 10.1007\/978-3-319-08587-6_28"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing \u2013 SAT 2017"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-66263-3_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,6,26]],"date-time":"2024-06-26T01:39:38Z","timestamp":1719365978000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-66263-3_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319662626","9783319662633"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-66263-3_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}