Optimal refutations for constraint satisfaction problems

Variable ordering heuristics have long been an important component of constraint satisfaction search algorithms. In this paper we study the behaviour of standard variable ordering heuristics when searching an insoluble (sub)problem. We employ the notion of an optimal refutation of an insoluble (sub)problem and describe an algorithm for obtaining it. We propose a novel approach to empirically looking at problem hardness and typical-case complexity by comparing optimal refutations with those generated by standard search heuristics. It is clear from our analysis that the standard variable orderings used to solve CSP s behave very differently on real-world problems than on random problems of comparable size. Our work introduces a potentially useful tool for analysing the causes of the heavy-tailed phenomenon observed in the runtime distributions of backtrack search procedures. This material is based on work supported by Science Foundation Ireland under Grant 00/PI.1/C075. We would like to thank Barbara M. Smith, Eugene C. Freuder, Nic Wilson, Chris Beck, Bart Selman, Carla Gomes and Susan Epstein for their comments and suggestions, and to John Morrison and the Boole Centre For Research in Informatics for providing access to their Beowulf cluster.