Small hard 3-SAT instances

Question

I have read various references that for 3-SAT instances with large numbers of clauses, the optimal clause/variable ratio to generate 'difficult' instances is around 4.

However, I would like to know if there is a similar result in the case for the number of clauses is small. For example, for < 20 clauses?

For example, if you had 8 clauses and you took a clause/variable ratio of 4, then you would have 2 variables, but this would be quite trivial to solve.

Do there exist heuristics for generating difficult small instances, or is it a simple matter of testing to see what works?

Answer 1

If the number of clauses is very small, then there's no clause/variable ratio that makes 3-SAT hard. 3-SAT with < 20 clauses is easy. It's asymptotically easy (technically, the running time is $O(1)$) and easy in practice (using off-the-shelf SAT solvers).

One way to derive hard instances is based upon cryptography, where you convert the problem "find a value $x$ whose SHA256 hash starts with 128 zeros" to SAT, or "find a 128-bit AES key $k$ that encrypts a fixed 128-bit string to another fixed 128-bit string". However, these are still going to have thousands of variables and tens of thousands of clauses, at minimum.