{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,12]],"date-time":"2025-10-12T01:51:41Z","timestamp":1760233901666,"version":"build-2065373602"},"reference-count":25,"publisher":"MDPI AG","issue":"3","license":[{"start":{"date-parts":[[2021,3,4]],"date-time":"2021-03-04T00:00:00Z","timestamp":1614816000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"the Science and Technology Foundation of Guizhou Province","award":["NO. [2019]1299"],"award-info":[{"award-number":["NO. [2019]1299"]}]},{"name":"the General program of Qiannan Normal University for Nationalities of China","award":["qnsy2018016"],"award-info":[{"award-number":["qnsy2018016"]}]},{"name":"the Industrial Technology Foundation of Qiannan State of China","award":["Qiannan Ke He Gong Zi (2017) 16 Hao"],"award-info":[{"award-number":["Qiannan Ke He Gong Zi (2017) 16 Hao"]}]},{"name":"the Nature Science Foundation of Qiannan","award":["[2017]10"],"award-info":[{"award-number":["[2017]10"]}]},{"name":"the Top-notch Talent Program of of Guizhou province","award":["KY[2018]080"],"award-info":[{"award-number":["KY[2018]080"]}]},{"name":"the Young Science and Technology Talent Growth Fund Project of Education Department of Guizhou Province of China","award":["Qian Jiao He KY Zi[2017]343","Qian Jiao He KY Zi[2017]354","Qian Jiao He KY Zi [2018]411"],"award-info":[{"award-number":["Qian Jiao He KY Zi[2017]343","Qian Jiao He KY Zi[2017]354","Qian Jiao He KY Zi [2018]411"]}]},{"DOI":"10.13039\/501100001809","name":"the National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["61762019","61862051","62062001"],"award-info":[{"award-number":["61762019","61862051","62062001"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Entropy"],"abstract":"<jats:p>The satisfiability (SAT) problem is a core problem in computer science. Existing studies have shown that most industrial SAT instances can be effectively solved by modern SAT solvers while random SAT instances cannot. It is believed that the structural characteristics of different SAT formula classes are the reasons behind this difference. In this paper, we study the structural properties of propositional formulas in conjunctive normal form (CNF) by the principle of structural entropy of formulas. First, we used structural entropy to measure the complex structure of a formula and found that the difficulty solving the formula is related to the structural entropy of the formula. The smaller the compressing information of a formula, the more difficult it is to solve the formula. Secondly, we proposed a \u03bb-approximation strategy to approximate the structural entropy of large formulas. The experimental results showed that the proposed strategy can effectively approximate the structural entropy of the original formula and that the approximation ratio is more than 92%. Finally, we analyzed the structural properties of a formula in the solution process and found that a local search solver tends to select variables in different communities to perform the next round of searches during a search and that the structural entropy of a variable affects the probability of the variable being flipped. By using these conclusions, we also proposed an initial candidate solution generation strategy for a local search for SAT, and the experimental results showed that this strategy effectively improves the performance of the solvers CCAsat and Sparrow2011 when incorporated into these two solvers.<\/jats:p>","DOI":"10.3390\/e23030303","type":"journal-article","created":{"date-parts":[[2021,3,4]],"date-time":"2021-03-04T21:58:07Z","timestamp":1614895087000},"page":"303","update-policy":"https:\/\/doi.org\/10.3390\/mdpi_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["A Structural Entropy Measurement Principle of Propositional Formulas in Conjunctive Normal Form"],"prefix":"10.3390","volume":"23","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0016-2419","authenticated-orcid":false,"given":"Zaijun","family":"Zhang","sequence":"first","affiliation":[{"name":"College of Computer Science and Technology, Guizhou University, Guiyang 550025, China"},{"name":"Key Laboratory of Complex Systems and Intelligent Computing and School of Mathematics and Statistics, Qiannan Normal University for Nationalities, Duyun 558000, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Daoyun","family":"Xu","sequence":"additional","affiliation":[{"name":"College of Computer Science and Technology, Guizhou University, Guiyang 550025, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1995-4002","authenticated-orcid":false,"given":"Jincheng","family":"Zhou","sequence":"additional","affiliation":[{"name":"Key Laboratory of Complex Systems and Intelligent Computing and School of Mathematics and Statistics, Qiannan Normal University for Nationalities, Duyun 558000, China"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"1968","published-online":{"date-parts":[[2021,3,4]]},"reference":[{"doi-asserted-by":"crossref","unstructured":"Cook, S.A. (1971). The Complexity of Theorem-Proving Procedures. Proceedings of the Third Annual ACM Symposium on Theory of Computing, Association for Computing Machinery.","key":"ref_1","DOI":"10.1145\/800157.805047"},{"unstructured":"Williams, R., Gomes, C., and Selman, B. (2003, January 9\u201315). Backdoors To Typical Case Complexity. Proceedings of the IJCAI International Joint Conference on Artificial Intelligence, Acapulco, Mexico.","key":"ref_2"},{"key":"ref_3","first-page":"109","article-title":"Towards Industrial-Like Random SAT Instances","volume":"184","author":"Bonet","year":"2008","journal-title":"Front. Artif. Intell. Appl."},{"doi-asserted-by":"crossref","unstructured":"Ans\u00f3tegui, C., Gir\u00e1ldez-Cru, J., and Levy, J. (2012). The community structure of SAT formulas. International Conference on Theory and Applications of Satisfiability Testing, Springer.","key":"ref_4","DOI":"10.1007\/978-3-642-31612-8_31"},{"key":"ref_5","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."},{"doi-asserted-by":"crossref","unstructured":"Newsham, Z., Ganesh, V., Fischmeister, S., Audemard, G., and Simon, L. (2014). Impact of community structure on SAT solver performance. International Conference on Theory and Applications of Satisfiability Testing, Springer.","key":"ref_6","DOI":"10.1007\/978-3-319-09284-3_20"},{"key":"ref_7","first-page":"62","article-title":"SATGraf: Visualizing the evolution of SAT formula structure in solvers","volume":"Volume 9340","author":"Newsham","year":"2015","journal-title":"International Conference on Theory and Applications of Satisfiability Testing"},{"doi-asserted-by":"crossref","unstructured":"Martins, R., Manquinho, V., and Lynce, I. (2013). Community-based partitioning for MaxSAT solving. International Conference on Theory and Applications of Satisfiability Testing, Springer.","key":"ref_8","DOI":"10.1007\/978-3-642-39071-5_14"},{"doi-asserted-by":"crossref","unstructured":"Sonobe, T., Kondoh, S., and Inaba, M. (2014). Community Branching for Parallel Portfolio SAT Solvers. International Conference on Theory and Applications of Satisfiability Testing, Springer.","key":"ref_9","DOI":"10.1007\/978-3-319-09284-3_14"},{"key":"ref_10","doi-asserted-by":"crossref","first-page":"119","DOI":"10.1016\/j.artint.2016.06.001","article-title":"Generating SAT instances with community structure","volume":"238","author":"Levy","year":"2016","journal-title":"Artif. Intell."},{"doi-asserted-by":"crossref","unstructured":"Gir\u00e1ldez-Cru, J., and Levy, J. (2017, January 19\u201325). Locality in random SAT instances. Proceedings of the IJCAI International Joint Conference on Artificial Intelligence, Melbourne, Australia.","key":"ref_11","DOI":"10.24963\/ijcai.2017\/89"},{"key":"ref_12","doi-asserted-by":"crossref","first-page":"3290","DOI":"10.1109\/TIT.2016.2555904","article-title":"Structural Information and Dynamical Complexity of Networks","volume":"62","author":"Li","year":"2016","journal-title":"IEEE Trans. Inf. Theory"},{"key":"ref_13","doi-asserted-by":"crossref","first-page":"211","DOI":"10.1016\/j.physa.2016.09.009","article-title":"Resistance maximization principle for defending networks against virus attack","volume":"466","author":"Li","year":"2017","journal-title":"Phys. A Stat. Mech. Appl."},{"key":"ref_14","doi-asserted-by":"crossref","first-page":"3265","DOI":"10.1038\/s41467-018-05691-7","article-title":"Decoding topologically associating domains with ultra-low resolution Hi-C data by graph structural entropy","volume":"9","author":"Li","year":"2018","journal-title":"Nat. Commun."},{"key":"ref_15","doi-asserted-by":"crossref","first-page":"20412","DOI":"10.1038\/srep20412","article-title":"Three-Dimensional Gene Map of Cancer Cell Types: Structural Entropy Minimisation Principle for Defining Tumour Subtypes","volume":"6","author":"Li","year":"2016","journal-title":"Sci. Rep."},{"key":"ref_16","doi-asserted-by":"crossref","first-page":"878","DOI":"10.1016\/j.physa.2015.05.039","article-title":"Discovering natural communities in networks","volume":"436","author":"Li","year":"2015","journal-title":"Phys. A Stat. Mech. Appl."},{"key":"ref_17","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1016\/j.artint.2013.09.001","article-title":"Local search for Boolean Satisfiability with configuration checking and subscore","volume":"204","author":"Cai","year":"2013","journal-title":"Artif. Intell."},{"doi-asserted-by":"crossref","unstructured":"Balint, A., and Frohlich, A. (2010, January 11\u201314). Improving Stochastic Local Search for SAT with a New Probability Distribution. Proceedings of the 13th International Conference (SAT 2010), Edinburgh, UK.","key":"ref_18","DOI":"10.1007\/978-3-642-14186-7_3"},{"key":"ref_19","doi-asserted-by":"crossref","first-page":"026113","DOI":"10.1103\/PhysRevE.69.026113","article-title":"Finding and Evaluating Community Structure in Networks","volume":"69","author":"Newman","year":"2004","journal-title":"Phys. Rev. E"},{"key":"ref_20","doi-asserted-by":"crossref","first-page":"1297","DOI":"10.1126\/science.264.5163.1297","article-title":"Critical Behavior in the Satis ability of Random Boolean Formulae","volume":"264","author":"Kirkpatrick","year":"1994","journal-title":"Science"},{"key":"ref_21","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1002\/rsa.20057","article-title":"Survey propagation: An algorithm for satisfiability","volume":"27","author":"Braunstein","year":"2005","journal-title":"Random Struct. Algorithms"},{"key":"ref_22","doi-asserted-by":"crossref","first-page":"056126","DOI":"10.1103\/PhysRevE.66.056126","article-title":"Random [formula presented]-satisfiability problem: From an analytic solution to an efficient algorithm","volume":"66","author":"Zecchina","year":"2002","journal-title":"Phys. Rev. E"},{"unstructured":"Selman, B., Kautz, H., and McAllester, D. (1997, January 23\u201329). Ten challenges in propositional reasoning and search. Proceedings of the IJCAI International Joint Conference on Artificial Intelligence, Nagoya, Japan.","key":"ref_23"},{"key":"ref_24","first-page":"1","article-title":"Ten challenges redux: Recent progress in propositional reasoning and search","volume":"Volume 2833","author":"Kautz","year":"2003","journal-title":"International Conference on Principles and Practice of Constraint Programming"},{"key":"ref_25","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."}],"container-title":["Entropy"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.mdpi.com\/1099-4300\/23\/3\/303\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T05:32:41Z","timestamp":1760160761000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.mdpi.com\/1099-4300\/23\/3\/303"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,3,4]]},"references-count":25,"journal-issue":{"issue":"3","published-online":{"date-parts":[[2021,3]]}},"alternative-id":["e23030303"],"URL":"https:\/\/doi.org\/10.3390\/e23030303","relation":{},"ISSN":["1099-4300"],"issn-type":[{"type":"electronic","value":"1099-4300"}],"subject":[],"published":{"date-parts":[[2021,3,4]]}}}