  We propose to use local search algorithms to produce SAT instances which are
harder to solve than randomly generated k-CNF formulae. The first results,
obtained with rudimentary search algorithms, show that the approach deserves
further study. It could be used as a test of robustness for SAT solvers, and
could help to investigate how branching heuristics, learning strategies, and
other aspects of solvers impact there robustness.
