A Theoretical Comparison of Resolution Proof Systems for CSP Algorithms

Many problems from a variety of applications such as graph coloring and circuit design can be modelled as constraint satisfaction problems (CSPs). This provides strong motivation to develop effective algorithms for CSPs. In this thesis, we study two resolution-based proof systems, NG-RES and C-RES, for finite-domain CSPs which have a close connection to common CSP algorithms. We give an almost complete characterization of the relative power among the systems and their restricted tree-like variants. We demonstrate an exponential separation between NG-RES and C-RES, improving on the previous super-polynomial separation, and present other new separations and simulations. We also show that most of the separations are nearly optimal. One immediate consequence of our results is that simple backtracking with 2-way branching is exponentially more powerful than simple backtracking with d-way branching.