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$?