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?
Small hard 3-SAT instances
complexity theory;satisfiability;3 sat