Optimal Refutations for Constraint Satisfaction Problems

Abstract

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 CSPs 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.