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
(taken from the
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
There are at least three kinds of questions that
you may want to ask about this problem, given x.
- 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
- 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
- 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
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.
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
- 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
- Satisfiability for two-variable first-order logic.
- Provability in first-order multiplicative additive
Naturally, NEXPTIME-complete problems are certifiable in
Happy theory nerding.