harrisj: Thanks for the bouquet. It's only because I happen to be good at remembering this esoteric excreta.
You mentioned verification in P-time, and I think it's worth exploring what that means. One technical definition of the class NP is:
NP is the class of decision problems (languages) L such that there is a polynomial time function f(x,c) where x is a string, c is another string whose size is polynomial in the size of x, and f(x, c)=True if and only if x is in L.
(taken from the comp.theory FAQ)
As an example, x might be a graph, c might be a path in that graph, and f(x, c) is the function "is c a Hamiltonian path in the graph x?"
There are at least three kinds of questions that you may want to ask about this problem, given x. They are:
- Is x in L, that is, does there exist c such that f(x, c)=True? That question corresponds to "does the graph have a Hamiltonian cycle"? Or "is the number composite"? This is called a "decision problem", and is not necessarily verifiable in P (unless P=NP, of course), because verifying an answer is identical to finding the answer.
- Given x, give me a c which proves that x is in L. This kind of problem is trivially certifiable in P, because all you need to do is take the certificate c and compute the value of f(x, c). This question corresponds to "find me a Hamiltonian cycle in this graph", or "find me factors of this number".
- Given x, find me the certificate c which minimises (or maximises) some cost function cost(c). This is called an "NP optimisation problem", and corresponds to something like "find me the Hamiltonian cycle of minimal distance" (i.e. the travelling salesman problem). I don't know whether this kind of problem is certifiable in P or not. Could someone please let me know?
Now to EXPTIME. EXPTIME-hard problems are not certifiable in P-time if the certificate is polynomial in the size of the input. If they were, you could construct a nondeterministic polynomial algorithm to solve them. (Nondeterministically guess the certificate in NP time then test it in P time.) So I guess EXPTIME-hard public-key systems and zero-knowledge proof systema aren't feasable. Darn.
If the certificate were not polynomial in the size of the input, that might be a different matter. That is, certifying EXPTIME-hard problems might be polynomial in the size of the certificate. I'm not sure about that one.
EXPTIME-hard problems often turn up when dealing with logic and theorem proving (e.g. constraint systems, conditional logic) or formal languages and the machines which generate/recognise them (e.g. tree automata). Here are some example EXPTIME-complete problems:
- Evaluation of datalog queries for single rule programs containing only a single clause.
- For tree automata, the intersection problem (i.e. given two tree automata, is the intersection of their languages empty) and equivalence problem (do two given tree automata accept the same language)
- Removing recursion from formulas in the mu calculus (i.e. given a recursive formula, give me a non-recursive equivalent if it exists)
- Satisfiability for definite set constraints
- Determining a winning strategy for chess generalised to an N*N board or go generalised to an N*N board. I'm not entirely sure how you generalise chess piece movement, but there you go.
And just for fun, here are a couple of NEXPTIME-complete problems:
- Satisfiability for two-variable first-order logic.
- Provability in first-order multiplicative additive linear logic
Naturally, NEXPTIME-complete problems are certifiable in EXPTIME.
Happy theory nerding.