{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,27]],"date-time":"2026-09-27T11:39:19Z","timestamp":1790509159024,"version":"4.1.0"},"reference-count":51,"publisher":"MDPI AG","issue":"6","license":[{"start":{"date-parts":[[2022,6,20]],"date-time":"2022-06-20T00:00:00Z","timestamp":1655683200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"MCIN\/AEI\/10.13039\/501100011033","award":["PID2019-109137GB-C21"],"award-info":[{"award-number":["PID2019-109137GB-C21"]}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Algorithms"],"abstract":"<jats:p>We focus on the random generation of SAT instances that have properties similar to real-world instances. It is known that many industrial instances, even with a great number of variables, can be solved by a clever solver in a reasonable amount of time. This is not possible, in general, with classical randomly generated instances. We provide a different generation model of SAT instances, called scale-free random SAT instances. This is based on the use of a non-uniform probability distribution P(i)\u223ci\u2212\u03b2 to select variable i, where \u03b2 is a parameter of the model. This results in formulas where the number of occurrences k of variables follows a power-law distribution P(k)\u223ck\u2212\u03b4, where \u03b4=1+1\/\u03b2. This property has been observed in most real-world SAT instances. For \u03b2=0, our model extends classical random SAT instances. We prove the existence of a SAT\u2013UNSAT phase transition phenomenon for scale-free random 2-SAT instances with \u03b2&lt;1\/2 when the clause\/variable ratio is m\/n=1\u22122\u03b2(1\u2212\u03b2)2. We also prove that scale-free random k-SAT instances are unsatisfiable with a high probability when the number of clauses exceeds \u03c9(n(1\u2212\u03b2)k). The proof of this result suggests that, when \u03b2&gt;1\u22121\/k, the unsatisfiability of most formulas may be due to small cores of clauses. Finally, we show how this model will allow us to generate random instances similar to industrial instances, of interest for testing purposes.<\/jats:p>","DOI":"10.3390\/a15060219","type":"journal-article","created":{"date-parts":[[2022,6,21]],"date-time":"2022-06-21T01:43:27Z","timestamp":1655775807000},"page":"219","update-policy":"https:\/\/doi.org\/10.3390\/mdpi_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Scale-Free Random SAT Instances"],"prefix":"10.3390","volume":"15","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7727-2766","authenticated-orcid":false,"given":"Carlos","family":"Ans\u00f3tegui\u00a0","sequence":"first","affiliation":[{"name":"Departament d\u2019Inform\u00e0tica i Enginyeria Industrial, Universitat de Lleida, 25001 Lleida, Spain"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1646-7177","authenticated-orcid":false,"given":"Maria Luisa","family":"Bonet","sequence":"additional","affiliation":[{"name":"Computer Science Department, Universitat Polit\u00e8cnica de Catalunya, 08034 Barcelona, Spain"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5883-5746","authenticated-orcid":false,"given":"Jordi","family":"Levy","sequence":"additional","affiliation":[{"name":"Instituto de Investigaci\u00f3n en Inteligencia Artificial (IIIA), CSIC, 08193 Bellaterra, Spain"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"1968","published-online":{"date-parts":[[2022,6,20]]},"reference":[{"key":"ref_1","unstructured":"Selman, B., Kautz, H.A., and McAllester, D.A. (1997, January 23\u201329). Ten Challenges in Propositional Reasoning and Search. Proceedings of the 15th International Joint Conference on Artificial Intelligence (IJCAI 1997), Nagoya, Japan."},{"key":"ref_2","unstructured":"Selman, B. (2000, January 26\u201329). Satisfiability Testing: Recent Developments and Challenge Problems. Proceedings of the 15th Annual IEEE Symposium on Logic in Computer Science (LICS 2000), Santa Barbara, CA, USA."},{"key":"ref_3","doi-asserted-by":"crossref","unstructured":"Kautz, H.A., and Selman, B. (October, January 29). Ten Challenges Redux: Recent Progress in Propositional Reasoning and Search. Proceedings of the 9th International Conference on Principles and Practice of Constraint Programming (CP 2003), Kinsale, Ireland.","DOI":"10.1007\/978-3-540-45193-8_1"},{"key":"ref_4","doi-asserted-by":"crossref","first-page":"1514","DOI":"10.1016\/j.dam.2006.10.004","article-title":"The state of SAT","volume":"155","author":"Kautz","year":"2007","journal-title":"Discret. Appl. Math."},{"key":"ref_5","doi-asserted-by":"crossref","first-page":"127","DOI":"10.1007\/978-3-642-04244-7_13","article-title":"On the Structure of Industrial SAT Instances","volume":"Volume 5732","author":"Bonet","year":"2009","journal-title":"Proceedings of the 15th International Conference on Principles and Practice of Constraint Programming, CP 2009"},{"key":"ref_6","doi-asserted-by":"crossref","first-page":"443","DOI":"10.1613\/jair.1.11741","article-title":"Community Structure in Industrial SAT Instances","volume":"66","author":"Bonet","year":"2019","journal-title":"J. Artif. Intell. Res."},{"key":"ref_7","doi-asserted-by":"crossref","unstructured":"Newsham, Z., Ganesh, V., Fischmeister, S., Audemard, G., and Simon, L. (2014, January 14\u201317). Impact of Community Structure on SAT Solver Performance. Proceedings of the 17th International Conference on Theory and Applications of Satisfiability Testing (SAT 2014), Vienna, Austria.","DOI":"10.1007\/978-3-319-09284-3_20"},{"key":"ref_8","doi-asserted-by":"crossref","unstructured":"Sonobe, T., Kondoh, S., and Inaba, M. (2014, January 14\u201317). Community Branching for Parallel Portfolio SAT Solvers. Proceedings of the 17th International Conference on Theory and Applications of Satisfiability Testing (SAT 2014), Vienna, Austria.","DOI":"10.1007\/978-3-319-09284-3_14"},{"key":"ref_9","doi-asserted-by":"crossref","unstructured":"Martins, R., Manquinho, V.M., and Lynce, I. (2013, January 8\u201312). Community-Based Partitioning for MaxSAT Solving. Proceedings of the 16th International Conference on Theory and Applications of Satisfiability Testing (SAT 2013), Helsinki, Finland.","DOI":"10.1007\/978-3-642-39071-5_14"},{"key":"ref_10","doi-asserted-by":"crossref","unstructured":"Katsirelos, G., and Simon, L. (2012, January 8\u201312). Eigenvector Centrality in Industrial SAT Instances. Proceedings of the 18th International Conference on Principles and Practice of Constraint Programming (CP 2012), Quebec, QC, Canada.","DOI":"10.1007\/978-3-642-33558-7_27"},{"key":"ref_11","unstructured":"Ans\u00f3tegui, C., Bonet, M.L., and Levy, J. (2009, January 2\u20135). Towards Industrial-Like Random SAT Instances. Proceedings of the 21st International Joint Conference on Artificial Intelligence, IJCAI 2009, Newark, NJ, USA."},{"key":"ref_12","doi-asserted-by":"crossref","unstructured":"Friedrich, T., Krohmer, A., Rothenberger, R., and Sutton, A.M. (2017, January 4\u20139). Phase Transitions for Scale-Free SAT Formulas. Proceedings of the Thirty-First AAAI Conference on Artificial Intelligence, AAAI 2017, San Francisco, CA, USA.","DOI":"10.1609\/aaai.v31i1.11133"},{"key":"ref_13","first-page":"37:1","article-title":"Bounds on the Satisfiability Threshold for Power Law Distributed Random SAT","volume":"Volume 87","author":"Friedrich","year":"2017","journal-title":"Proceedings of the 25th Annual European Symposium on Algorithms, ESA 2017"},{"key":"ref_14","doi-asserted-by":"crossref","first-page":"1017","DOI":"10.1090\/S0894-0347-99-00305-7","article-title":"Sharp Thresholds of Graph properties, and the k-SAT Problem","volume":"12","author":"Friedgut","year":"1998","journal-title":"J. Am. Math. Soc."},{"key":"ref_15","doi-asserted-by":"crossref","first-page":"273","DOI":"10.1007\/978-3-319-94144-8_17","article-title":"Sharpness of the Satisfiability Threshold for Non-uniform Random k-SAT","volume":"Volume 10929","author":"Friedrich","year":"2018","journal-title":"Proceedings of the 21st International Conference Theory and Applications of Satisfiability Testing, SAT 2018"},{"key":"ref_16","first-page":"61:1","article-title":"The Satisfiability Threshold for Non-Uniform Random 2-SAT","volume":"Volume 132","author":"Friedrich","year":"2019","journal-title":"Proceedings of the 46th International Colloquium on Automata, Languages, and Programming, ICALP 2019"},{"key":"ref_17","doi-asserted-by":"crossref","first-page":"249","DOI":"10.1007\/s00453-007-0082-7","article-title":"Random 2-SAT with Prescribed Literal Degrees","volume":"48","author":"Cooper","year":"2007","journal-title":"Algorithmica"},{"key":"ref_18","doi-asserted-by":"crossref","first-page":"53","DOI":"10.1007\/978-3-030-24258-9_4","article-title":"Satisfiability Threshold for Power Law Random 2-SAT in Configuration Model","volume":"Volume 11628","author":"Omelchenko","year":"2019","journal-title":"Proceedings of the 22nd International Conference on Theory and Applications of Satisfiability Testing, SAT 2019"},{"key":"ref_19","unstructured":"Omelchenko, O., and Bulatov, A. (2021, January 2\u20139). Satisfiability and Algorithms for Non-uniform Random k-SAT. Proceedings of the Thirty-Fifth AAAI Conference on Artificial Intelligence, AAAI 2021, Vancouver, BC, Canada."},{"key":"ref_20","doi-asserted-by":"crossref","first-page":"70","DOI":"10.1016\/j.tcs.2021.07.028","article-title":"Satisfiability threshold for power law random 2-SAT in configuration model","volume":"888","author":"Omelchenko","year":"2021","journal-title":"Theor. Comput. Sci."},{"key":"ref_21","doi-asserted-by":"crossref","unstructured":"Gir\u00e1ldez-Cru, J., and Levy, J. (2017, January 19\u201325). Locality in Random SAT Instances. Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence, IJCAI 2017. ijcai.org, Melbourne, Australia.","DOI":"10.24963\/ijcai.2017\/89"},{"key":"ref_22","doi-asserted-by":"crossref","first-page":"103537","DOI":"10.1016\/j.artint.2021.103537","article-title":"Popularity-similarity random SAT formulas","volume":"299","author":"Levy","year":"2021","journal-title":"Artif. Intell."},{"key":"ref_23","doi-asserted-by":"crossref","first-page":"609","DOI":"10.1002\/rsa.20993","article-title":"The number of satisfying assignments of random 2-SAT formulas","volume":"58","author":"Achlioptas","year":"2021","journal-title":"Random Struct. Algorithms"},{"key":"ref_24","doi-asserted-by":"crossref","unstructured":"Bl\u00e4sius, T., Friedrich, T., G\u00f6bel, A., Levy, J., and Rothenberger, R. (2021, January 10\u201313). The Impact of Heterogeneity and Geometry on the Proof Complexity of Random Satisfiability. Proceedings of the 2021 ACM-SIAM Symposium on Discrete Algorithms, SODA 2021, SIAM 2021.","DOI":"10.1137\/1.9781611976465.4"},{"key":"ref_25","doi-asserted-by":"crossref","first-page":"509","DOI":"10.1126\/science.286.5439.509","article-title":"Emergence of scaling in random networks","volume":"286","author":"Albert","year":"1999","journal-title":"Science"},{"key":"ref_26","unstructured":"Dorogovtsev, S.N., and Mendes, J.F.F. (2003). Evolution of Networks: From Biological Nets to the Internet and WWW (Physics), Oxford University Press, Inc."},{"key":"ref_27","doi-asserted-by":"crossref","first-page":"1842","DOI":"10.1103\/PhysRevE.62.1842","article-title":"Evolution of networks with aging of sites","volume":"62","author":"Dorogovtsev","year":"2000","journal-title":"Phys. Rev. E"},{"key":"ref_28","doi-asserted-by":"crossref","first-page":"296","DOI":"10.1016\/0097-3165(78)90059-6","article-title":"The asymptotic number of labeled graphs with given degree sequences","volume":"24","author":"Bender","year":"1978","journal-title":"J. Comb. Theory Ser. A"},{"key":"ref_29","doi-asserted-by":"crossref","unstructured":"Bollob\u00e1s, B. (2001). Random Graphs, Cambridge Studies in Advanced Mathematics, Cambridge University Press.","DOI":"10.1017\/CBO9780511814068"},{"key":"ref_30","doi-asserted-by":"crossref","unstructured":"Aiello, W., Chung, F., and Lu, L. (2000, January 21\u201323). A Random Graph Model for Massive Graphs. Proceedings of the Thirty-Second Annual ACM Symposium on Theory of Computing, Portland, OR, USA.","DOI":"10.1145\/335305.335326"},{"key":"ref_31","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1007\/PL00012580","article-title":"Connected Components in Random Graphs with Given Expected Degree Sequences","volume":"6","author":"Chung","year":"2002","journal-title":"Ann. Comb."},{"key":"ref_32","doi-asserted-by":"crossref","first-page":"278701","DOI":"10.1103\/PhysRevLett.87.278701","article-title":"Universal behavior of load distribution in scale-free networks","volume":"87","author":"Goh","year":"2001","journal-title":"Phys. Rev. Lett."},{"key":"ref_33","doi-asserted-by":"crossref","first-page":"479","DOI":"10.1007\/BF00050700","article-title":"Approximations to the birthday problem with unequal occurrence probabilities and their application to the surname problem in Japan","volume":"44","author":"Mase","year":"1992","journal-title":"Ann. Inst. Stat. Math."},{"key":"ref_34","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1007\/s10817-005-9012-z","article-title":"Regular Random k-SAT: Properties of Balanced Formulas","volume":"35","author":"Boufkhad","year":"2005","journal-title":"J. Autom. Reason."},{"key":"ref_35","doi-asserted-by":"crossref","unstructured":"Chv\u00e1tal, V., and Reed, B.A. (1992, January 244\u201327). Mick Gets Some (the Odds Are on His Side). Proceedings of the 33rd Annual Symposium on Foundations of Computer Science, FOCS 1992, Pittsburgh, PA, USA.","DOI":"10.1109\/SFCS.1992.267789"},{"key":"ref_36","first-page":"290","article-title":"On Random Graphs I","volume":"6","year":"1959","journal-title":"Publ. Math."},{"key":"ref_37","doi-asserted-by":"crossref","first-page":"1141","DOI":"10.1214\/aoms\/1177706098","article-title":"Random Graphs","volume":"30","author":"Gilbert","year":"1959","journal-title":"Ann. Math. Stat."},{"key":"ref_38","first-page":"17","article-title":"On the evolution of random graphs","volume":"5","year":"1960","journal-title":"Publ. Math. Inst. Hungary. Acad. Sci."},{"key":"ref_39","unstructured":"Mitchell, D.G., Selman, B., and Levesque, H.J. (1992, January 12\u201316). Hard and Easy Distributions of SAT Problems. Proceedings of the 10th National Conference on Artificial Intelligence (AAAI 1992), San Jose, CA, USA."},{"key":"ref_40","unstructured":"Gent, I.P., and Walsh, T. (1994, January 8\u201312). The SAT Phase Transition. Proceedings of the 11th European Conference on Artificial Intelligenc (ECAI 1994), Amsterdam, The Netherlands."},{"key":"ref_41","unstructured":"Achlioptas, D., Chtcherba, A.D., Istrate, G., and Moore, C. (2001, January 7\u20139). The phase transition in 1-in-k SAT and NAE 3-SAT. Proceedings of the 20th Annual Symposium on Discrete Algorithms, SODA 2001, Washington, DC, USA."},{"key":"ref_42","doi-asserted-by":"crossref","first-page":"251","DOI":"10.1002\/rsa.20465","article-title":"Delaying satisfiability for random 2SAT","volume":"43","author":"Sinclair","year":"2013","journal-title":"Random Struct. Algorithms"},{"key":"ref_43","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1002\/rsa.1006","article-title":"The Scaling Window of the 2-SAT Transition","volume":"18","author":"Borgs","year":"2001","journal-title":"Random Struct. Algorithms"},{"key":"ref_44","doi-asserted-by":"crossref","first-page":"257","DOI":"10.1090\/S0002-9947-1984-0756039-5","article-title":"The evolution of random graphs","volume":"286","year":"1984","journal-title":"Trans. Am. Math. Soc."},{"key":"ref_45","doi-asserted-by":"crossref","first-page":"414","DOI":"10.1002\/(SICI)1098-2418(199910\/12)15:3\/4<414::AID-RSA10>3.0.CO;2-G","article-title":"2+p-SAT: Relation of typical-case complexity to the nature of the phase transition","volume":"15","author":"Monasson","year":"1999","journal-title":"Random Struct. Algorithms"},{"key":"ref_46","doi-asserted-by":"crossref","first-page":"121","DOI":"10.1016\/0020-0190(79)90002-4","article-title":"A Linear-Time Algorithm for Testing the Truth of Certain Quantified Boolean Formulas","volume":"8","author":"Aspvall","year":"1979","journal-title":"Inf. Process. Lett."},{"key":"ref_47","doi-asserted-by":"crossref","first-page":"161","DOI":"10.1002\/rsa.3240060204","article-title":"A critical point for random graphs with a given degree sequence","volume":"6","author":"Molloy","year":"1995","journal-title":"Random Struct. Algorithms"},{"key":"ref_48","doi-asserted-by":"crossref","unstructured":"Newman, M.E.J. (2010). Networks: An Introduction, Oxford University Press.","DOI":"10.1093\/acprof:oso\/9780199206650.003.0001"},{"key":"ref_49","doi-asserted-by":"crossref","first-page":"4626","DOI":"10.1103\/PhysRevLett.85.4626","article-title":"Resilience of the Internet to Random Breakdowns","volume":"85","author":"Cohen","year":"2000","journal-title":"Phys. Rev. Lett."},{"key":"ref_50","doi-asserted-by":"crossref","unstructured":"Cohen, R., Havlin, S., and ben Avraham, D. (2002). Structural properties of scale-free networks. Handbook of Graphs and Networks, John Wiley & Sons, Ltd.. Chapter 4.","DOI":"10.1002\/3527602755.ch4"},{"key":"ref_51","unstructured":"Boufkhad, Y., Dubois, O., Interian, Y., and Selman, B. (2005, January 19\u201323). Regular Random k-SAT: Properties of Balanced Formulas. Proceedings of the 8th International Conference on Theory and Applications of Satisfiability Testing (SAT 2005), St Andrews, UK."}],"container-title":["Algorithms"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.mdpi.com\/1999-4893\/15\/6\/219\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T23:36:10Z","timestamp":1760139370000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.mdpi.com\/1999-4893\/15\/6\/219"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,6,20]]},"references-count":51,"journal-issue":{"issue":"6","published-online":{"date-parts":[[2022,6]]}},"alternative-id":["a15060219"],"URL":"https:\/\/doi.org\/10.3390\/a15060219","relation":{},"ISSN":["1999-4893"],"issn-type":[{"value":"1999-4893","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,6,20]]}}}