{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,24]],"date-time":"2025-06-24T21:40:03Z","timestamp":1750801203123,"version":"3.41.0"},"publisher-location":"Cham","reference-count":26,"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_5","type":"book-chapter","created":{"date-parts":[[2017,8,8]],"date-time":"2017-08-08T08:05:11Z","timestamp":1502179511000},"page":"65-82","source":"Crossref","is-referenced-by-count":0,"title":["On the Community Structure of Bounded Model Checking SAT Problems"],"prefix":"10.1007","author":[{"given":"Guillaume","family":"Baud-Berthier","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jes\u00fas","family":"Gir\u00e1ldez-Cru","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Laurent","family":"Simon","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,8,9]]},"reference":[{"key":"5_CR1","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). doi: 10.1007\/978-3-642-31612-8_31"},{"key":"5_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"238","DOI":"10.1007\/978-3-319-24318-4_18","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2015","author":"C Ans\u00f3tegui","year":"2015","unstructured":"Ans\u00f3tegui, C., Gir\u00e1ldez-Cru, J., Levy, J., Simon, L.: using community structure to detect relevant learnt clauses. In: Heule, M., Weaver, S. (eds.) SAT 2015. LNCS, vol. 9340, pp. 238\u2013254. Springer, Cham (2015). doi: 10.1007\/978-3-319-24318-4_18"},{"key":"5_CR3","unstructured":"Audemard, G., Simon, L.: Predicting learnt clauses quality in modern sat solvers. In: Proceeding of IJCAI 2009, pp. 399\u2013404 (2009)"},{"key":"5_CR4","unstructured":"Biere, A.: Splatz, Lingeling, Plingeling, Treengeling, YalSAT Entering the SAT Competition 2016. In: Proceeding of the SAT Competition 2016, Department of Computer Science Series of Publications B, vol. B-2016-1, pp. 44\u201345. University of Helsinki (2016)"},{"key":"5_CR5","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 and 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, pp. 193\u2013207. Springer, Heidelberg (1999). doi: 10.1007\/3-540-49059-0_14"},{"issue":"10","key":"5_CR6","doi-asserted-by":"crossref","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. Exper. 2008(10), P10008 (2008)","journal-title":"J. Stat. Mech. Theor. Exper."},{"key":"5_CR7","doi-asserted-by":"crossref","unstructured":"Darwiche, A., Pipatsrisawat, K.: Complete Algorithms, chap. 3, pp. 99\u2013130. IOS Press (2009)","DOI":"10.3233\/978-1-58603-929-5-99"},{"key":"5_CR8","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). doi: 10.1007\/11499107_5"},{"key":"5_CR9","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":"3\u20135","key":"5_CR10","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1016\/j.physrep.2009.11.002","volume":"486","author":"S Fortunato","year":"2010","unstructured":"Fortunato, S.: Community detection in graphs. Phys. Rep. 486(3\u20135), 75\u2013174 (2010)","journal-title":"Phys. Rep."},{"key":"5_CR11","unstructured":"Gir\u00e1ldez-Cru, J., Levy, J.: A modularity-based random SAT instances generator. In: Proceeding of IJCAI 2015, pp. 1952\u20131958 (2015)"},{"key":"5_CR12","doi-asserted-by":"crossref","first-page":"119","DOI":"10.1016\/j.artint.2016.06.001","volume":"238","author":"J Gir\u00e1ldez-Cru","year":"2016","unstructured":"Gir\u00e1ldez-Cru, J., Levy, J.: Generating SAT instances with community structure. Artif. Intell. 238, 119\u2013134 (2016)","journal-title":"Artif. Intell."},{"key":"5_CR13","doi-asserted-by":"crossref","unstructured":"Gir\u00e1ldez-Cru, J., Levy, J.: Locality in random SAT instances. In: Proceeding of IJCAI 2017 (2017)","DOI":"10.24963\/ijcai.2017\/89"},{"key":"5_CR14","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":"CP 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. 1330, pp. 121\u2013135. Springer, Heidelberg (1997). doi: 10.1007\/BFb0017434"},{"key":"5_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/978-3-319-40970-2_9","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2016","author":"JH Liang","year":"2016","unstructured":"Liang, J.H., Ganesh, V., Poupart, P., Czarnecki, K.: Learning rate based branching heuristic for SAT solvers. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 123\u2013140. Springer, Cham (2016). doi: 10.1007\/978-3-319-40970-2_9"},{"issue":"4","key":"5_CR16","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":"5_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1007\/978-3-642-39071-5_14","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2013","author":"R Martins","year":"2013","unstructured":"Martins, R., Manquinho, V., Lynce, I.: Community-based partitioning for MaxSAT solving. In: J\u00e4rvisalo, M., Van Gelder, A. (eds.) SAT 2013. LNCS, vol. 7962, pp. 182\u2013191. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-39071-5_14"},{"key":"5_CR18","doi-asserted-by":"crossref","unstructured":"Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient SAT solver. In: Proceeding of DAC 2001, pp. 530\u2013535 (2001)","DOI":"10.1145\/378239.379017"},{"key":"5_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"272","DOI":"10.1007\/978-3-319-24318-4_20","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2015","author":"M Neves","year":"2015","unstructured":"Neves, M., Martins, R., Janota, M., Lynce, I., Manquinho, V.: Exploiting resolution-based representations for MaxSAT solving. In: Heule, M., Weaver, S. (eds.) SAT 2015. LNCS, vol. 9340, pp. 272\u2013286. Springer, Cham (2015). doi: 10.1007\/978-3-319-24318-4_20"},{"issue":"2","key":"5_CR20","doi-asserted-by":"crossref","first-page":"026113","DOI":"10.1103\/PhysRevE.69.026113","volume":"69","author":"MEJ Newman","year":"2004","unstructured":"Newman, M.E.J., Girvan, M.: Finding and evaluating community structure in networks. Phys. Rev. E 69(2), 026113 (2004)","journal-title":"Phys. Rev. E"},{"key":"5_CR21","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, Cham (2014). doi: 10.1007\/978-3-319-09284-3_20"},{"key":"5_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/978-3-319-24318-4_23","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2015","author":"C Oh","year":"2015","unstructured":"Oh, C.: Between SAT and UNSAT: the fundamental difference in CDCL SAT. In: Heule, M., Weaver, S. (eds.) SAT 2015. LNCS, vol. 9340, pp. 307\u2013323. Springer, Cham (2015). doi: 10.1007\/978-3-319-24318-4_23"},{"issue":"2","key":"5_CR23","doi-asserted-by":"crossref","first-page":"512","DOI":"10.1016\/j.artint.2010.10.002","volume":"175","author":"K Pipatsrisawat","year":"2011","unstructured":"Pipatsrisawat, K., Darwiche, A.: On the power of clause-learning SAT solvers as resolution engines. Artif. Intell. 175(2), 512\u2013525 (2011)","journal-title":"Artif. Intell."},{"issue":"5","key":"5_CR24","doi-asserted-by":"crossref","first-page":"506","DOI":"10.1109\/12.769433","volume":"48","author":"JPM Silva","year":"1999","unstructured":"Silva, J.P.M., Sakallah, K.A.: GRASP: A search algorithm for propositional satisfiability. IEEE Trans. Comput. 48(5), 506\u2013521 (1999)","journal-title":"IEEE Trans. Comput."},{"key":"5_CR25","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, pp. 348\u2013356. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-33558-7_27"},{"issue":"1","key":"5_CR26","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1023\/B:FORM.0000004785.67232.f8","volume":"24","author":"O Strichman","year":"2004","unstructured":"Strichman, O.: Accelerating bounded model checking of safety properties. Form. Methods Syst. Des. 24(1), 5\u201324 (2004)","journal-title":"Form. Methods Syst. Des."}],"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_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,24]],"date-time":"2025-06-24T20:59:48Z","timestamp":1750798788000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-66263-3_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319662626","9783319662633"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-66263-3_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}