Are there natural separations in the nondeterministic time hierarchy?

Question

The original Nondeterministic Time Hierarchy Theorem is due to Cook (the link is to S. Cook, A hierarchy for nondeterministic time complexity, JCSS 7 343–353, 1973). The theorem states that for any real numbers $r_1$ and $r_2$, if $1 \le r_1 \lt r_2$ then NTIME($n^{r_1}$) is strictly contained in NTIME($n^{r_2}$).

One key part of the proof uses (an unspecified) diagonalization to construct a separating language from the elements of the smaller class. Not only is this a nonconstructive argument, but languages obtained by diagonalization usually provide no insight other than the separation itself.

If we want to understand the structure of the NTIME hierarchy, the following question probably needs to be answered:

Is there a natural language in NTIME($n^{k+1}$) but not in NTIME($n^k$)?

One candidate might be k-ISOLATED SAT, which requires finding a solution to a CNF formula with no other solutions within Hamming distance k. However, proving the lower bound seems is tricky, as usual. It is obvious that checking a Hamming k-ball is clear of potential solutions "should" require $\Omega(n^k)$ different assignments to be checked, but this is by no means easy to prove. (Note: Ryan Williams points out this lower bound for $k$-ISOLATED SAT would actually prove P ≠ NP, so this problem does not seem to be the right candidate.)

Note that the theorem holds unconditionally, regardless of unproved separations such as P vs. NP. An affirmative answer to this question would therefore not resolve P vs. NP, unless it has additional properties like $k$-ISOLATED SAT above. A natural separation of NTIME would perhaps help to illuminate part of the "difficult" behaviour of NP, the part which derives its difficulty from an infinite ascending sequence of hardness.

Since lower bounds are hard, I will accept as an answer natural languages for which we may have a good reason to believe a lower bound, even though there may not yet be a proof. For instance, if this question had been about DTIME, then I would have accepted $f(k)$-CLIQUE, for a non-decreasing function $f(x) \in \Theta(x)$, as a natural language that probably provides the required separations, based on Razborov's and Rossman's circuit lower bounds and the $n^{1-\epsilon}$-inapproximability of CLIQUE.

(Edited to address Kaveh's comment and Ryan's answer.)

Answer 1

As far as I know, we don't know of such languages, or if we do, there is significant controversy about the "naturalness" of them. I know this isn't really a satisfying answer, but I can say:

(a) If you prove an $\Omega(n^k)$ time lower bound for k-ISOLATED SAT for every $k$, then you have actually proved $P \neq NP$.

(b) One way you might hope to show that k-ISOLATED SAT is one of these natural problems in $NTIME[n^{k+1}] - NTIME[n^k]$ is to show that k-ISOLATED SAT problem is hard (in the usual, formal sense of having efficient reductions) for $NTIME[n^k]$. In fact this is the only way we know how to prove such results. But k-ISOLATED SAT is probably not hard in this sense, there are some very unlikely consequences.

The main reason is that k-ISOLATED SAT instances are solvable in $\Sigma_2 TIME[n]$, independently of $k$. You can existentially guess the isolated assignment, then universally verify (for all $O(\log (\sum_{i=1}^k {n \choose i}))$ ways to flip up to $k$ bits in the assignment) that none of the other "local" assignments work.

Here is the proof of part (a). Let ISOLATED SAT be the version of the problem with $k$ given as part of the input (in unary, say). Suppose we prove that ISOLATED SAT requires $\Omega(n^k)$ time for all $k$. If $P=NP$, then $\Sigma_2 TIME[n]$ is in $TIME[n^c]$ for some fixed $c$ (the proof uses an efficient version of Cook's theorem: if there is a SAT algorithm running in time $n^d$, then any $c > d^2$ suffices). But we proved that there is a language in $\Sigma_2 TIME[n]$ that is not in $TIME[n^k]$ for every $k$. This is a contradiction, so $P \neq NP$.

Here is the proof of part (b). If every $L \in NTIME[n^k]$ could be efficiently reduced to a k-ISOLATED SAT formula (e.g., all $n$ bit instances of $L$ get reduced to $k$-ISOLATED SAT formulas of at most $f(k) n^{c}$ size) then $NP=\bigcup_{k} NTIME[n^k] \subseteq \Sigma_2 TIME[n^{c+1}]$. This would immediately imply $coNP \neq NP$, but moreover it just looks very unlikely that all of $NP$ can be simulated so efficiently within the polynomial hierarchy.