Finding a solution to a satisfiable formula I know that it is as hard to find a solution to a SAT formula, as it is to decide it has a solution at all. See the answer to:
Is finding a solution of a satisfiability problem harder than deciding satisfiability?

Are there also families of formulas for which it is guaranteed that there is a solution, but it is hard to find one?
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.