Approximation doesn't help, since you can require optimal solutions, but yes, it's very difficult to come up with hard instances. After all, you need to know th

Approximation doesn't help, since you can require optimal solutions, but yes, it's very difficult to come up with hard instances. After all, you need to know the correct answer, so you can't just randomly generate instances. In addition, SAT solvers are ridiculously good these days.