SAT requires exhaustive search

Abstract

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 \ne NP. This constructive method for proving impossibility results is very different (and missing) from existing approaches in computational complexity theory, but aligns with Gödel’s technique for proving logical impossibility. Just as Gödel 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ödel’s incompleteness theorem, as they reveal the limits of reasoning and highlight the intrinsic distinction between syntax and semantics.

Graphical abstract

Keywords

CSP / SAT / exhaustive search / brute-force computation / lower bounds / self-reference / Model RB

References

[1] Xu K, Li W. Exact phase transitions in random constraint satisfaction problems. Journal of Artificial Intelligence Research, 2000, 12( 1): 93–103

[2] 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−342

[3] Xu K, Li W. Many hard examples in exact phase transitions. Theoretical Computer Science, 2006, 355( 3): 291–302

[4] Xu K, Boussemart F, Hemery F, Lecoutre C. Random constraint satisfaction: easy generation of hard (satisfiable) instances. Artificial Intelligence, 2007, 171(8−9): 514−534

[5] 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−616

[6] Cai S, Su K, Sattar A. Local search with edge weighting and configuration checking heuristics for minimum vertex cover. Artificial Intelligence, 2011, 175(9−10): 1672−1696

[7] Zhao C, Zheng Z. Threshold behaviors of a random constraint satisfaction problem with exact phase transitions. Information Processing Letters, 2011, 111( 20): 985–988

[8] Saitta L, Giordana A, Cornuejols A. Phase Transitions in Machine Learning. Cambridge: Cambridge University Press, 2011

[9] 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

[10] Fan Y, Shen J, Xu K. A general model and thresholds for random constraint satisfaction problems. Artificial Intelligence, 2012, 193: 1–17

[11] Lecoutre C. Constraint Networks: Targeting Simplicity for Techniques and Algorithms. John Wiley & Sons, 2013

[12] Huang P, Yin M. An upper (lower) bound for Max (Min) CSP. Science China Information Sciences, 2014, 57( 7): 1–9

[13] 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

[14] Liu T, Wang C, Xu K. Large hypertree width for sparse random hypergraphs. Journal of Combinatorial Optimization, 2015, 29( 3): 531–540

[15] Knuth D E. The Art of Computer Programming. Addison-Wesley Professional, 2015

[16] 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–66

[17] 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–833

[18] Wang X F, Xu D Y. Convergence of the belief propagation algorithm for RB model instances. Journal of Software, 2016, 27(11): 2712−2724

[19] 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–153

[20] Karalias N, Loukas A. Erdős 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−6672

[21] Zhou G, Xu W. Super solutions of the model RB. Frontiers of Computer Science, 2022, 16( 6): 166406

[22] Gödel K. Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I. Monatshefte für Mathematik und Physik, 1931, 38( 1): 173–198

[23] 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−85

[24] Turing A M. On computable numbers, with an application to the entscheidungsproblem. Proceedings of the London Mathematical Society, 1937, S2−42(1): 230−265

[25] Walsh T. SAT v CSP. In: Proceedings of the 6th International Conference on Principles and Practice of Constraint Programming. 2000, 441−456

[26] Cook S A. The complexity of theorem-proving procedures. In: Proceedings of the 3rd Annual ACM Symposium on Theory of Computing. 1971, 151−158

RIGHTS & PERMISSIONS

The Author(s) 2025. This article is published with open access at link.springer.com and journal.hep.com.cn