2-NEXPTIME-complete problems We have a problem and we found an algorithm that appear to be 2-nexptime.

I would like to find known 2-nexptime-complete problems in order to find a lower bound.

I found in literature mainly two such problems:


whether PCP as a solution of size less than $2^{2^n}$
and the tilling problem for a square of size $2^{2^n}$


However I was unable to encode these problems in mine. So I would like to know other 2-NEXPTIME-complete problems, first to have more intuition on this class, and second in the better case prove a lower bound.

I do not provide here the problem on purpose in order to have a broad overview of 2-NEXPTIME.

Thanks
The obvious N2Exp problem is of course the word acceptance problem for 2exp time bounded nondeterministic Turing machines. Using this might be as hard/easy as 2exp tiling, because the simulation of such a Turing machine computation in essence also requires you to define a double-exponentially large grid (2exp many configurations of memory tapes of length 2exp each) that is then filled in a non-deterministic way. In practice, showing N2Exp lower bounds often boils down to constructing such a grid (and making sure that it is not a tree or something else of insufficient structure). The "N" (nondeterminism) is often an inherent part of the problem and not so difficult to get once you have a large enough grid (if not, one would maybe shoot for 2exp at first).

Another practical N2ExpTime-complete problem is reasoning in expressive description logics (DL). In particular, the DL $\mathcal{SROIQ}$ that is underlying the W3C OWL 2 Web Ontology Language standard is N2ExpTime-complete (Yevgeny Kazakov: RIQ and SROIQ Are Harder than SHOIQ. KR 2008: 274-284). Now this is probably not a problem you want to use in reductions, since the definition of the logic is a bit unwieldy because of its many features. The actual lower bound proof for $\mathcal{SROIQ}$ has also been done by reduction to 2-exp tiling. However, depending on your problem, the construction given for $\mathcal{SROIQ}$ could be inspiring to see how to craft such large grids.

The tiling also shows another general pattern: N2Exp really is like NP, you just need to find a way to encode even larger problem instances very efficiently. In principle, you could try to scale up any NP problem. The reason why tiling is nice is that you only need to scale the size of the grid in this case (which is rather uniform).

On the other hand, if your problem is possibly only 2ExpTime-complete, then you could get away with an exponentially space-bounded alternating Turing machine simulation. If you have troubles building a 2exp grid, but you can get to exponential sizes, then this might be worth a try.