Finding hard instances of the satisfiability problem: A survey
Stephen Cook, David G. M. Mitchell · DIMACS series in discrete mathematics and theoretical computer science · 1997
. Finding sets of hard instances of propositional satisfiability is of interest for understanding the complexity of SAT, and for experimentally evaluating SAT algorithms. In discussing this we consider the performance of the most popular SAT algorithms on random problems, the theory of average case complexity, the threshold phenomenon, known lower bounds for certain classes of algorithms, and the problem of generating hard instances with solutions.