Finding a solution to a satisfiable formula
Absolutely, a hash function is a prime example of a function (which can be modelled by a very complex binary formula of its inputs) where it is easy to find the output given an input, but finding an input which matches an output is very hard.

But since we generated the original output we know that there must be a solution.

This construction requires the ability to forget information (the original input) however.