Generating Satisfiable Problem Instances

Knowledge Representation and Reasoning

Volume

Proceedings of the AAAI Conference on Artificial Intelligence, 17

Boolean Satisfiability

A major difficulty in evaluating incomplete local-search style algorithms for constraint satisfaction problems is the need for a source of hard problem instances that are guaranteed to be satisfiable. A standard approach to evaluate incomplete search methods has been to use a general problem generator and a complete search method to filter out the unsatisfiable instances. Unfortunately, this approach cannot be used to create problem instances that are beyond the reach of complete search methods. So far, it has proven surprisingly difficult to develop a direct generator for satisfiable instances only. In this paper, we propose the first such generator that outputs uniformly distributed satisfiable problem instances. We also show how one can finely control the hardness of the satisfiable instances by establishing a connection between problem hardness and a new kind of phase transition phenomenon in the space of problem instances. Finally, we use our problem distribution to provide the first conclusive evidence for the existence of an easy-hard-easy pattern in search complexity for local search procedures, analogous to the previously reported pattern for complete search methods.