Is embedding a solution feasible for SAT? I am interested in "hard" individual instances of NP-complete problems.

Ryan Williams discussed the SAT0 problem at Richard Lipton's blog.  SAT0 asks whether a SAT instance has the specific solution consisting of all 0's.  This got me thinking about constructing SAT instances that are likely to be "hard".

Consider a SAT instance $\phi$ with $m$ clauses and $n$ variables, where $\alpha = m/n$ is "large enough", in the sense that it falls into the region beyond the phase transition, where nearly all instances are unsatisfiable.  Let $x$ be a random assignment to the values of $\phi$.


  Is it possible to modify $\phi$ to obtain a new instance $\phi|x$, so that $\phi|x$ is "largely similar" to $\phi$, but so that $x$ is a satisfying assigment for $\phi|x$?


For instance, one could try to add to each clause a randomly chosen literal from the solution, that does not already occur in the clause.  This will guarantee that $x$ is a solution.

Or is this hopeless, leading to a fast algorithm for finding the "hidden" solution, along the lines of the following recent paper?


Uriel Feige and Dorit Ron, Finding hidden cliques in linear time, DMTCS proc. AM, 2010, 189–204.


I am aware of the discussion by Cook and Mitchell and work they reference.  However, I couldn't find anything about what happens to the structure of a formula when one tries to explicitly embed a satisfying assignment into it.  If this is folklore, pointers would be very welcome!


Stephen A. Cook and David G. Mitchell, Finding Hard Instances of the Satisfiability Problem: A Survey, DIMACS Series in Discrete Mathematics and Theoretical Computer Science 35 1–17, AMS, ISBN 0-8218-0479-0, 1997. (PS)
You can take any formula $\varphi$ and change it to the formula $\varphi \vee \psi_x$ where $\psi_x$ is a "hard" SAT instance whose only solution is $x$. One way to construct such a formula is using cryptography:  if $f:\{0,1\}^n\rightarrow \{0,1\}^n$ is a one-way permutation and we choose $x$ at random and set $y=f(x)$, then one can convert $y$ into a SAT formula such that $x$ is its only solution and thus finding $x$ corresponds to inverting $f$. (We need for this $x$ to be random, but this something similar is anyway assumed if we think finding $x$ should be hard.)