  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.
