Resolution and constraint satisfaction

Abstract

We study two resolution-like refutation systems for finitedomain constraint satisfaction problems, and the efficiency of these and of common CSP algorithms. By comparing the relative strength of these systems, we show that for instances with domain size d, backtracking with 2-way branching is super-polynomially more powerful than back-tracking with d-way branching. We compare these systems with prepositional resolution, and show that every family of CNF formulas which are hard for prepositional resolution induces families of CSP instances that are hard for most of the standard CSP algorithms in the literature. © Springer-Verlag 2003.