{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T23:30:41Z","timestamp":1742945441733,"version":"3.40.3"},"publisher-location":"Cham","reference-count":48,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030802226"},{"type":"electronic","value":"9783030802233"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"DOI":"10.1007\/978-3-030-80223-3_25","type":"book-chapter","created":{"date-parts":[[2021,7,1]],"date-time":"2021-07-01T14:13:49Z","timestamp":1625148829000},"page":"359-376","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["On the Hierarchical Community Structure of Practical Boolean Formulas"],"prefix":"10.1007","author":[{"given":"Chunxiao","family":"Li","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jonathan","family":"Chung","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Soham","family":"Mukherjee","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marc","family":"Vinyals","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Noah","family":"Fleming","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Antonina","family":"Kolokolova","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alice","family":"Mu","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":[[2021,7,2]]},"reference":[{"issue":"4","key":"25_CR1","doi-asserted-by":"publisher","first-page":"649","DOI":"10.1007\/s00037-011-0033-1","volume":"20","author":"M Alekhnovich","year":"2011","unstructured":"Alekhnovich, M., Razborov, A.: Satisfiability. Branch-width and Tseitin tautologies. Comput. Complex. 20(4), 649\u2013678 (2011). https:\/\/doi.org\/10.1007\/s00037-011-0033-1","journal-title":"Comput. Complex."},{"key":"25_CR2","doi-asserted-by":"publisher","unstructured":"Ans\u00f3tegui, C., Bonet, M.L., Gir\u00e1ldez-Cru, J., Levy, J.: The fractal dimension of SAT formulas. In: Proceedings of the 7th International Joint Conference on Automated Reasoning - IJCAR 2014, pp. 107\u2013121 (2014). https:\/\/doi.org\/10.1007\/978-3-319-08587-6_8","DOI":"10.1007\/978-3-319-08587-6_8"},{"key":"25_CR3","unstructured":"Ans\u00f3tegui, C., Bonet, M.L., Levy, J.: Towards industrial-like random SAT instances. In: IJCAI 2009, Proceedings of the 21st International Joint Conference on Artificial Intelligence, pp. 387\u2013392 (2009)"},{"key":"25_CR4","doi-asserted-by":"publisher","unstructured":"Ans\u00f3tegui, C., Gir\u00e1ldez-Cru, J., Levy, J.: The community structure of SAT formulas. In: Proceedings of the 15th International Conference on Theory and Applications of Satisfiability Testing - SAT 2012, pp. 410\u2013423 (2012). https:\/\/doi.org\/10.1007\/978-3-642-31612-8_31","DOI":"10.1007\/978-3-642-31612-8_31"},{"key":"25_CR5","doi-asserted-by":"crossref","unstructured":"Ben-Sasson, E., Wigderson, A.: Short proofs are narrow\u2014resolution made simple. J. ACM (JACM) 48(2), 149\u2013169 (2001)","DOI":"10.1145\/375827.375835"},{"key":"25_CR6","doi-asserted-by":"publisher","unstructured":"Bl\u00e4sius, T., Friedrich, T., G\u00f6bel, A., Levy, J., Rothenberger, R.: The impact of heterogeneity and geometry on the proof complexity of random satisfiability. In: Proceedings of the 2021 ACM-SIAM Symposium on Discrete Algorithms, SODA 2021, pp. 42\u201353 (2021). https:\/\/doi.org\/10.1137\/1.9781611976465.4","DOI":"10.1137\/1.9781611976465.4"},{"key":"25_CR7","doi-asserted-by":"publisher","unstructured":"Blondel, V., Guillaume, J.L., Lambiotte, R., Lefebvre, E.: Fast unfolding of communities in large networks. J. Stat. Mech. Theory Exp. 2008, P10008 (2008). https:\/\/doi.org\/10.1088\/1742-5468\/2008\/10\/P10008","DOI":"10.1088\/1742-5468\/2008\/10\/P10008"},{"issue":"1\u20132","key":"25_CR8","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1016\/S0004-3702(96)00047-1","volume":"90","author":"AL Blum","year":"1997","unstructured":"Blum, A.L., Furst, M.L.: Fast planning through planning graph analysis. Artif. Intell. 90(1\u20132), 281\u2013300 (1997)","journal-title":"Artif. Intell."},{"key":"25_CR9","doi-asserted-by":"publisher","unstructured":"Breiman, L.: Random forests. Mach. Learn. 45(1), 5\u201332 (2001). https:\/\/doi.org\/10.1023\/A:1010933404324","DOI":"10.1023\/A:1010933404324"},{"issue":"2","key":"25_CR10","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1455518.1455522","volume":"12","author":"C Cadar","year":"2008","unstructured":"Cadar, C., Ganesh, V., Pawlowski, P.M., Dill, D.L., Engler, D.R.: EXE: automatically generating inputs of death. ACM Trans. Inf. Syst. Secur. (TISSEC) 12(2), 1\u201338 (2008)","journal-title":"ACM Trans. Inf. Syst. Secur. (TISSEC)"},{"key":"25_CR11","unstructured":"Cheeseman, P., Kanefsky, B., Taylor, W.M.: Where the really hard problems are. In: Proceedings of the 12th International Joint Conference on Artificial Intelligence IJCAI 1991, pp. 331\u2013337. (1991)"},{"key":"25_CR12","unstructured":"Clarke Jr, E.M., Grumberg, O., Kroening, D., Peled, D., Veith, H.: Model Checking. MIT Press (2018)"},{"issue":"7191","key":"25_CR13","doi-asserted-by":"publisher","first-page":"98","DOI":"10.1038\/nature06830","volume":"453","author":"A Clauset","year":"2008","unstructured":"Clauset, A., Moore, C., Newman, M.E.J.: Hierarchical structure and the prediction of missing links in networks. Nature 453(7191), 98\u2013101 (2008). https:\/\/doi.org\/10.1038\/nature06830","journal-title":"Nature"},{"key":"25_CR14","doi-asserted-by":"publisher","unstructured":"Coarfa, C., Demopoulos, D.D., San Miguel Aguirre, A., Subramanian, D., Vardi, M.Y.: Random $$3$$-SAT: the plot thickens. Constraints 8(3), 243\u2013261 (2003). https:\/\/doi.org\/10.1023\/A:1025671026963","DOI":"10.1023\/A:1025671026963"},{"key":"25_CR15","doi-asserted-by":"publisher","unstructured":"Cook, S.A.: The complexity of theorem-proving procedures. In: Proceedings of the 3rd Annual ACM Symposium on Theory of Computing, pp. 151\u2013158 (1971). https:\/\/doi.org\/10.1145\/800157.805047","DOI":"10.1145\/800157.805047"},{"key":"25_CR16","doi-asserted-by":"publisher","unstructured":"Dolby, J., Vaziri, M., Tip, F.: Finding bugs efficiently with a SAT solver. In: Proceedings of the 6th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT International Symposium on Foundations of Software Engineering, pp. 195\u2013204 (2007). https:\/\/doi.org\/10.1145\/1287624.1287653","DOI":"10.1145\/1287624.1287653"},{"key":"25_CR17","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). https:\/\/doi.org\/10.1007\/11499107_5"},{"issue":"1","key":"25_CR18","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1073\/pnas.0605965104","volume":"104","author":"S Fortunato","year":"2007","unstructured":"Fortunato, S., Barth\u00e9lemy, M.: Resolution limit in community detection. Proc. Natl. Acad. Sci. 104(1), 36\u201341 (2007). https:\/\/doi.org\/10.1073\/pnas.0605965104","journal-title":"Proc. Natl. Acad. Sci."},{"key":"25_CR19","doi-asserted-by":"crossref","unstructured":"Friedrich, T., Krohmer, A., Rothenberger, R., Sutton, A.M.: Phase transitions for scale-free SAT formulas. In: Proceedings of the Thirty-First AAAI Conference on Artificial Intelligence, AAAI 2017, pp. 3893\u20133899. AAAI Press (2017)","DOI":"10.1609\/aaai.v31i1.11133"},{"key":"25_CR20","doi-asserted-by":"crossref","unstructured":"Gir\u00e1ldez-Cru, J.: Beyond the structure of SAT formulas. Ph.D. thesis, Universitat Aut\u00f2noma de Barcelona (2016)","DOI":"10.1007\/s10601-016-9260-z"},{"key":"25_CR21","unstructured":"Gir\u00e1ldez-Cru, J., Levy, J.: A modularity-based random SAT instances generator. In: Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, IJCAI 2015, pp. 1952\u20131958 (2015). http:\/\/ijcai.org\/Abstract\/15\/277"},{"issue":"07","key":"25_CR22","doi-asserted-by":"publisher","first-page":"1250171","DOI":"10.1142\/S0218127412501714","volume":"22","author":"C Granell","year":"2012","unstructured":"Granell, C., Gomez, S., Arenas, A.: Hierarchical multiresolution method to overcome the resolution limit in complex networks. Int. J. Bifurcat. Chaos 22(07), 1250171 (2012)","journal-title":"Int. J. Bifurcat. Chaos"},{"issue":"4","key":"25_CR23","doi-asserted-by":"publisher","first-page":"439","DOI":"10.1090\/S0273-0979-06-01126-8","volume":"43","author":"S Hoory","year":"2006","unstructured":"Hoory, S., Linial, N., Wigderson, A.: Expander graphs and their applications. Bull. Am. Math. Soc. 43(4), 439\u2013561 (2006)","journal-title":"Bull. Am. Math. Soc."},{"key":"25_CR24","first-page":"1368","volume":"3","author":"P Kilby","year":"2005","unstructured":"Kilby, P., Slaney, J., Thiebaux, S., Walsh, T.: Backbones and backdoors in satisfiability. Proc. Natl. Conf. Artif. Intell. 3, 1368\u20131373 (2005)","journal-title":"Proc. Natl. Conf. Artif. Intell."},{"key":"25_CR25","doi-asserted-by":"publisher","unstructured":"Lauria, M., Elffers, J., Nordstr\u00f6m, J., Vinyals, M.: CNFgen: a generator of crafted benchmarks. In: Proceedings of the 20th International Conference on Theory and Applications of Satisfiability Testing (SAT 2017), pp. 464\u2013473 (2017). https:\/\/doi.org\/10.1007\/978-3-319-94144-8_18","DOI":"10.1007\/978-3-319-94144-8_18"},{"key":"25_CR26","unstructured":"Li, C., et al.: On the hierarchical community structure of practical sat formulas. arXiv preprint arXiv:2103.14992 (2021)"},{"key":"25_CR27","doi-asserted-by":"publisher","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, pp. 123\u2013140 (2016). https:\/\/doi.org\/10.1007\/978-3-319-40970-2_9","DOI":"10.1007\/978-3-319-40970-2_9"},{"key":"25_CR28","unstructured":"Mateescu, R.: Treewidth in industrial SAT benchmarks. Tech. Rep. MSR-TR-2011-22, Microsoft (2011). https:\/\/www.microsoft.com\/en-us\/research\/publication\/treewidth-in-industrial-sat-benchmarks\/"},{"issue":"6740","key":"25_CR29","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1038\/22055","volume":"400","author":"R Monasson","year":"1999","unstructured":"Monasson, R., Zecchina, R., Kirkpatrick, S., Selman, B., Troyansky, L.: Determining computational complexity from characteristic \u2018phase transitions\u2019. Nature 400(6740), 133\u2013137 (1999)","journal-title":"Nature"},{"key":"25_CR30","doi-asserted-by":"publisher","unstructured":"Mull, N., Fremont, D.J., Seshia, S.A.: On the hardness of SAT with community structure. In: Proceedings of the 19th International Conference on Theory and Applications of Satisfiability Testing (SAT), pp. 141\u2013159 (2016). https:\/\/doi.org\/10.1007\/978-3-319-40970-2_10","DOI":"10.1007\/978-3-319-40970-2_10"},{"key":"25_CR31","doi-asserted-by":"publisher","unstructured":"Newman, M.E.J., Girvan, M.: Finding and evaluating community structure in networks. Phys. Rev. E 69(2), 026113 (2004). https:\/\/doi.org\/10.1103\/physreve.69.026113","DOI":"10.1103\/physreve.69.026113"},{"key":"25_CR32","doi-asserted-by":"publisher","unstructured":"Newsham, Z., Ganesh, V., Fischmeister, S., Audemard, G., Simon, L.: Impact of community structure on SAT solver performance. In: Theory and Applications of Satisfiability Testing - SAT 2014\u201317th International Conference, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, 14\u201317 July, 2014. Proceedings, pp. 252\u2013268 (2014). https:\/\/doi.org\/10.1007\/978-3-319-09284-3_20","DOI":"10.1007\/978-3-319-09284-3_20"},{"key":"25_CR33","first-page":"2825","volume":"12","author":"F Pedregosa","year":"2011","unstructured":"Pedregosa, F., et al.: Scikit-learn: machine learning in python. J. Mach. Learn. Res. 12, 2825\u20132830 (2011)","journal-title":"J. Mach. Learn. Res."},{"key":"25_CR34","doi-asserted-by":"crossref","unstructured":"Platt, J.C.: Probabilistic outputs for support vector machines and comparisons to regularized likelihood methods. In: Advances in Large Margin Classifiers, pp. 61\u201374. MIT Press (1999)","DOI":"10.7551\/mitpress\/1113.003.0008"},{"key":"25_CR35","doi-asserted-by":"crossref","unstructured":"Ravasz, E., Somera, A.L., Mongru, D.A., Oltvai, Z.N., Barab\u00e1si, A.L.: Hierarchical organization of modularity in metabolic networks. Science 297(5586), 1551\u20131555 (2002)","DOI":"10.1126\/science.1073374"},{"key":"25_CR36","unstructured":"Samer, M., Szeider, S.: Backdoor trees. In: Automated Reasoning, vol. 1, pp. 363\u2013368. Springer (2008)"},{"key":"25_CR37","doi-asserted-by":"crossref","unstructured":"Samer, M., Szeider, S.: Fixed-parameter tractability. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, 2nd edn., vol. 336. IOS Press (2021)","DOI":"10.3233\/FAIA201000"},{"key":"25_CR38","unstructured":"SAT: The International SAT Competition. http:\/\/www.satcompetition.org. Accessed 06 Mar 2021"},{"issue":"1\u20132","key":"25_CR39","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1016\/0004-3702(95)00045-3","volume":"81","author":"B Selman","year":"1996","unstructured":"Selman, B., Mitchell, D.G., Levesque, H.J.: Generating hard satisfiability problems. Artif. Intell. 81(1\u20132), 17\u201329 (1996)","journal-title":"Artif. Intell."},{"key":"25_CR40","unstructured":"SHARCNET: SHARCNET: Graham Cluster. https:\/\/www.sharcnet.ca\/my\/systems\/show\/114. Accessed 06 Mar 2021"},{"key":"25_CR41","unstructured":"Simon, H.A.: The architecture of complexity. Proc. Am. Philos. Soc. 106(6), 467\u2013482 (1962). http:\/\/www.jstor.org\/stable\/985254"},{"key":"25_CR42","unstructured":"Steel, R.G.D., Torrie, J.H.: Principles and Procedures of Statistics. McGraw-Hill (1960)"},{"key":"25_CR43","unstructured":"Szeider, S.: Algorithmic utilization of structure in SAT instances. Theoretical Foundations of SAT\/SMT Solving Workshop at the Simons Institute for the Theory of Computing (2021)"},{"key":"25_CR44","unstructured":"Williams, R., Gomes, C.P., Selman, B.: Backdoors to typical case complexity. In: IJCAI-2003, Proceedings of the Eighteenth International Joint Conference on Artificial Intelligence, pp. 1173\u20131178 (2003). http:\/\/ijcai.org\/Proceedings\/03\/Papers\/168.pdf"},{"key":"25_CR45","doi-asserted-by":"publisher","unstructured":"Xie, Y., Aiken, A.: Saturn: a SAT-based tool for bug detection. In: Proceedings of the 17th International Conference on Computer Aided Verification, CAV 2005, pp. 139\u2013143 (2005). https:\/\/doi.org\/10.1007\/11513988_13","DOI":"10.1007\/11513988_13"},{"key":"25_CR46","unstructured":"Xu, L., Hutter, F., Hoos, H., Leyton-Brown, K.: Features for SAT (2012). http:\/\/www.cs.ubc.ca\/labs\/beta\/Projects\/SATzilla\/. Accessed Feb 2021"},{"key":"25_CR47","doi-asserted-by":"publisher","unstructured":"Zulkoski, E., Martins, R., Wintersteiger, C.M., Liang, J.H., Czarnecki, K., Ganesh, V.: The effect of structural measures and merges on SAT solver performance. In: Proceedings of the 24th International Conference on Principles and Practice of Constraint Programming, pp. 436\u2013452 (2018). https:\/\/doi.org\/10.1007\/978-3-319-98334-9_29","DOI":"10.1007\/978-3-319-98334-9_29"},{"key":"25_CR48","doi-asserted-by":"publisher","unstructured":"Zulkoski, E., et al.: Learning-sensitive backdoors with restarts. In: Proceedings of the 24th International Conference on Principles and Practice of Constraint Programming, pp. 453\u2013469 (2018). https:\/\/doi.org\/10.1007\/978-3-319-98334-9_30","DOI":"10.1007\/978-3-319-98334-9_30"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing \u2013 SAT 2021"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-80223-3_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,3]],"date-time":"2024-09-03T03:16:06Z","timestamp":1725333366000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-80223-3_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030802226","9783030802233"],"references-count":48,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-80223-3_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"2 July 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SAT","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Theory and Applications of Satisfiability Testing","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Barcelona","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Spain","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"5 July 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 July 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"sat2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.iiia.csic.es\/sat2021\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}