# Confirming existence in polynomial time while solution finding is NP-complete

Assume P≠NP.

Say there's an NP-complete decision problem:

Does $$P$$ have a $$Q$$ ?

And we have a proposition $$F$$ computable in polynomial time, where $$F(P)$$ implies the existence of a solution in the original problem.

My question is:

Is there a "natural" case such that finding $$Q$$ is non-polynomial (maybe NP-hard?) even if $$F(P)$$ is given?

Insight:

Many theorems concerning the existence of a solution of a NP-complete problem is just a polynomial-time algorithm, e.g. Chvatal-Erdos theorem, Ore's condition, Kőnig's theorem on edge-coloring bipartite graphs. I wonder whether all such theorems should be of this kind.

Of course there are counterexamples.

Let $$P$$ be a bunch of statements, and the decision problem is "Does $$P$$ have a true statement ?", and $$F$$ searches for statements with the form $$A$$ and $$¬A$$. Surely, $$F(P)$$ implies the existence of a true statement, but picking out the statement is definitely hard. However, it seems too unnatural.

This paper provides an example about finding Hamilton cycles:$$|d − λ_i | ≤ c \frac{(log log n)^2}{log n(log log log n)}d$$ implies Hamiltonicity, and they provide an algorithm of $$n^{ clnn}$$ time. I'm not sure whether there is a polynomial-time algorithm or not. If there's no such algorithm, finding Hamiltonian cycles in those graphs constitutes a case.