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.

翻译：硬搜索问题确实存在