Unique $k$-SAT benchmarks
Here is one way to generate a Unique $k$-SAT instance, given a SAT instance $\varphi$ that you know is satisfiable.  Consider the formula $\psi(x)$ given by

$$\varphi(x) \land h(x)=y,$$

where $h$ is a hash function that maps an assignment $x$ to a $k$-bit value (for some small value of $k$), and $y$ is a random $k$-bit value.  If $\varphi$ has about $2^k$ satisfying assignments, then (heuristically) we assume that $\psi$ will have exactly one satisfying assignment (with constant probability).  We can test whether this is the case using a SAT solver (namely, test whether $\psi$ is satisfiable; if it is, and $x_0$ is one satisfying assignment, test whether $\psi(x) \land x \ne x_0$ is satisfiable).  If $k$ is not known, you can find $k$ using binary search or just by iterating over each candidate value $k=1,2,\dots,n$ (where $n$ is the number of boolean variables in $x$).

You can choose the hash function freely.  You'll probably want to make it as simple as possible.  One extremely simple construction is to have $h$ pick out a random subset of $k$ bits from $x$.  A slightly more sophisticated construction is to have the $i$th bit of $h(x)$ be the xor of two randomly chosen bits from $x$ (choosing a separate pair of bit positions for each $i$, independently).  Keeping $h$ simple will keep $\psi$ relatively simple.

This kind of transformation is sometimes used/suggested, as part of a scheme for estimating the number of satisfying assignments to a formula $\varphi$; I've adapted it for your particular need.

You can find many testbeds of SAT instances on the Internet, and you could apply this transformation to all of them, to obtain a collection of Unique $k$-SAT instances.



Another possibility would be to generate Unique $k$-SAT instances from cryptography.  For instance, suppose $f:\{0,1\}^n \to \{0,1\}^n$ is a cryptographic one-way permutation.  Let $x$ be a randomly chosen element of $\{0,1\}^n$, and let $y=f(x)$.  Then the formula $\varphi(x)$ given by $f(x)=y$ is a Unique $k$-SAT instance.  As another example, pick two large prime numbers $p,q$ randomly, and let $n=pq$.  Then the formula $\varphi(x,y)$ given by $x \cdot y = n \land x&gt;1 \land y&gt;1 \land x \le y$ (with the obvious correspondence between bit-strings and integers) is a Unique $k$-SAT instance.  However, these constructions do not seem like a useful way to benchmark or optimize your solver.  They all have a special structure, and there is no reason to believe that this structure is representative of real-world problems.  In particular, SAT instances drawn from cryptographic problems are known to be extremely hard, much harder than SAT instances drawn from many other real-world applications of SAT solvers, so they aren't a very good basis for benchmarking your solver.



In general, all of the techniques mentioned in this answer have the drawback that they generate Unique $k$-SAT instances with a particular structure, so they might not be what you are looking for -- or, at least, you might not want to rely solely upon formulae generated in this way.  A better approach would be to identify applications of Unique $k$-SAT (who do you think is going to use your solver, and for what purpose?), and then try to obtain some realistic examples from those application domains.

For a related topic, see also Generating interesting combinatorial optimization problems