{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,11,13]],"date-time":"2026-11-13T17:56:59Z","timestamp":1794592619437,"version":"4.9.1"},"publisher-location":"Cham","reference-count":43,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319262864","type":"print"},{"value":"9783319262871","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-26287-1_14","type":"book-chapter","created":{"date-parts":[[2015,10,26]],"date-time":"2015-10-26T01:44:58Z","timestamp":1445823898000},"page":"225-241","source":"Crossref","is-referenced-by-count":34,"title":["Understanding VSIDS Branching Heuristics in\u00a0Conflict-Driven Clause-Learning 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":"Ed","family":"Zulkoski","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Atulan","family":"Zaman","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":[[2015,11,28]]},"reference":[{"key":"14_CR1","unstructured":"Starexec. http:\/\/www.starexec.org\/"},{"key":"14_CR2","unstructured":"Proceedings of Past SAT Conferences (2013). http:\/\/www.satisfiability.org"},{"key":"14_CR3","unstructured":"SAT Competition Website (2013). http:\/\/www.satcompetition.org"},{"key":"14_CR4","unstructured":"SHARCNET Website (2013). https:\/\/www.sharcnet.ca"},{"key":"14_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1007\/978-3-642-02777-2_13","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2009","author":"A Atserias","year":"2009","unstructured":"Atserias, A., Fichte, J.K., Thurley, M.: Clause-learning algorithms with many restarts and bounded-width resolution. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 114\u2013127. Springer, Heidelberg (2009)"},{"key":"14_CR6","first-page":"399","volume":"9","author":"G Audemard","year":"2009","unstructured":"Audemard, G., Simon, L.: Glucose: a solver that predicts learnt clauses quality. IJCAI 9, 399\u2013404 (2009)","journal-title":"IJCAI"},{"key":"14_CR7","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. J. Artif. Intell. Res. (JAIR) 22, 319\u2013351 (2004)","journal-title":"J. Artif. Intell. Res. (JAIR)"},{"key":"14_CR8","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":"14_CR9","unstructured":"Biere, A.: Lingeling (2010)"},{"issue":"10","key":"14_CR10","doi-asserted-by":"publisher","first-page":"P10008","DOI":"10.1088\/1742-5468\/2008\/10\/P10008","volume":"2008","author":"VD Blondel","year":"2008","unstructured":"Blondel, V.D., Guillaume, J.L., Lambiotte, R., Lefebvre, E.: Fast unfolding of communities in large networks. J. Stat. Mech. Theor. Exp. 2008(10), P10008 (2008)","journal-title":"J. Stat. Mech. Theor. Exp."},{"key":"14_CR11","volume-title":"Exponential Smoothing for Predicting Demand","author":"RG Brown","year":"1956","unstructured":"Brown, R.G.: Exponential Smoothing for Predicting Demand. Little, Cambridge (1956)"},{"key":"14_CR12","unstructured":"Buro, M., B\u00fcning, H.K.: Report on a SAT competition. Fachbereich Math.-Informatik, Univ. Gesamthochschule (1992)"},{"issue":"6","key":"14_CR13","doi-asserted-by":"publisher","first-page":"066111","DOI":"10.1103\/PhysRevE.70.066111","volume":"70","author":"A Clauset","year":"2004","unstructured":"Clauset, A., Newman, M.E., Moore, C.: Finding community structure in very large networks. Phys. Rev. E 70(6), 066111 (2004)","journal-title":"Phys. Rev. E"},{"key":"14_CR14","doi-asserted-by":"crossref","unstructured":"Cook, S.A.: The complexity of theorem-proving procedures. In: Proceedings of the Third Annual ACM Symposium on Theory of Computing, STOC 1971, pp. 151\u2013158. ACM, New York (1971)","DOI":"10.1145\/800157.805047"},{"key":"14_CR15","unstructured":"Een, N., S\u00f6rensson, N.: MiniSat: a SAT solver with conflict-clause minimization. In: SAT 2005 (2005)"},{"issue":"2","key":"14_CR16","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1016\/S0378-8733(96)00300-0","volume":"19","author":"K Faust","year":"1997","unstructured":"Faust, K.: Centrality in affiliation networks. Soc. Netw. 19(2), 157\u2013191 (1997)","journal-title":"Soc. Netw."},{"issue":"4","key":"14_CR17","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"},{"key":"14_CR18","unstructured":"Freeman, J.W.: Improvements to propositional satisfiability search algorithms. Ph.D. thesis, Philadelphia, PA, USA (1995). uMI Order No. GAX95-32175"},{"issue":"3","key":"14_CR19","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1016\/0378-8733(78)90021-7","volume":"1","author":"L Freeman","year":"1979","unstructured":"Freeman, L.: Centrality in social networks conceptual clarification. Soc. Netw. 1(3), 215\u2013239 (1979)","journal-title":"Soc. Netw."},{"issue":"121","key":"14_CR20","doi-asserted-by":"publisher","first-page":"124","DOI":"10.2307\/2223319","volume":"31","author":"C Gini","year":"1921","unstructured":"Gini, C.: Measurement of inequality of incomes. Econ. J. 31(121), 124\u2013126 (1921)","journal-title":"Econ. J."},{"issue":"12","key":"14_CR21","doi-asserted-by":"publisher","first-page":"7821","DOI":"10.1073\/pnas.122653799","volume":"99","author":"M Girvan","year":"2002","unstructured":"Girvan, M., Newman, M.E.: Community structure in social and biological networks. Proc. Natl. Acad. Sci. 99(12), 7821\u20137826 (2002)","journal-title":"Proc. Natl. Acad. Sci."},{"key":"14_CR22","doi-asserted-by":"crossref","unstructured":"Gloor, P., Krauss, J., Nann, S., Fischbach, K., Schoder, D.: Web science 2.0: identifying trends through semantic social network analysis. In: 2009 International Conference on Computational Science and Engineering, CSE 2009, vol. 4, pp. 215\u2013222, August 2009","DOI":"10.1109\/CSE.2009.186"},{"key":"14_CR23","volume-title":"Matrix Computations","author":"GH Golub","year":"2012","unstructured":"Golub, G.H., Van Loan, C.F.: Matrix Computations. JHU Press, Baltimore (2012)"},{"issue":"4","key":"14_CR24","first-page":"245","volume":"6","author":"Y Hamadi","year":"2009","unstructured":"Hamadi, Y., Jabbour, S., Sais, L.: ManySAT: a parallel SAT solver. JSAT 6(4), 245\u2013262 (2009)","journal-title":"JSAT"},{"key":"14_CR25","volume-title":"Stochastic Local Search: Foundations & Applications","author":"HH Hoos","year":"2004","unstructured":"Hoos, H.H., St\u00fctzle, T.: Stochastic Local Search: Foundations & Applications. Morgan Kaufmann Publishers Inc., San Francisco (2004)"},{"issue":"1","key":"14_CR26","first-page":"293","volume":"43","author":"R Huang","year":"2012","unstructured":"Huang, R., Chen, Y., Zhang, W.: SAS+ planning as satisfiability. J. Artif. Int. Res. 43(1), 293\u2013328 (2012)","journal-title":"J. Artif. Int. Res."},{"key":"14_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"483","DOI":"10.1007\/978-3-642-31612-8_46","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2012","author":"M Iser","year":"2012","unstructured":"Iser, M., Taghdiri, M., Sinz, C.: Optimizing MiniSAT variable orderings for the relational model finder kodkod. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 483\u2013484. Springer, Heidelberg (2012)"},{"issue":"1\u20134","key":"14_CR28","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. Ann. Math. Artif. Intell. 1(1\u20134), 167\u2013187 (1990)","journal-title":"Ann. Math. Artif. Intell."},{"key":"14_CR29","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)"},{"key":"14_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/978-3-642-33558-7_27","volume-title":"Principles and Practice of Constraint Programming","author":"G Katsirelos","year":"2012","unstructured":"Katsirelos, G., Simon, L.: Eigenvector centrality in industrial SAT instances. In: Milano, M. (ed.) CP 2012. LNCS, vol. 7514, pp. 348\u2013356. Springer, Heidelberg (2012)"},{"key":"14_CR31","volume-title":"Trading Systems and Methods","author":"PJ Kaufman","year":"2013","unstructured":"Kaufman, P.J.: Trading Systems and Methods. Wiley, New York (2013)"},{"key":"14_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"360","DOI":"10.1007\/11527695_27","volume-title":"Theory and Applications of Satisfiability Testing","author":"YS Mahajan","year":"2005","unstructured":"Mahajan, Y.S., Fu, Z., Malik, S.: Zchaff2004: an efficient SAT solver. In: H. Hoos, H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol. 3542, pp. 360\u2013375. Springer, Heidelberg (2005)"},{"key":"14_CR33","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)"},{"issue":"5","key":"14_CR34","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. Comput. 48(5), 506\u2013521 (1999)","journal-title":"IEEE Trans. Comput."},{"key":"14_CR35","unstructured":"Moskewicz, M.W., Madigan, C.F., Malik, S.: Method and system for efficient implementation of boolean satisfiability (26 August 2008), US Patent 7,418,369"},{"key":"14_CR36","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":"14_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"375","DOI":"10.1007\/978-3-642-14186-7_35","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2010","author":"A Nadel","year":"2010","unstructured":"Nadel, A., Ryvchin, V.: Assignment stack shrinking. In: Strichman, O., Szeider, S. (eds.) SAT 2010. LNCS, vol. 6175, pp. 375\u2013381. Springer, Heidelberg (2010)"},{"key":"14_CR38","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":"14_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"654","DOI":"10.1007\/978-3-642-04244-7_51","volume-title":"Principles and Practice of Constraint Programming - CP 2009","author":"K Pipatsrisawat","year":"2009","unstructured":"Pipatsrisawat, K., Darwiche, A.: On the power of clause-learning SAT solvers with restarts. In: Gent, I.P. (ed.) CP 2009. LNCS, vol. 5732, pp. 654\u2013668. Springer, Heidelberg (2009)"},{"issue":"1","key":"14_CR40","doi-asserted-by":"publisher","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."},{"issue":"5","key":"14_CR41","doi-asserted-by":"publisher","first-page":"269","DOI":"10.2307\/2689388","volume":"53","author":"PD Straffin","year":"1980","unstructured":"Straffin, P.D.: Linear algebra in geography: eigenvectors of networks. Math. Mag. 53(5), 269\u2013276 (1980)","journal-title":"Math. Mag."},{"key":"14_CR42","doi-asserted-by":"crossref","unstructured":"Yu, P.S., Li, X., Liu, B.: Adding the temporal dimension to search - a case study in publication search. In: Skowron, A., Agrawal, R., Luck, M., Yamaguchi, T., Morizet-Mahoudeaux, P., Liu, J., Zhong, N. (eds.) Web Intelligence, pp. 543\u2013549. IEEE Computer Society (2005)","DOI":"10.1109\/WI.2005.21"},{"key":"14_CR43","unstructured":"Zhang, W., Pan, G., Wu, Z., Li, S.: Online community detection for large complex networks. In: Proceedings of the Twenty-Third international joint conference on Artificial Intelligence, pp. 1903\u20131909. AAAI Press (2013)"}],"container-title":["Lecture Notes in Computer Science","Hardware and Software: Verification and Testing"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-26287-1_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,31]],"date-time":"2025-05-31T00:13:13Z","timestamp":1748650393000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-26287-1_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319262864","9783319262871"],"references-count":43,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-26287-1_14","relation":{"is-part-of":[{"id-type":"doi","id":"https:\/\/doi.org\/10.1007\/978-3-319-26287-1","asserted-by":"object"}]},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]}}}