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 implies a weaker conclusion 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. The intuition behind this mathematical tractability is that proving exhaustive search for constructed examples avoids handling numerous effective strategies of avoiding exhaustive search that exist for many hard problems such as 3-SAT. Consequently, it makes the separation of lower bounds between SAT (with long clauses) and 3-SAT much easier than that between 3-SAT and 2-SAT.

翻译：本文通过构造极端困难的CSP（大值域）和SAT（长子句）实例，证明此类问题无法在不进行穷举搜索的情况下求解，从而推导出较弱结论P≠NP。这种构造性不可行性证明方法与当前计算复杂性理论中常用的方法截然不同（且尚付阙如），但与库尔特·哥德尔证明其著名逻辑不可判定性定理的方法高度相似。正如哥德尔的结果表明在数学中证明形式不可证明性具有可行性，本文成果展示了在数学中证明计算困难性并非难事。这种数学可处理性背后的直觉在于：针对构造性实例证明穷举搜索必要性时，可规避大量针对3-SAT等困难问题存在的避免穷举搜索的有效策略。因此，这使得（长子句）SAT与3-SAT的下界分离难度远低于3-SAT与2-SAT的分离难度。