SAT Requires Exhaustive Search

TL;DR

This paper constructs extremely hard CSP and SAT instances to demonstrate that solving them requires exhaustive search, providing a new approach to proving computational hardness that parallels G"odel's logical impossibility results.

Contribution

It introduces a constructive method to prove that certain CSP and SAT instances cannot be solved without exhaustive search, surpassing traditional complexity theory techniques.

Findings

Hard CSP and SAT instances require exhaustive search to solve.

Proving computational hardness can be as straightforward as G"odel's logical impossibility proofs.

Separation between SAT variants is clarified through these hard instances.

Abstract

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.