{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,27]],"date-time":"2026-09-27T11:39:23Z","timestamp":1790509163782,"version":"4.1.0"},"reference-count":111,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2022,3,30]],"date-time":"2022-03-30T00:00:00Z","timestamp":1648598400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Comput. Surv."],"published-print":{"date-parts":[[2023,3,31]]},"abstract":"<jats:p>The Boolean<jats:bold>satisfiability problem (SAT)<\/jats:bold>is a fundamental NP-complete decision problem in automated reasoning and mathematical logic. As evidenced by the results of SAT competitions, the performance of SAT solvers varies substantially between different SAT categories (random, crafted, and industrial). A suggested explanation is that SAT solvers may exploit the underlying structure inherent to SAT instances. There have been attempts to define the structure of SAT in terms of structural measures such as phase transition, backbones, backdoors, small-world, scale-free, treewidth, centrality, community, self-similarity, and entropy. Still, the empirical evidence of structural measures for SAT has been provided for only some SAT categories. Furthermore, the evidence has not been theoretically proven. Also, the impact of structural measures on the behavior of SAT solvers has not been extensively examined. This work provides a comprehensive study on structural measures for SAT that have been presented in the literature. We provide an overview of the works on structural measures for SAT and their relatedness to the performance of SAT solvers. Accordingly, a taxonomy of structural measures for SAT is presented. We also review in detail important applications of structural measures for SAT, focusing mainly on enhancing SAT solvers, generating SAT instances, and classifying SAT instances.<\/jats:p>","DOI":"10.1145\/3491210","type":"journal-article","created":{"date-parts":[[2022,3,30]],"date-time":"2022-03-30T09:24:35Z","timestamp":1648632275000},"page":"1-34","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":28,"title":["On the Structure of the Boolean Satisfiability Problem: A Survey"],"prefix":"10.1145","volume":"55","author":[{"given":"Tasniem Nasser","family":"Alyahya","sequence":"first","affiliation":[{"name":"Dept. of Computer Science, Coll. of Computer and Information Sciences, King Saud University, Riyadh, Saudi Arabia"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Mohamed El Bachir","family":"Menai","sequence":"additional","affiliation":[{"name":"Dept. of Computer Science, Coll. of Computer and Information Sciences, King Saud University, Riyadh, Saudi Arabia"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Hassan","family":"Mathkour","sequence":"additional","affiliation":[{"name":"Dept. of Computer Science, Coll. of Computer and Information Sciences, King Saud University, Riyadh, Saudi Arabia"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2022,3,30]]},"reference":[{"key":"e_1_3_3_2_2","doi-asserted-by":"crossref","unstructured":"http:\/\/www.satcompetition.org 2002 SAT Competitions","DOI":"10.1145\/504689.504690"},{"key":"e_1_3_3_3_2","unstructured":"https:\/\/satsolvercomplexity.github.io\/hcs\/data 2021 SATsolvercomplexity group"},{"key":"e_1_3_3_4_2","doi-asserted-by":"publisher","DOI":"10.1145\/335305.335309"},{"key":"e_1_3_3_5_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.orl.2005.07.009"},{"key":"e_1_3_3_6_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF00153759"},{"key":"e_1_3_3_7_2","doi-asserted-by":"publisher","DOI":"10.1038\/43601"},{"key":"e_1_3_3_8_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jal.2016.11.004"},{"key":"e_1_3_3_9_2","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1007\/978-3-319-08587-6_8","volume-title":"Automated Reasoning","author":"Ans\u00f3tegui Carlos","year":"2014","unstructured":"Carlos Ans\u00f3tegui, Maria Luisa Bonet, Jes\u00fas Gir\u00e1ldez-Cru, and Jordi Levy. 2014. The fractal dimension of SAT formulas. In Automated Reasoning, St\u00e9phane Demri, Deepak Kapur, and Christoph Weidenbach (Eds.). Springer International Publishing, Cham, 107\u2013121."},{"key":"e_1_3_3_10_2","doi-asserted-by":"publisher","DOI":"10.3233\/978-1-61499-578-4-163"},{"key":"e_1_3_3_11_2","doi-asserted-by":"publisher","DOI":"10.1613\/jair.1.11741"},{"key":"e_1_3_3_12_2","first-page":"109","volume-title":"Proceedings of the 11th International Conference of the Catalan Association for Artificial Intelligence (Frontiers in Artificial Intelligence and Applications)","volume":"184","author":"Ans\u00f3tegui Carlos","year":"2008","unstructured":"Carlos Ans\u00f3tegui, Maria Luisa Bonet, and Jordi Levy. 2008. Random SAT instances \u00e0 la carte. In Proceedings of the 11th International Conference of the Catalan Association for Artificial Intelligence (Frontiers in Artificial Intelligence and Applications), Vol. 184. IOS Press, 109\u2013117."},{"key":"e_1_3_3_13_2","first-page":"127","volume-title":"Principles and Practice of Constraint Programming - CP 200","author":"Ans\u00f3tegui Carlos","year":"2009","unstructured":"Carlos Ans\u00f3tegui, Mar\u00eda Luisa Bonet, and Jordi Levy. 2009. On the structure of industrial SAT instances. In Principles and Practice of Constraint Programming - CP 200, Ian P. Gent (Ed.). Springer Berlin, Berlin, 127\u2013141."},{"key":"e_1_3_3_14_2","first-page":"387","volume-title":"IJCAI 2009, Proceedings of the 21st International Joint Conference on Artificial Intelligence, Pasadena, California, USA, July 11-17, 2009","author":"Ans\u00f3tegui Carlos","year":"2009","unstructured":"Carlos Ans\u00f3tegui, Maria Luisa Bonet, and Jordi Levy. 2009. Towards industrial-like random SAT instances. In IJCAI 2009, Proceedings of the 21st International Joint Conference on Artificial Intelligence, Pasadena, California, USA, July 11-17, 2009. 387\u2013392. http:\/\/ijcai.org\/Proceedings\/09\/Papers\/072.pdf"},{"key":"e_1_3_3_15_2","doi-asserted-by":"publisher","DOI":"10.5555\/1619995.1620032"},{"key":"e_1_3_3_16_2","doi-asserted-by":"crossref","first-page":"410","DOI":"10.1007\/978-3-642-31612-8_31","volume-title":"Theory and Applications of Satisfiability Testing\u2013SAT 2012","author":"Ans\u00f3tegui Carlos","year":"2012","unstructured":"Carlos Ans\u00f3tegui, Jes\u00fas Gir\u00e1ldez-Cru, and Jordi Levy. 2012. The community structure of SAT formulas. In Theory and Applications of Satisfiability Testing\u2013SAT 2012, Alessandro Cimatti and Roberto Sebastiani (Eds.). Springer Berlin, Berlin, 410\u2013423."},{"key":"e_1_3_3_17_2","first-page":"00","volume-title":"Theory and Applications of Satisfiability Testing\u2013SAT 2012","author":"Audemard Gilles","year":"2012","unstructured":"Gilles Audemard, Beno\u00eet Hoessen, Sa\u00efd Jabbour, Jean-Marie Lagniez, and C\u00e9dric Piette. 2012. Revisiting clause exchange in parallel SAT solving. In Theory and Applications of Satisfiability Testing\u2013SAT 2012, Alessandro Cimatti and Roberto Sebastiani (Eds.). Springer Berlin, Berlin, 00\u2013213."},{"key":"e_1_3_3_18_2","doi-asserted-by":"publisher","DOI":"10.5555\/1661445.1661509"},{"key":"e_1_3_3_19_2","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0095115"},{"key":"e_1_3_3_20_2","first-page":"75","article-title":"PicoSAT essentials","volume":"4","author":"Biere Armin","year":"2008","unstructured":"Armin Biere. 2008. PicoSAT essentials. JSAT 4 (2008), 75\u201397.","journal-title":"JSAT"},{"key":"e_1_3_3_21_2","unstructured":"Armin Biere. 2009. Pre icoSAT@SC\u201909. (2009)."},{"issue":"1","key":"e_1_3_3_22_2","first-page":"201","article-title":"Decomposing SAT problems into connected components","volume":"2","author":"Biere Armin","year":"2006","unstructured":"Armin Biere and Carsten Sinz. 2006. Decomposing SAT problems into connected components. JSAT 2, 1\u20134 (2006), 201\u2013208.","journal-title":"JSAT"},{"key":"e_1_3_3_23_2","doi-asserted-by":"publisher","DOI":"10.1088\/1742-5468\/2008\/10\/p10008"},{"key":"e_1_3_3_24_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF02127976"},{"key":"e_1_3_3_25_2","doi-asserted-by":"publisher","DOI":"10.1023\/A:1010933404324"},{"key":"e_1_3_3_26_2","doi-asserted-by":"publisher","DOI":"10.5555\/1631171.1631221"},{"key":"e_1_3_3_27_2","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1992.267789"},{"key":"e_1_3_3_28_2","doi-asserted-by":"publisher","DOI":"10.1016\/B978-1-55860-377-6.50022-0"},{"key":"e_1_3_3_29_2","doi-asserted-by":"publisher","DOI":"10.1016\/B978-1-55860-377-6.50023-2"},{"key":"e_1_3_3_30_2","doi-asserted-by":"publisher","DOI":"10.5555\/3000001.3000069"},{"key":"e_1_3_3_31_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-01929-6_6"},{"key":"e_1_3_3_32_2","first-page":"73","volume-title":"SAT (Lecture Notes in Computer Science)","author":"Dilkina Bistra N.","year":"2009","unstructured":"Bistra N. Dilkina, Carla P. Gomes, and Ashish Sabharwal. 2009. Backdoors in the context of learning. In SAT (Lecture Notes in Computer Science), Vol. 5584. Springer, 73\u201379."},{"key":"e_1_3_3_33_2","doi-asserted-by":"publisher","DOI":"10.1006\/jagm.1997.0867"},{"key":"e_1_3_3_34_2","doi-asserted-by":"publisher","DOI":"10.5555\/338219.338243"},{"key":"e_1_3_3_35_2","doi-asserted-by":"publisher","DOI":"10.5555\/1642090.1642124"},{"key":"e_1_3_3_36_2","first-page":"502","volume-title":"SAT (Lecture Notes in Computer Science)","author":"E\u00e9n Niklas","year":"2003","unstructured":"Niklas E\u00e9n and Niklas S\u00f6rensson. 2003. An extensible SAT-solver. In SAT (Lecture Notes in Computer Science), Enrico Giunchiglia and Armando Tacchella (Eds.), Vol. 2919. Springer, 502\u2013518."},{"key":"e_1_3_3_37_2","article-title":"The 3rd international planning competition: Results and analysis","volume":"1106","author":"Fox Maria","year":"2011","unstructured":"Maria Fox and Derek Long. 2011. The 3rd international planning competition: Results and analysis. CoRR abs\/1106.5998 (2011).","journal-title":"CoRR"},{"key":"e_1_3_3_38_2","doi-asserted-by":"publisher","DOI":"10.1023\/A:1007421302149"},{"key":"e_1_3_3_39_2","doi-asserted-by":"publisher","DOI":"10.2307\/3033543"},{"key":"e_1_3_3_40_2","doi-asserted-by":"publisher","DOI":"10.1016\/0378-8733(78)90021-7"},{"key":"e_1_3_3_41_2","doi-asserted-by":"publisher","DOI":"10.1006\/jagm.1996.0016"},{"key":"e_1_3_3_42_2","doi-asserted-by":"crossref","first-page":"223","DOI":"10.1007\/978-3-319-24318-4_17","volume-title":"Theory and Applications of Satisfiability Testing\u2013SAT 2015","author":"Ganian Robert","year":"2015","unstructured":"Robert Ganian and Stefan Szeider. 2015. Community structure inspired algorithms for SAT and #SAT. In Theory and Applications of Satisfiability Testing\u2013SAT 2015, Marijn Heule and Sean Weaver (Eds.). Springer International Publishing, 223\u2013237."},{"key":"e_1_3_3_43_2","volume-title":"The SAT Phase Transition","author":"Gent Ian Philip","year":"1994","unstructured":"Ian Philip Gent and Toby Walsh. 1994. The SAT Phase Transition. Department of Artificial Intelligence, University of Edinburgh."},{"key":"e_1_3_3_44_2","doi-asserted-by":"publisher","DOI":"10.5555\/2832415.2832520"},{"key":"e_1_3_3_45_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.artint.2016.06.001"},{"key":"e_1_3_3_46_2","doi-asserted-by":"publisher","DOI":"10.24963\/ijcai.2017\/89"},{"key":"e_1_3_3_47_2","volume-title":"SPAA 1996","author":"Goerdt A.","year":"1996","unstructured":"A. Goerdt. 1996. A threshold for unsatisfiability. In SPAA 1996."},{"key":"e_1_3_3_48_2","doi-asserted-by":"publisher","DOI":"10.1023\/A:1006314320276"},{"key":"e_1_3_3_49_2","first-page":"431","volume-title":"Proceedings of the Fifteenth National Conference on Artificial Intelligence and Tenth Innovative Applications of Artificial Intelligence Conference, AAAI 98, IAAI 98, July 26\u201330, 1998, Madison, Wisconsin, USA.","author":"Gomes Carla P.","year":"1998","unstructured":"Carla P. Gomes, Bart Selman, and Henry A. Kautz. 1998. Boosting combinatorial search through randomization. In Proceedings of the Fifteenth National Conference on Artificial Intelligence and Tenth Innovative Applications of Artificial Intelligence Conference, AAAI 98, IAAI 98, July 26\u201330, 1998, Madison, Wisconsin, USA.431\u2013437. http:\/\/www.aaai.org\/Library\/AAAI\/1998\/aaai98-061.php."},{"key":"e_1_3_3_50_2","doi-asserted-by":"crossref","first-page":"618","DOI":"10.1007\/978-3-540-85958-1_53","volume-title":"Principles and Practice of Constraint Programming","author":"Gregory Peter","year":"2008","unstructured":"Peter Gregory, Maria Fox, and Derek Long. 2008. A new empirical study of weak backdoors. In Principles and Practice of Constraint Programming, Peter J. Stuckey (Ed.). Springer Berlin, Berlin, 618\u2013623."},{"key":"e_1_3_3_51_2","first-page":"252","volume-title":"Principles and Practice of Constraint Programming\u2013CP 2010","author":"Guo Long","year":"2010","unstructured":"Long Guo, Youssef Hamadi, Said Jabbour, and Lakhdar Sais. 2010. Diversification and intensification in parallel SAT solving. In Principles and Practice of Constraint Programming\u2013CP 2010, David Cohen (Ed.). Springer Berlin, Berlin, 252\u2013265."},{"key":"e_1_3_3_52_2","doi-asserted-by":"publisher","DOI":"10.1145\/3310986.3310989"},{"key":"e_1_3_3_53_2","doi-asserted-by":"crossref","first-page":"247","DOI":"10.1007\/978-3-030-10801-4_20","volume-title":"SOFSEM 2019: Theory and Practice of Computer Science","author":"Hemaspaandra Lane A.","year":"2019","unstructured":"Lane A. Hemaspaandra and David E. Narv\u00e1ez. 2019. Existence versus exploitation: The opacity of backdoors and backbones under a weak assumption. In SOFSEM 2019: Theory and Practice of Computer Science, Barbara Catania, Rastislav Kr\u00e1lovi\u010d, Jerzy Nawrocki, and Giovanni Pighizzini (Eds.). Springer International Publishing, Cham, 247\u2013259."},{"issue":"2","key":"e_1_3_3_54_2","first-page":"117","article-title":"Whose side are you on? Finding solutions in a biased search-tree","volume":"4","author":"Heule Marijn","year":"2008","unstructured":"Marijn Heule and Hans van Maaren. 2008. Whose side are you on? Finding solutions in a biased search-tree. JSAT 4, 2\u20134 (2008), 117\u2013148.","journal-title":"JSAT"},{"key":"e_1_3_3_55_2","doi-asserted-by":"publisher","DOI":"10.1016\/0004-3702(95)00050-x"},{"key":"e_1_3_3_56_2","first-page":"283","volume-title":"SAT2000","author":"Hoos H.","year":"2000","unstructured":"H. Hoos and T. Stutzle. 2000. SATLIB: An online resource for research on SAT. In SAT2000, H. van Maaren I. P. Gent and T. Walsh (Eds.). IOS Press, 283\u2013292."},{"key":"e_1_3_3_57_2","first-page":"283","volume-title":"SAT","author":"Hoos Holger H.","year":"2000","unstructured":"Holger H. Hoos and Thomas St\u00fctzle. 2000. SATLIB: An online resource for research on SAT. In SAT. 283\u2013292. http:\/\/www.satlib.org"},{"key":"e_1_3_3_58_2","doi-asserted-by":"publisher","DOI":"10.1145\/337180.337616"},{"key":"e_1_3_3_59_2","doi-asserted-by":"publisher","DOI":"10.29007\/3pxg"},{"key":"e_1_3_3_60_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-94144-8_8"},{"key":"e_1_3_3_61_2","doi-asserted-by":"publisher","DOI":"10.5555\/2074158.2074196"},{"key":"e_1_3_3_62_2","doi-asserted-by":"publisher","DOI":"10.5555\/1860967.1861114"},{"key":"e_1_3_3_63_2","doi-asserted-by":"publisher","DOI":"10.5555\/2891460.2891696"},{"key":"e_1_3_3_64_2","first-page":"348","volume-title":"CP (Lecture Notes in Computer Science)","author":"Katsirelos George","year":"2012","unstructured":"George Katsirelos and Laurent Simon. 2012. Eigenvector centrality in industrial SAT instances. In CP (Lecture Notes in Computer Science), Vol. 7514. Springer, 348\u2013356."},{"key":"e_1_3_3_65_2","doi-asserted-by":"publisher","DOI":"10.5555\/1624218.1624265"},{"key":"e_1_3_3_66_2","doi-asserted-by":"publisher","DOI":"10.5555\/1619499.1619553"},{"key":"e_1_3_3_67_2","doi-asserted-by":"publisher","DOI":"10.2307\/2347628"},{"key":"e_1_3_3_68_2","first-page":"359","volume-title":"Theory and Applications of Satisfiability Testing\u2013SAT 2021","author":"Li Chunxiao","year":"2021","unstructured":"Chunxiao Li, Jonathan Chung, Soham Mukherjee, Marc Vinyals, Noah Fleming, Antonina Kolokolova, Alice Mu, and Vijay Ganesh. 2021. On the hierarchical community structure of practical Boolean formulas. In Theory and Applications of Satisfiability Testing\u2013SAT 2021, Chu-Min Li and Felip Many\u00e0 (Eds.). Springer International Publishing, Cham, 359\u2013376."},{"key":"e_1_3_3_69_2","first-page":"366","volume-title":"Proceedings of the 15th International Joint Conference on Artificial Intelligence - Volume 1 (IJCAI\u201997)","author":"Li Chu Min","year":"1997","unstructured":"Chu Min Li and Anbulagan Anbulagan. 1997. Heuristics based on unit propagation for satisfiability problems. In Proceedings of the 15th International Joint Conference on Artificial Intelligence - Volume 1 (IJCAI\u201997). Morgan Kaufmann Publishers Inc., San Francisco, CA, USA, 366\u2013371. http:\/\/dl.acm.org\/citation.cfm?id=1624162.1624216."},{"key":"e_1_3_3_70_2","first-page":"269","volume-title":"Advances in Artificial Intelligence","author":"Li Zijie","year":"2011","unstructured":"Zijie Li and Peter van Beek. 2011. Finding small backdoors in SAT instances. In Advances in Artificial Intelligence, Cory Butz and Pawan Lingras (Eds.). Springer Berlin, Berlin, 269\u2013280."},{"key":"e_1_3_3_71_2","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1007\/978-3-319-40970-2_9","volume-title":"Theory and Applications of Satisfiability Testing\u2013SAT 2016","author":"Liang Jia Hui","year":"2016","unstructured":"Jia Hui Liang, Vijay Ganesh, Pascal Poupart, and Krzysztof Czarnecki. 2016. Learning rate based branching heuristic for SAT solvers. In Theory and Applications of Satisfiability Testing\u2013SAT 2016, Nadia Creignou and Daniel Le Berre (Eds.). Springer International Publishing, Cham, 123\u2013140."},{"key":"e_1_3_3_72_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-26287-1_14"},{"key":"e_1_3_3_73_2","first-page":"52","volume-title":"SAT Competition 2016: Solver and Benchmark Descriptions","author":"Liang Jia Hui","year":"2016","unstructured":"Jia Hui Liang, Chanseok Oh, Vijay Ganesh, and Krzysztof Czarnecki. 2016. MapleCOMSPS, MapleCOMSPS LRB, MapleCOMSPS CHB. In SAT Competition 2016: Solver and Benchmark Descriptions, Vol. B-2016-1. 52\u201353."},{"issue":"2","key":"e_1_3_3_74_2","first-page":"13","article-title":"The AIPS-98 planning competition","volume":"21","author":"Long Derek","year":"2000","unstructured":"Derek Long, Henry A. Kautz, Bart Selman, Blai Bonet, Hector Geffner, Jana Koehler, Michael Brenner, J\u00f6rg Hoffmann, Frank Rittinger, Corin R. Anderson, Daniel S. Weld, David E. Smith, and Maria Fox. 2000. The AIPS-98 planning competition. AI Magazine 21, 2 (2000), 13\u201333.","journal-title":"AI Magazine"},{"key":"e_1_3_3_75_2","doi-asserted-by":"publisher","DOI":"10.5555\/1597538.1597556"},{"key":"e_1_3_3_76_2","first-page":"15","volume-title":"ECAI 2010-19th European Conference on Artificial Intelligence, Lisbon, Portugal, August 16-20, 2010, Proceedings (Frontiers in Artificial Intelligence and Applications)","volume":"215","author":"Marques-Silva Jo\u00e3o","year":"2010","unstructured":"Jo\u00e3o Marques-Silva, Mikol\u00e1s Janota, and In\u00eas Lynce. 2010. On computing backbones of propositional theories. In ECAI 2010-19th European Conference on Artificial Intelligence, Lisbon, Portugal, August 16-20, 2010, Proceedings (Frontiers in Artificial Intelligence and Applications), Helder Coelho, Rudi Studer, and Michael J. Wooldridge (Eds.), Vol. 215. IOS Press, 15\u201320. http:\/\/www.booksonline.iospress.nl\/Content\/View.aspx?piid=17706."},{"key":"e_1_3_3_77_2","doi-asserted-by":"publisher","DOI":"10.1109\/12.769433"},{"key":"e_1_3_3_78_2","unstructured":"Robert Mateescu. 2011. Treewidth in Industrial SAT Benchmarks. (February 2011)."},{"key":"e_1_3_3_79_2","doi-asserted-by":"publisher","DOI":"10.5555\/1867135.1867206"},{"key":"e_1_3_3_80_2","doi-asserted-by":"publisher","DOI":"10.1038\/22055"},{"key":"e_1_3_3_81_2","doi-asserted-by":"publisher","DOI":"10.1145\/378239.379017"},{"key":"e_1_3_3_82_2","doi-asserted-by":"crossref","first-page":"141","DOI":"10.1007\/978-3-319-40970-2_10","volume-title":"Theory and Applications of Satisfiability Testing\u2013SAT 2016","author":"Mull Nathan","year":"2016","unstructured":"Nathan Mull, Daniel J. Fremont, and Sanjit A. Seshia. 2016. On the hardness of SAT with community structure. In Theory and Applications of Satisfiability Testing\u2013SAT 2016, Nadia Creignou and Daniel Le Berre (Eds.). Springer International Publishing, Cham, 141\u2013159."},{"key":"e_1_3_3_83_2","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevE.69.026113"},{"key":"e_1_3_3_84_2","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevE.69.066133"},{"key":"e_1_3_3_85_2","doi-asserted-by":"crossref","first-page":"252","DOI":"10.1007\/978-3-319-09284-3_20","volume-title":"Theory and Applications of Satisfiability Testing\u2013SAT 2014","author":"Newsham Zack","year":"2014","unstructured":"Zack Newsham, Vijay Ganesh, Sebastian Fischmeister, Gilles Audemard, and Laurent Simon. 2014. Impact of community structure on SAT solver performance. In Theory and Applications of Satisfiability Testing\u2013SAT 2014, Carsten Sinz and Uwe Egly (Eds.). Springer International Publishing, Cham, 252\u2013268."},{"key":"e_1_3_3_86_2","first-page":"62","volume-title":"Theory and Applications of Satisfiability Testing\u2013SAT 2015","author":"Czarnecki Zach Newsham, William Lindsay, Vijay Ganesh, Jia Hui Liang, Sebastian Fischmeister, and Krzysztof","year":"2015","unstructured":"Zach Newsham, William Lindsay, Vijay Ganesh, Jia Hui Liang, Sebastian Fischmeister, and Krzysztof Czarnecki. 2015. SATGraf: Visualizing the evolution of SAT formula structure in solvers. In Theory and Applications of Satisfiability Testing\u2013SAT 2015, Heule, Marijn and Weaver, Sean (Ed.). Springer International Publishing, Cham, 62\u201370."},{"key":"e_1_3_3_87_2","first-page":"340","volume-title":"In Proc. of the 14th Nat. Conf. on AI","author":"Parkes Andrew J.","year":"1997","unstructured":"Andrew J. Parkes. 1997. Clustering at the phase transition. In In Proc. of the 14th Nat. Conf. on AI. AAAI Press \/ The MIT Press, 340\u2013345."},{"key":"e_1_3_3_88_2","doi-asserted-by":"crossref","first-page":"294","DOI":"10.1007\/978-3-540-72788-0_28","volume-title":"Theory and Applications of Satisfiability Testing\u2013SAT 2007","author":"Pipatsrisawat Knot","year":"2007","unstructured":"Knot Pipatsrisawat and Adnan Darwiche. 2007. A lightweight component caching scheme for satisfiability solvers. In Theory and Applications of Satisfiability Testing\u2013SAT 2007, Jo\u00e3o Marques-Silva and Karem A. Sakallah (Eds.). Springer Berlin, Berlin, 294\u2013299."},{"key":"e_1_3_3_89_2","volume-title":"Advances in Kernel Methods - Support Vector Learning","author":"Platt J.","year":"1998","unstructured":"J. Platt. 1998. Fast training of support vector machines using sequential minimal optimization. In Advances in Kernel Methods - Support Vector Learning, B. Schoelkopf, C. Burges, and A. Smola (Eds.). MIT Press. http:\/\/research.microsoft.com\/~jplatt\/smo.html"},{"key":"e_1_3_3_90_2","doi-asserted-by":"publisher","DOI":"10.1145\/3167132.3167230"},{"key":"e_1_3_3_91_2","doi-asserted-by":"publisher","DOI":"10.5555\/152181"},{"key":"e_1_3_3_92_2","doi-asserted-by":"publisher","DOI":"10.1016\/0095-8956(83)90079-5"},{"key":"e_1_3_3_93_2","first-page":"50","volume-title":"Proceedings of the 15th International Joint Conference on Artificial Intelligence - Volume 1 (IJCAI\u201997)","author":"Selman Bart","year":"1997","unstructured":"Bart Selman, Henry Kautz, and David McAllester. 1997. Ten challenges in propositional reasoning and search. In Proceedings of the 15th International Joint Conference on Artificial Intelligence - Volume 1 (IJCAI\u201997). Morgan Kaufmann Publishers Inc., San Francisco, CA, USA, 50\u201354. http:\/\/dl.acm.org\/citation.cfm?id=1624162.1624170"},{"key":"e_1_3_3_94_2","first-page":"220","volume-title":"Proceedings of the 1996 IEEE\/ACM International Conference on Computer-aided Design (ICCAD\u201996)","author":"Silva Jo\u00e3o P. Marques","year":"1996","unstructured":"Jo\u00e3o P. Marques Silva and Karem A. Sakallah. 1996. GRASP\u2013a new search algorithm for satisfiability. In Proceedings of the 1996 IEEE\/ACM International Conference on Computer-aided Design (ICCAD\u201996). IEEE Computer Society, Washington, DC, USA, 220\u2013227. http:\/\/dl.acm.org\/citation.cfm?id=244522.244560"},{"key":"e_1_3_3_95_2","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0653(04)00318-X"},{"key":"e_1_3_3_96_2","doi-asserted-by":"crossref","first-page":"591","DOI":"10.1007\/3-540-36187-1_52","volume-title":"AI 2002: Advances in Artificial Intelligence","author":"Slater Andrew","year":"2002","unstructured":"Andrew Slater. 2002. Modelling more realistic SAT problems. In AI 2002: Advances in Artificial Intelligence, Bob McKay and John Slaney (Eds.). Springer Berlin, Berlin, 591\u2013602."},{"key":"e_1_3_3_97_2","doi-asserted-by":"publisher","DOI":"10.1038\/nature03248"},{"key":"e_1_3_3_98_2","first-page":"188","volume-title":"SAT (Lecture Notes in Computer Science)","author":"Sonobe Tomohiro","year":"2014","unstructured":"Tomohiro Sonobe, Shuya Kondoh, and Mary Inaba. 2014. Community branching for parallel portfolio SAT solvers. In SAT (Lecture Notes in Computer Science), Vol. 8561. Springer, 188\u2013196."},{"key":"e_1_3_3_99_2","first-page":"244","volume-title":"SAT (Lecture Notes in Computer Science)","author":"Soos Mate","year":"2009","unstructured":"Mate Soos, Karsten Nohl, and Claude Castelluccia. 2009. Extending SAT solvers to cryptographic problems. In SAT (Lecture Notes in Computer Science), Vol. 5584. Springer, 244\u2013257."},{"key":"e_1_3_3_100_2","doi-asserted-by":"publisher","DOI":"10.2307\/1412159"},{"key":"e_1_3_3_101_2","first-page":"25","volume-title":"Proc. of SAT Competition 2014\u2013Solver and Benchmark Descriptions (Department of Computer Science Series of Publications B)","author":"Tomohiro Sonobe","year":"2016","unstructured":"Sonobe Tomohiro. 2016. CBPeneLoPe2016, CCSPeneLoPe2016, gulch entering the SAT competition 2016. In Proc. of SAT Competition 2014\u2013Solver and Benchmark Descriptions (Department of Computer Science Series of Publications B), Tom\u00e1\u0161 Balyo, Marijn Heule, and Matti J\u00e4rvisalo (Eds.), Vol. B-2016-1. University of Helsinki, 25\u201326."},{"key":"e_1_3_3_102_2","first-page":"14","volume-title":"Proc. of SAT Competition 2014\u2013Solver and Benchmark Descriptions (Department of Computer Science Series of Publications B)","author":"Tomohiro Sonobe","year":"2014","unstructured":"Sonobe Tomohiro and Shuya Kondoh. 2014. CBPeneLoPe and ParaCIRMiniSAT entering the SAT competition 2014. In Proc. of SAT Competition 2014\u2013Solver and Benchmark Descriptions (Department of Computer Science Series of Publications B), Tom\u00e1\u0161 Balyo, Marijn Heule, and Matti J\u00e4rvisalo (Eds.), Vol. B-2014-2. University of Helsinki, 14\u201315."},{"key":"e_1_3_3_103_2","unstructured":"Jia Hui Liang and Vijay Ganesh. MapleSAT: Combining Machine Learning and Deduction in SAT solvers. ([n.d.]). https:\/\/sites.google.com\/a\/gsd.uwaterloo.ca\/maplesat\/."},{"key":"e_1_3_3_104_2","doi-asserted-by":"publisher","DOI":"10.5555\/1624312.1624385"},{"key":"e_1_3_3_105_2","doi-asserted-by":"publisher","DOI":"10.1038\/30918"},{"key":"e_1_3_3_106_2","first-page":"4","article-title":"On the connections between backdoors, restarts, and heavy-tailedness in combinatorial search","volume":"23","author":"Williams Ryan","year":"2003","unstructured":"Ryan Williams, Carla Gomes, and Bart Selman. 2003. On the connections between backdoors, restarts, and heavy-tailedness in combinatorial search. Structure 23 (2003), 4.","journal-title":"Structure"},{"key":"e_1_3_3_107_2","doi-asserted-by":"publisher","DOI":"10.5555\/1630659.1630827"},{"issue":"1","key":"e_1_3_3_108_2","first-page":"565","article-title":"SATzilla: Portfolio-based algorithm selection for SAT","volume":"32","author":"Xu Lin","year":"2008","unstructured":"Lin Xu, Frank Hutter, Holger H. Hoos, and Kevin Leyton-Brown. 2008. SATzilla: Portfolio-based algorithm selection for SAT. J. Artif. Int. Res. 32, 1 (June 2008), 565\u2013606. http:\/\/dl.acm.org\/citation.cfm?id=1622673.1622687","journal-title":"J. Artif. Int. Res."},{"key":"e_1_3_3_109_2","doi-asserted-by":"publisher","DOI":"10.3390\/e23030303"},{"key":"e_1_3_3_110_2","first-page":"436","volume-title":"CP (Lecture Notes in Computer Science)","author":"Zulkoski Edward","year":"2018","unstructured":"Edward Zulkoski, Ruben Martins, Christoph M. Wintersteiger, Jia Hui Liang, Krzysztof Czarnecki, and Vijay Ganesh. 2018. The effect of structural measures and merges on SAT solver performance. In CP (Lecture Notes in Computer Science), Vol. 11008. Springer, 436\u2013452."},{"key":"e_1_3_3_111_2","article-title":"Relating complexity-theoretic parameters with SAT solver performance","volume":"1706","author":"Zulkoski Edward","year":"2017","unstructured":"Edward Zulkoski, Ruben Martins, Christoph M. Wintersteiger, Robert Robere, Jia Hui Liang, Krzysztof Czarnecki, and Vijay Ganesh. 2017. Relating complexity-theoretic parameters with SAT solver performance. CoRR abs\/1706.08611 (2017).","journal-title":"CoRR"},{"key":"e_1_3_3_112_2","first-page":"453","volume-title":"CP (Lecture Notes in Computer Science)","author":"Zulkoski Edward","year":"2018","unstructured":"Edward Zulkoski, Ruben Martins, Christoph M. Wintersteiger, Robert Robere, Jia Hui Liang, Krzysztof Czarnecki, and Vijay Ganesh. 2018. Learning-sensitive backdoors with restarts. In CP (Lecture Notes in Computer Science), Vol. 11008. Springer, 453\u2013469."}],"container-title":["ACM Computing Surveys"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3491210","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3491210","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T18:09:18Z","timestamp":1750183758000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3491210"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,3,30]]},"references-count":111,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2023,3,31]]}},"alternative-id":["10.1145\/3491210"],"URL":"https:\/\/doi.org\/10.1145\/3491210","relation":{},"ISSN":["0360-0300","1557-7341"],"issn-type":[{"value":"0360-0300","type":"print"},{"value":"1557-7341","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,3,30]]},"assertion":[{"value":"2021-04-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2021-10-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2022-03-30","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}