# Small hard 3-SAT instances

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?

• Hard for what purpose? Small instance are easily brute-forced. – Raphael Jun 14 '16 at 9:34
• Yes... I suppose what I mean is non-trivial instead of hard. For example, given a 15 clause problem, would it take more effort to solve a problem with 3, 4, 5, 6 etc. variables? The purpose being to test small scale instances for a new algorithm and scale up later – SamTheTomato Jun 16 '16 at 0:21

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.