SAT Requires Exhaustive Search

要約

この論文では、CSP (ドメインが大きい) と SAT (句が長い) の非常に難しい例を構築することにより、このような例は P $\neq$ NP よりも強力な徹底的な検索なしでは解決できないことを証明します。
不可能性の結果を証明するためのこの建設的なアプローチは、計算複雑性理論で現在使用されているものとは大きく異なります (そして欠落しています) が、Kurt G\'{o}del が有名な論理的不可能性の結果を証明する際に使用したものと似ています。
形式的証明不可能性の証明が数学において実現可能であることを G\'{o}del の結果が示したように、この論文の結果は、数学において計算の困難さを証明することが難しくないことを示しています。
特に、3-SAT などの多くの問題の下限を証明することは、これらの問題には徹底的な探索を回避するために利用できるさまざまな効果的な戦略があるため、困難な場合があります。
ただし、非常に困難な例の場合は、徹底的な検索が唯一の実行可能なオプションである可能性があり、その必要性を証明するのがより簡単になります。
その結果、SAT (長い節を含む) と 3-SAT の間の分離は、3-SAT と 2-SAT の間の分離よりもはるかに簡単になります。
最後に、この論文の主な結果は、G\'{o}del の結果によって明らかにされた構文とセマンティクスの間の根本的な違いが 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\'{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.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google