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. 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 $\neq$ NP。这种证明不可能性结果的构造方法与计算复杂性理论目前所使用的方法非常不同(和缺失),但与Kurt Gödel在证明他著名的逻辑不可能性结果时所使用的方法类似。正如Gödel的结果表明在数学中证明形式不可证明性是可行的一样,本文的结果表明在数学中证明计算难度不难。具体而言,对于许多问题,例如3-SAT,证明下限可能具有挑战性,因为这些问题有多种可用于避免全面搜索的有效策略。然而,在极难的案例中,全面搜索可能是唯一可行的选择,证明其必要性变得更加直接。因此,这篇论文的主要结果表明,Gödel的结果揭示的语法和语义之间的基本差异也存在于CSP和SAT之间。