{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,12]],"date-time":"2025-10-12T02:51:49Z","timestamp":1760237509876,"version":"build-2065373602"},"reference-count":32,"publisher":"MDPI AG","issue":"5","license":[{"start":{"date-parts":[[2020,5,19]],"date-time":"2020-05-19T00:00:00Z","timestamp":1589846400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100001809","name":"the National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["61762019,61862051"],"award-info":[{"award-number":["61762019,61862051"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Entropy"],"abstract":"<jats:p>Unique k-SAT is the promised version of k-SAT where the given formula has 0 or 1 solution and is proved to be as difficult as the general k-SAT. For any     k \u2265 3    ,     s \u2265 f ( k , d )     and     ( s + d ) \/ 2 &gt; k \u2212 1    , a parsimonious reduction from k-CNF to d-regular (k,s)-CNF is given. Here regular (k,s)-CNF is a subclass of CNF, where each clause of the formula has exactly k distinct variables, and each variable occurs in exactly s clauses. A d-regular (k,s)-CNF formula is a regular (k,s)-CNF formula, in which the absolute value of the difference between positive and negative occurrences of every variable is at most a nonnegative integer d. We prove that for all     k \u2265 3    ,     f ( k , d ) \u2264 u ( k , d ) + 1     and     f ( k , d + 1 ) \u2264 u ( k , d )    . The critical function     f ( k , d )     is the maximal value of s, such that every d-regular (k,s)-CNF formula is satisfiable. In this study,     u ( k , d )     denotes the minimal value of s such that there exists a uniquely satisfiable d-regular (k,s)-CNF formula. We further show that for     s \u2265 f ( k , d ) + 1     and     ( s + d ) \/ 2 &gt; k \u2212 1    , there exists a uniquely satisfiable d-regular     ( k , s + 1 )    -CNF formula. Moreover, for     k \u2265 7    , we have that     u ( k , d ) \u2264 f ( k , d ) + 1    .<\/jats:p>","DOI":"10.3390\/e22050569","type":"journal-article","created":{"date-parts":[[2020,5,20]],"date-time":"2020-05-20T02:48:24Z","timestamp":1589942904000},"page":"569","update-policy":"https:\/\/doi.org\/10.3390\/mdpi_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Uniquely Satisfiable d-Regular (k,s)-SAT Instances"],"prefix":"10.3390","volume":"22","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6605-2370","authenticated-orcid":false,"given":"Zufeng","family":"Fu","sequence":"first","affiliation":[{"name":"College of Computer Science and Technology, Guizhou University, Guiyang 550025, China"},{"name":"Department of Electronics and Information Engineering, Anshun University, Anshun 561000, 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"}]}],"member":"1968","published-online":{"date-parts":[[2020,5,19]]},"reference":[{"key":"ref_1","doi-asserted-by":"crossref","unstructured":"Cook, S.A. (1971, January 3\u20135). The complexity of theorem-proving procedures. Proceedings of the Third Annual ACM Symposium on Theory of Computing, Shaker Heights, OH, USA.","DOI":"10.1145\/800157.805047"},{"key":"ref_2","doi-asserted-by":"crossref","unstructured":"E\u00e9n, N., and Sorenss\u00f6n, N. (2003). An Extensible SAT-solver. Theory and Applications of Satisfiability Testing, Springer.","DOI":"10.1007\/978-3-540-24605-3_37"},{"key":"ref_3","unstructured":"Audemard, G., and Simon, L. (2012, January 16). GLUCOSE2.1: Aggressive-but Reactive-Clause Database Management, Dynamic Restarts. Proceedings of the International Workshop of Pragmatics of SAT, Trento, Italy."},{"key":"ref_4","doi-asserted-by":"crossref","unstructured":"Luo, M., Minli, M., Xiao, F., Many\u00e1, F., and Zhipeng, L. (2017, January 19\u201325). An Effective Learnt Clause Minimization Approach for CDCL SAT Solvers. Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence, Melbourne, Australia.","DOI":"10.24963\/ijcai.2017\/98"},{"key":"ref_5","doi-asserted-by":"crossref","unstructured":"Calabro, C., and Paturi, R. (2009). k-SAT Is No Harder Than Decision-Unique-k-SAT. Computer Science Symposium in Russia, Springer.","DOI":"10.1007\/978-3-642-03351-3_8"},{"key":"ref_6","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1016\/0166-218X(84)90081-7","article-title":"A simplified NP-complete satisfiability problem","volume":"8","author":"Tovey","year":"1984","journal-title":"Discret. Appl. Math."},{"key":"ref_7","first-page":"691","article-title":"A Regular NP-Complete Problem and Its Inapproximability","volume":"7","author":"Daoyun","year":"2013","journal-title":"J. Front. Comput. Sci. Technol."},{"key":"ref_8","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1016\/0004-3702(95)00046-1","article-title":"Experimental Results on the Crossover Point in Satisfiability Problems","volume":"81","author":"Crawford","year":"1996","journal-title":"Artif. Intell."},{"key":"ref_9","doi-asserted-by":"crossref","first-page":"1297","DOI":"10.1126\/science.264.5163.1297","article-title":"Critical behavior in the satisfiability of random boolean expressions","volume":"264","author":"Kirkpatrick","year":"1994","journal-title":"Science"},{"key":"ref_10","first-page":"2985","article-title":"Satisfiability Threshold of the Regular Random (k,r)-SAT Problem","volume":"27","author":"Jincheng","year":"2016","journal-title":"J. Softw."},{"key":"ref_11","first-page":"7","article-title":"Satisfiability threshold of regular (k,r)-SAT problem via 1RSB theory","volume":"45","author":"Jincheng","year":"2017","journal-title":"J. Huazhong Univ. Sci. Technol."},{"key":"ref_12","doi-asserted-by":"crossref","first-page":"812","DOI":"10.1126\/science.1073287","article-title":"Analytic and algorithmic solution of random satisfiability problems","volume":"297","author":"Parisi","year":"2002","journal-title":"Science"},{"key":"ref_13","doi-asserted-by":"crossref","unstructured":"Wahlstr\u00f6m, M. (2005). Faster exact solving of SAT formulae with a low number of occurrences per variable. Theory and Applications of Satisfiability Testing (SAT-2005), Springer.","DOI":"10.1007\/11499107_23"},{"key":"ref_14","doi-asserted-by":"crossref","unstructured":"Wahlstr\u00f6m, M. (2005). An algorithm for the SAT problem for formulae of linear length. European Conference on Algorithms, Springer.","DOI":"10.1007\/11561071_12"},{"key":"ref_15","doi-asserted-by":"crossref","unstructured":"Johannsen, D., Razgon, I., and Wahlstr\u00f6m, M. (2009). Solving SAT for CNF Formulas with a One-Sided Restriction on Variable Occurrences. Theory and Applications of Satisfiability Testing, Springer.","DOI":"10.1007\/978-3-642-02777-2_10"},{"key":"ref_16","first-page":"1113","article-title":"The NP-completeness of d-regular (k,s)-SAT problem","volume":"31","author":"Fu","year":"2020","journal-title":"J. Softw."},{"key":"ref_17","doi-asserted-by":"crossref","unstructured":"Fu, Z., and Xu, D. (2020). (1,0)-Super Solutions of (k,s)-CNF Formula. Entropy, 22.","DOI":"10.3390\/e22020253"},{"key":"ref_18","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1016\/0304-3975(86)90135-0","article-title":"NP is as easy as detecting unique solutions","volume":"47","author":"Valiant","year":"1986","journal-title":"Theor. Comput. Sci."},{"key":"ref_19","doi-asserted-by":"crossref","first-page":"386","DOI":"10.1016\/j.jcss.2007.06.015","article-title":"The complexity of unique k-SAT: An isolation lemma for k-CNFs","volume":"74","author":"Calabro","year":"2008","journal-title":"Comput. Syst. Sci."},{"key":"ref_20","doi-asserted-by":"crossref","unstructured":"Matthews, W., and Paturi, R. (2010). Uniquely Satisfiable k-SAT Instances with Almost Minimal Occurrences of Each Variable. Theory and Applications of Satisfiability Testing, Springer.","DOI":"10.1007\/978-3-642-14186-7_34"},{"key":"ref_21","first-page":"203","article-title":"One more occurrence of variables makes satisfiability jump from trivial to NP-complete","volume":"22","author":"Tuza","year":"1993","journal-title":"Acta Inform."},{"key":"ref_22","doi-asserted-by":"crossref","first-page":"347","DOI":"10.1016\/j.tcs.2005.02.004","article-title":"Computing unsatisfiable k-SAT instances with few occurrences per variable","volume":"337","author":"Hoory","year":"2004","journal-title":"Theor. Comput. Sci."},{"key":"ref_23","doi-asserted-by":"crossref","first-page":"523","DOI":"10.1137\/S0895480104445745","article-title":"Families of unsatisfiable k-CNF formulas with few occurrences per variable","volume":"20","author":"Hoory","year":"2006","journal-title":"SIAM J. Discret. Math."},{"key":"ref_24","first-page":"495","article-title":"DNF tautologies with a limited number of occurrences of every variable","volume":"238","author":"Sgall","year":"2007","journal-title":"Theor. Comput. Sci."},{"key":"ref_25","first-page":"664","article-title":"The Local Lemma is asymptotically tight for SAT","volume":"63","author":"Gebauer","year":"2016","journal-title":"ACM"},{"key":"ref_26","doi-asserted-by":"crossref","first-page":"221","DOI":"10.3233\/SAT190024","article-title":"Locality and Hard SAT-Instances","volume":"2","year":"2006","journal-title":"J. Satisf. Boolean Modeling Comput."},{"key":"ref_27","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."},{"key":"ref_28","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, Melbourne, Australia.","DOI":"10.24963\/ijcai.2017\/89"},{"key":"ref_29","doi-asserted-by":"crossref","unstructured":"Clark, D., Frank, J., Gent, I., MacIntyre, E., Tomov, N., and Walsh, T. (1996). Local search and the number of solutions. The Principles and Practices of Contraint Programming (CP96), Springer.","DOI":"10.1007\/3-540-61551-2_70"},{"key":"ref_30","doi-asserted-by":"crossref","first-page":"235","DOI":"10.1613\/jair.711","article-title":"Backbone fragility and the local search cost peak","volume":"12","author":"Singer","year":"2000","journal-title":"J. Artif. Intell. Res."},{"key":"ref_31","unstructured":"Znidaric, M. (2005). Single-solution Random 3-SAT Instances. arXiv."},{"key":"ref_32","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1016\/0166-218X(90)90020-D","article-title":"On the r,s-SAT satisfiability problem and a conjecture of Tovey","volume":"26","author":"Dubois","year":"1990","journal-title":"Discret. Appl. Math."}],"container-title":["Entropy"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.mdpi.com\/1099-4300\/22\/5\/569\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T09:30:26Z","timestamp":1760175026000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.mdpi.com\/1099-4300\/22\/5\/569"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,5,19]]},"references-count":32,"journal-issue":{"issue":"5","published-online":{"date-parts":[[2020,5]]}},"alternative-id":["e22050569"],"URL":"https:\/\/doi.org\/10.3390\/e22050569","relation":{},"ISSN":["1099-4300"],"issn-type":[{"type":"electronic","value":"1099-4300"}],"subject":[],"published":{"date-parts":[[2020,5,19]]}}}