Is the Witness Size of Membership for Every NP Language Already Known? The question occurred to me when I get Dana Moshkovitz answer to another topic.

Let $L$ be an NP Language, and let $R_L$ be the respective NP relation. We know that there exists some polynomial $p$ such that:

$\forall x \in L, \\, \exists w \in \\{0,1\\}^{p(|x|)} \quad (x,w) \in R_L$

The above statement only requires the existence of such $p$, but it does not force it to be explicitly determined. In contrast, for every NP language I know, $p$ is already known:


For SAT, the size of witness is equal to the number of atoms appearing in the formula.
For Hamiltonicity, the size of witness is $O(|V|)$, where $V$ is the vertex set.
For Graph 3-Coloring, the size of witness is $O(|V|)$, where $V$ is the vertex set.



  Does there exist an NP language (even an artificial one), for which we know there exist some polynomial $p$ bounding the size of witness, yet we cannot explicitly determine $p$?
If you don't mind artificial languages, we can construct such problems using pretty much any number k whose value is unknown to mathematicians. For example, we don't know the value of R(5,5) (the fifth Ramsey number), or the size of the largest excluded minor of the family of knotless graphs (this number is finite due to the Robertson-Seymour theorem), or the value of BB(10), where BB() stands for the Busy Beaver function. Let k equal any of these numbers. We know that k is finite, but we don't know the value of k.

Now construct some problem in NP where the witness is of size $O(n^k)$. Off the top of my head I can't think of a nice way of doing this, but here's one way. Let the input be a succinct description of a graph. Since the description size is n, the graph is on exponentially many vertices. (For example, maybe the input is a circuit that accepts two inputs x and y and tells you if (x,y) is an edge in the graph.) The question is to determine if the graph contains a path of length $n^k$. This problem is in NP because the prover can send the list of vertices on the path in order, which the verifier can check. The size of the witness is $n^k$.