{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,19]],"date-time":"2025-09-19T09:30:49Z","timestamp":1758274249983,"version":"3.41.0"},"reference-count":26,"publisher":"Springer Science and Business Media LLC","issue":"12","license":[{"start":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T00:00:00Z","timestamp":1751587200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T00:00:00Z","timestamp":1751587200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Front. Comput. Sci."],"published-print":{"date-parts":[[2025,12]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>In this paper, we identify the distinction between non-brute-force computation and brute-force computation as the most fundamental problem in computer science. Subsequently, we prove, by the diagonalization method, that constructed self-referential CSPs cannot be solved by non-brute-force computation, which is stronger than P \u2260 NP. This constructive method for proving impossibility results is very different (and missing) from existing approaches in computational complexity theory, but aligns with G\u00f6del\u2019s technique for proving logical impossibility. Just as G\u00f6del showed that proving formal unprovability is feasible in mathematics, our results show that proving computational hardness is not hard in mathematics. Specifically, proving lower bounds for many problems, such as 3-SAT, can be challenging because these problems have various effective strategies available to avoid exhaustive search. However, for self-referential examples that are extremely hard, exhaustive search becomes unavoidable, making its necessity easier to prove. Consequently, it renders the separation between non-brute-force computation and brute-force computation much simpler than that between P and NP. Finally, our results are akin to G\u00f6del\u2019s incompleteness theorem, as they reveal the limits of reasoning and highlight the intrinsic distinction between syntax and semantics.<\/jats:p>","DOI":"10.1007\/s11704-025-50231-4","type":"journal-article","created":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T04:31:35Z","timestamp":1751603495000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["SAT requires exhaustive search"],"prefix":"10.1007","volume":"19","author":[{"given":"Ke","family":"Xu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Guangyan","family":"Zhou","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,7,4]]},"reference":[{"issue":"1","key":"50231_CR1","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1613\/jair.696","volume":"12","author":"K Xu","year":"2000","unstructured":"Xu K, Li W. Exact phase transitions in random constraint satisfaction problems. Journal of Artificial Intelligence Research, 2000, 12(1): 93\u2013103","journal-title":"Journal of Artificial Intelligence Research"},{"key":"50231_CR2","first-page":"337","volume-title":"Proceedings of the 19th International Joint Conference on Artificial Intelligence","author":"K Xu","year":"2005","unstructured":"Xu K, Boussemart F, Hemery F, Lecoutre C. A simple model to generate hard satisfiable instances. In: Proceedings of the 19th International Joint Conference on Artificial Intelligence. 2005, 337\u2013342"},{"issue":"3","key":"50231_CR3","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1016\/j.tcs.2006.01.001","volume":"355","author":"K Xu","year":"2006","unstructured":"Xu K, Li W. Many hard examples in exact phase transitions. Theoretical Computer Science, 2006, 355(3): 291\u2013302","journal-title":"Theoretical Computer Science"},{"issue":"8\u20139","key":"50231_CR4","doi-asserted-by":"publisher","first-page":"514","DOI":"10.1016\/j.artint.2007.04.001","volume":"171","author":"K Xu","year":"2007","unstructured":"Xu K, Boussemart F, Hemery F, Lecoutre C. Random constraint satisfaction: easy generation of hard (satisfiable) instances. Artificial Intelligence, 2007, 171(8\u20139): 514\u2013534","journal-title":"Artificial Intelligence"},{"key":"50231_CR5","first-page":"611","volume-title":"Proceedings of the 22nd International Joint Conference on Artificial Intelligence","author":"T Liu","year":"2011","unstructured":"Liu T, Lin X, Wang C, Su K, Xu K. Large hinge width on sparse random hypergraphs. In: Proceedings of the 22nd International Joint Conference on Artificial Intelligence. 2011, 611\u2013616"},{"issue":"9\u201310","key":"50231_CR6","doi-asserted-by":"publisher","first-page":"1672","DOI":"10.1016\/j.artint.2011.03.003","volume":"175","author":"S Cai","year":"2011","unstructured":"Cai S, Su K, Sattar A. Local search with edge weighting and configuration checking heuristics for minimum vertex cover. Artificial Intelligence, 2011, 175(9\u201310): 1672\u20131696","journal-title":"Artificial Intelligence"},{"issue":"20","key":"50231_CR7","doi-asserted-by":"publisher","first-page":"985","DOI":"10.1016\/j.ipl.2011.07.006","volume":"111","author":"C Zhao","year":"2011","unstructured":"Zhao C, Zheng Z. Threshold behaviors of a random constraint satisfaction problem with exact phase transitions. Information Processing Letters, 2011, 111(20): 985\u2013988","journal-title":"Information Processing Letters"},{"key":"50231_CR8","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511975509","volume-title":"Phase Transitions in Machine Learning","author":"L Saitta","year":"2011","unstructured":"Saitta L, Giordana A, Cornuejols A. Phase Transitions in Machine Learning. Cambridge: Cambridge University Press, 2011"},{"issue":"1","key":"50231_CR9","doi-asserted-by":"publisher","first-page":"016106","DOI":"10.1103\/PhysRevE.85.016106","volume":"85","author":"C Zhao","year":"2012","unstructured":"Zhao C, Zhang P, Zheng Z, Xu K. Analytical and belief-propagation studies of random constraint satisfaction problems with growing domains. Physical Review E, 2012, 85(1): 016106","journal-title":"Physical Review E"},{"key":"50231_CR10","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.artint.2012.08.003","volume":"193","author":"Y Fan","year":"2012","unstructured":"Fan Y, Shen J, Xu K. A general model and thresholds for random constraint satisfaction problems. Artificial Intelligence, 2012, 193: 1\u201317","journal-title":"Artificial Intelligence"},{"key":"50231_CR11","volume-title":"Constraint Networks: Targeting Simplicity for Techniques and Algorithms","author":"C Lecoutre","year":"2013","unstructured":"Lecoutre C. Constraint Networks: Targeting Simplicity for Techniques and Algorithms. John Wiley & Sons, 2013"},{"issue":"7","key":"50231_CR12","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s11432-014-5096-6","volume":"57","author":"P Huang","year":"2014","unstructured":"Huang P, Yin M. An upper (lower) bound for Max (Min) CSP. Science China Information Sciences, 2014, 57(7): 1\u20139","journal-title":"Science China Information Sciences"},{"key":"50231_CR13","doi-asserted-by":"publisher","first-page":"P12006","DOI":"10.1088\/1742-5468\/2015\/12\/P12006","volume":"2015","author":"W Xu","year":"2015","unstructured":"Xu W, Zhang P, Liu T, Gong F. The solution space structure of random constraint satisfaction problems with growing domains. Journal of Statistical Mechanics: Theory and Experiment, 2015, 2015: P12006","journal-title":"Journal of Statistical Mechanics: Theory and Experiment"},{"issue":"3","key":"50231_CR14","doi-asserted-by":"publisher","first-page":"531","DOI":"10.1007\/s10878-013-9704-y","volume":"29","author":"T Liu","year":"2015","unstructured":"Liu T, Wang C, Xu K. Large hypertree width for sparse random hypergraphs. Journal of Combinatorial Optimization, 2015, 29(3): 531\u2013540","journal-title":"Journal of Combinatorial Optimization"},{"key":"50231_CR15","volume-title":"The Art of Computer Programming","author":"D E Knuth","year":"2015","unstructured":"Knuth D E. The Art of Computer Programming. Addison-Wesley Professional, 2015"},{"issue":"1","key":"50231_CR16","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1007\/s10878-015-9891-9","volume":"32","author":"W Xu","year":"2016","unstructured":"Xu W, Gong F. Performances of pure random walk algorithms on constraint satisfaction problems with growing domains. Journal of Combinatorial Optimization, 2016, 32(1): 51\u201366","journal-title":"Journal of Combinatorial Optimization"},{"issue":"1","key":"50231_CR17","doi-asserted-by":"publisher","first-page":"799","DOI":"10.1613\/jair.4953","volume":"55","author":"Z Fang","year":"2016","unstructured":"Fang Z, Li C M, Xu K. An exact algorithm based on MaxSAT reasoning for the maximum weight clique problem. Journal of Artificial Intelligence Research, 2016, 55(1): 799\u2013833","journal-title":"Journal of Artificial Intelligence Research"},{"issue":"11","key":"50231_CR18","first-page":"2712","volume":"27","author":"X F Wang","year":"2016","unstructured":"Wang X F, Xu D Y. Convergence of the belief propagation algorithm for RB model instances. Journal of Software, 2016, 27(11): 2712\u20132724","journal-title":"Journal of Software"},{"issue":"1","key":"50231_CR19","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1287\/ijoc.2017.0770","volume":"30","author":"C M Li","year":"2018","unstructured":"Li C M, Fang Z, Jiang H, Xu K. Incremental upper bound for the maximum clique problem. INFORMS Journal on Computing, 2018, 30(1): 137\u2013153","journal-title":"INFORMS Journal on Computing"},{"key":"50231_CR20","first-page":"6659","volume-title":"Proceedings of the 34th International Conference on Neural Information Processing Systems","author":"N Karalias","year":"2020","unstructured":"Karalias N, Loukas A. Erd\u0151s goes neural: an unsupervised learning framework for combinatorial optimization on graphs. In: Proceedings of the 34th International Conference on Neural Information Processing Systems. 2020, 6659\u20136672"},{"issue":"6","key":"50231_CR21","doi-asserted-by":"publisher","first-page":"166406","DOI":"10.1007\/s11704-021-1189-8","volume":"16","author":"G Zhou","year":"2022","unstructured":"Zhou G, Xu W. Super solutions of the model RB. Frontiers of Computer Science, 2022, 16(6): 166406","journal-title":"Frontiers of Computer Science"},{"issue":"1","key":"50231_CR22","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/BF01700692","volume":"38","author":"K G\u00f6del","year":"1931","unstructured":"G\u00f6del K. \u00dcber formal unentscheidbare S\u00e4tze der Principia Mathematica und verwandter Systeme I. Monatshefte f\u00fcr Mathematik und Physik, 1931, 38(1): 173\u2013198","journal-title":"Monatshefte f\u00fcr Mathematik und Physik"},{"key":"50231_CR23","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1007\/978-3-642-11269-0_6","volume-title":"Proceedings of the 4th International Workshop on Parameterized and Exact Computation","author":"C Calabro","year":"2009","unstructured":"Calabro C, Impagliazzo R, Paturi R. The complexity of satisfiability of small depth circuits. In: Proceedings of the 4th International Workshop on Parameterized and Exact Computation. 2009, 75\u201385"},{"issue":"1","key":"50231_CR24","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1112\/plms\/s2-42.1.230","volume":"S2\u201342","author":"A M Turing","year":"1937","unstructured":"Turing A M. On computable numbers, with an application to the entscheidungsproblem. Proceedings of the London Mathematical Society, 1937, S2\u201342(1): 230\u2013265","journal-title":"Proceedings of the London Mathematical Society"},{"key":"50231_CR25","first-page":"441","volume-title":"Proceedings of the 6th International Conference on Principles and Practice of Constraint Programming","author":"T Walsh","year":"2000","unstructured":"Walsh T. SAT v CSP. In: Proceedings of the 6th International Conference on Principles and Practice of Constraint Programming. 2000, 441\u2013456"},{"key":"50231_CR26","first-page":"151","volume-title":"Proceedings of the 3rd Annual ACM Symposium on Theory of Computing","author":"S A Cook","year":"1971","unstructured":"Cook S A. The complexity of theorem-proving procedures. In: Proceedings of the 3rd Annual ACM Symposium on Theory of Computing. 1971, 151\u2013158"}],"container-title":["Frontiers of Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11704-025-50231-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s11704-025-50231-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11704-025-50231-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T04:31:38Z","timestamp":1751603498000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s11704-025-50231-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,7,4]]},"references-count":26,"journal-issue":{"issue":"12","published-print":{"date-parts":[[2025,12]]}},"alternative-id":["50231"],"URL":"https:\/\/doi.org\/10.1007\/s11704-025-50231-4","relation":{},"ISSN":["2095-2228","2095-2236"],"issn-type":[{"value":"2095-2228","type":"print"},{"value":"2095-2236","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,7,4]]},"assertion":[{"value":"7 March 2025","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"18 May 2025","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"4 July 2025","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"Ke XU is Deputy Editors-in-Chief of the journal and a co-author of this article. To minimize bias, he was excluded from all editorial decision-making related to the acceptance of this article for publication. The remaining authors declare no conflict of interest.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Competing interests"}}],"article-number":"1912405"}}