# A canonical complete problem for EXP and NEXP in terms of formulae

3SAT is a complete problem for NP. TQBF is a complete problem for PSPACE.

Is there direct way to define canonical complete problems for EXP and NEXP in terms of boolean formulae? I have only seen examples in terms of bounded halting problem, games and succinct formulation of problems in various classes within P and PSPACE.

• An option would be exponential sized formulae (eg 3SAT with exponential number of clauses), but this breaks down when we want polynomial reductions. This is why we resort to succinct representation of formulae and the like. – VigneshM Sep 25 '19 at 22:57
• What is wrong with games and succinct problems? – Sasho Nikolov Sep 26 '19 at 1:58
• Do you not allow succinct 3-SAT? Did you look at this: cstheory.stackexchange.com/a/3307/969? – Huck Bennett Sep 26 '19 at 2:58
• @VigneshM: maybe you meant SAT instead of 3SAT? (With 3SAT, if you have n variables, you can have at most $O(n^3)$ clauses, not exponentially many.) – Joshua Grochow Sep 26 '19 at 5:00
• An NEXP-complete problem in terms of second-order quantified Bolean formulas is given in cstheory.stackexchange.com/questions/44231 and the ensuing commments. – Emil Jeřábek Sep 26 '19 at 7:46