# 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

• Containment of recursive Datalog programs in unions of conjunctive queries (Chaudhuri/Vardi 1997). There should also be other logic or database problems that are 2NEXP-complete, but no other specific ones spring to mind. Jan 10 '17 at 22:35
• @AndrásSalamon Thank you for your answer. I didn't find the reference you pointed. All I found was an earlier paper from the authors that state that this problem is 2-EXP-complete (and not 2-NEXP). Am I missing something.?
– wece
Jan 11 '17 at 14:48
• you are right, I misremembered the result: the problem is 2EXP-complete. Jan 17 '17 at 17:13
• I would always write this as N2ExpTime rather than 2NExpTime, since "2" and "Exp" both refer to the value of the upper time bound, while "N" refers to the machine model. It does not seem natural to put the machine model in the middle.
– mak
Feb 3 '17 at 23:32
• Can someone give me the reference for the 2-NEXPTIME-completeness of PCP with a solution of length less than 2^2^n please ? Apr 2 '19 at 15:02

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.