In this paper, by constructing extremely hard examples of CSP (with large domains) and SAT (with long clauses), we prove that such examples cannot be solved without exhaustive search, which is stronger than P $\neq$ NP. This constructive approach for proving impossibility results is very different (and missing) from those currently used in computational complexity theory, but is similar to that used by Kurt G\"{o}del in proving his famous logical impossibility results. Just as shown by G\"{o}del's results that proving formal unprovability is feasible in mathematics, the results of this paper 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 for avoiding exhaustive search. However, in cases of extremely hard examples, exhaustive search may be the only viable option, and proving its necessity becomes more straightforward. Consequently, it makes the separation between SAT (with long clauses) and 3-SAT much easier than that between 3-SAT and 2-SAT. Finally, the main results of this paper demonstrate that the fundamental difference between the syntax and the semantics revealed by G\"{o}del's results also exists in CSP and SAT.

翻译：本文通过构造极其困难的CSP（大值域）和SAT（长子句）实例，证明此类问题无法在避免穷举搜索的情况下求解——这一结论严格强于P≠NP。这种基于构造的不可解性证明方法与当前计算复杂性理论中常用的方法截然不同（且缺失），却与库尔特·哥德尔在证明其著名的逻辑不可解性定理时采用的方法高度相似。正如哥德尔的结果表明在数学中证明形式不可证明性是可行的，本文结果证明：在数学中证明计算困难性并非难事。具体而言，对3-SAT等问题的下界证明之所以具有挑战性，是因为这些问题存在多种规避穷举搜索的有效策略。但面对极端困难实例时，穷举搜索可能是唯一可行途径，此时证明其必要性反而更为直接。这使得SAT（长子句）与3-SAT之间的区分难度远低于3-SAT与2-SAT之间的区分。最后，本文主要结果表明：哥德尔结果揭示的语法与语义之间的根本差异同样存在于CSP和SAT领域。