A Theoretical Comparison of Resolution Proof Systems for CSP Algorithms
Cho Yee Joey Hwang · Summit (Simon Fraser University) · 2004
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. TO my parentsDr. David Mitchell, for introducing me to the field of constraint satisfaction and providing tremendous guidance, support, and feedback at every stage of this thesis work.I would also like to