Constructing uniquely satisfiable formulas
If I understand your question correctly, you're looking for ways to generate lots of non-trivial uniquely satisfiable 3SAT instances.
There's a tension between your desire to find a way to generate all uniquely satisfiable instances and your desire to find a way to generate hard uniquely satisfiable instances.  For the moment let's ignore your uniqueness condition. Then I know there has been some work on this problem, e.g., see Generating satisfiable problem instances by Achlioptas, Gomes, Kautz, and Selman.  You might think that they proceed by generating random clauses and discarding the clauses that are inconsistent with a randomly chosen but fixed assignment.  But although this method will in principle generate every satisfiable instance (with some probability), it tends to produce instances that are easy to solve.  To get hard instances, Achlioptas et al. adopt the approach of picking some known hard problem and generating instances based on that.
I suspect that a similar dilemma will arise for uniquely satisfiable instances.  My guess is that a randomized method that generates every uniquely satisfiable instance with some probability will tend to produce easily solved instances.  If you want hard instances, your best bet is probably to pick some cryptographic problem (where the unique solution is the cryptographic secret, e.g., a factorization) and generate instances based on that.