Unique $k$-SAT benchmarks This question is probably on the border line between on-topic and off-topic, however I've seen similar questions here, therefore I'll ask it.



I'm implementing a Unique $k$-SAT solver, whose input is a $k$-CNF formula having at most $1$ satisfying assignment. To test its practical behaviour, I need a set of such formulas. I've searched for them on the web, and found nothing (while, on the other hand, it is very easy to find suites of ordinary $k$-CNF formulas).


  Where can I find Unique $k$-SAT instances?


Alternatively, I would be content also to know any procedure to generate uniquely satisfiable instances. The only approach I'm aware of goes under the name of planted SAT instance generation: you randomly generate an assignment of $n$ variables, then you generate only those clauses which agree with such assignment. This approach is unsatisfactory for my purposes, for the following reasons:


The obtained formula may have further undesired satisfying assignments.
To be sure that the formula is satisfied uniquely by the desired assignment, you should introduce all the possible clauses that agree with it. This would produce formulas with too many clauses, which will probably be easy to solve and therefore not representative of the worst case behaviour of the solver. It is not obvious to me how we can efficiently force uniqueness while keeping the number of clauses reasonable.



  How can we generate uniquely satisfiable formulas with a reasonable number of clauses? By reasonable I mean far from the maximum $2^k \cdot {n \choose k}$.
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