Unique $k$-SAT benchmarks

Question

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}$.

Answer 1

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>1 \land y>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

Answer 2

You might consider the algorithms that are used for generating Sudoku puzzles - presumably generalized to $n \times n$ - since (usually) Sudoku puzzles are supposed to have a unique solution. On the other hand, Sudoku puzzles are also usually guaranteed to have at least one solution... But finding that solution could still be a good benchmark for your solver.

You might use a Sudoku-generator together with a reduction to SAT, or you might think about how to apply the techniques used in Sudoku generation to more directly generate Unique SAT instances. For the former, obviously your SAT instances will have some structure, but it's unclear to me whether it's more or less structure than e.g. planting a solution or using the witness isolation technique. Probably depends on your needs and your solver.

The one reference I know of here is: Sudoku Puzzles Generating: from Easy to Evil.

Answer 3

I think a good test case would be to generate random uniquely satisfiable 3XOR instances (planted instances) with $\Theta(n)$ constraints and then convert them to 3SAT instances.

Answer 4

imho one of the best ways to create "presumably hard" SAT instances while controlling the number of solutions is from integer factoring instances/circuits encoded in binary. the code is not very complex, it uses mainly EE addition circuits, and does not lead to "large" SAT instances. the number of solutions is equal to the number of factors (including "permutations" of the factors). therefore prime numbers generate exactly two solutions, $(1,p),(p,1)$. a single solution can be guaranteed with a further "comparison" constraint that restricts the factors to $a<b$ or that $a \neq 1$ or $b \neq p$.

also with this approach is it is relatively easy to find numbers with roughly however many factors/solutions are desired. the "smoother" the number, the more factors.

various researchers over the years have created this factoring SAT code (eg for DIMACS competition/arcihve which has stored some factoring instances in the past) but unfortunately there does not seem to be a publicly available version. see also the 1st link below for a ref where the code was written/implemented apparently for a graduate course.

• Reducing the integer factorization problem to an NP-Complete problem
• Generating 3SAT circuit for Integer factorization example

another empirical/iterative approach that may be useful for some, to create more "unstructured" instances: create random SAT instances $e_n$ near the transition point (the region where the equation has a probability 50% between "solvable and unsolvable"), and then solve the equation. if it is unsolvable, throw away and restart. if it is solvable, add clauses that restrict the solution "not" to be the found solution, obtaining $e_{n+1}$, and re-solve. repeat if necessary. when the equation $e_{n+1}$ is no longer solvable, the $e_n$ must have had a single/unique solution.

Answer 5

You can easily generate directly Unique SAT formulas with reasonable size $(|F|<n+2^k)$

Let $m$ be the unique model - say $m$ contains only "0"s (rename the variables later if needed).
Let $F$ a $k$-SAT formula satisfied only by $m$ - the maximum size of $F$ is the total number of clauses satisfied by $m$ i.e. $(2^k-1) \binom{n}{k}$.

Take the $\binom{k}{1}$ clauses that eliminate all models assigning exactly one "1" among $x_1,x_2 \ldots x_k$:
$(\lnot x_1, x_2 \ldots x_k)(x_1, \lnot x_2 \ldots x_k)\ldots (x_1,x_2 \ldots \lnot x_k)$

Take the $\binom{k}{2}$ clauses that eliminate all models assigning exactly two "1" among $x_1,x_2 \ldots x_k$:
$(\lnot x_1, \lnot x_2, x_3 \ldots x_k)(\lnot x_1,x_2, \lnot x_3 \ldots x_k)\ldots (x_1,x_2 \ldots \lnot x_{k-1} \lnot x_k)$

Keep going until taking the only $\binom{k}{k}$ clause that eliminates all models assigning "1" to each variables among $x_1,x_2 \ldots x_k$.

The only models which are not yet eliminated assign all $x_1,x_2 \ldots x_k$ to "0". Since $m$ is a model, then take any set of $n-k$ clauses that eliminate all models assigning "1" to $x_i (k<i\leq n)$ and $0$ to any $k-1$ variables among $x_1,x_2 \ldots x_k$, for instance:
$(\lnot x_{k+1}, x_1 \ldots, x_{k-1}) \ldots (\lnot x_n, x_1 \ldots x_{k-1})$.

Then $|F|=\sum_{i=1}^k \binom{k}{i} +n-k = 2^k-1+n-k$

To get more clauses, add any clause containing at least one negated variable. To get an unsatisfiable formula, just add a clause with $k$ unnegated variables.