SAT需要穷举搜索
SAT Requires Exhaustive Search
AI总结：
本文通过构造CSP和SAT的极难实例，证明此类实例必须依赖穷举搜索，从而得到强于P≠NP的结论，并揭示语法与语义的根本差异同样存在于CSP和SAT中。
摘要：
在本文中，通过构造CSP（具有大域）和SAT（具有长子句）的极难实例，我们证明了此类实例无法在不进行穷举搜索的情况下求解，这一结论强于P≠NP。这种用于证明不可能性结果的构造性方法与计算复杂性理论中当前使用的方法截然不同（且一直缺失），但与库尔特·哥德尔在证明其著名的逻辑不可能性结果时所使用的方法相似。正如哥德尔的结果所表明的那样，在数学中证明形式不可证明性是可行的，本文的结果表明，在数学中证明计算困难性并不困难。具体而言，证明许多问题（如3-SAT）的下界可能具有挑战性，因为这些问题具有各种可用于避免穷举搜索的有效策略。然而，在极难实例的情况下，穷举搜索可能是唯一可行的选择，而证明其必要性则变得更加直接。因此，这使得SAT（具有长子句）与3-SAT之间的分离比3-SAT与2-SAT之间的分离容易得多。最后，本文的主要结果表明，哥德尔的结果所揭示的语法与语义之间的根本差异也存在于CSP和SAT中。
英文摘要：
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ödel in proving his famous logical impossibility results. Just as shown by Gö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ödel's results also exists in CSP and SAT.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
