The resolution complexity of constraint satisfaction

Constraint satisfaction provides a uniform framework for addressing a variety of combinatorial problems. Propositional proof complexity is the study of the minimum lengths of proofs in propositional logic. We view constraint satisfaction problems (CSPs) as generalizing propositional satisfiability, and adapt ideas from resolution proof complexity to their study. We study a previously defined resolution-like proof system for CSPs, denoted here NG-RES, and a new system C-RES. NG-RES is very natural, but C-RES is more powerful, and is equivalent to propositional resolution for CSPs equivalent to SAT.; We examine CSP algorithms that employ standard techniques from the literature, and show they are resolution-based. They implicitly construct NG-RES or C-RES proofs. We also give resolution-based algorithms for binary CSPs with non-trivial upper bounds. For domain size d, we construct C-RES proofs in time O([ d/2]n), and for domain size 3 we obtain O(1.38027n), which is close to the best algorithmic upper bound.; For resolution-based algorithms, minimum resolution proof size is a lower bound on running time. We demonstrate there are many CSP instances for which the shortest C-RES proof is of exponential size: Any k-CNF formula which is hard for propositional resolution induces two families of CSP instances which are hard for C-RES, one with domain size k and binary constraints, and one with domain size two and k-ary constraints.; Based on a known relationship between clause size and refutation length for propositional resolution, we reduce C-RES length to the “sub-critical expansion” of CSP instances. We use this to obtain C-RES lower bounds for random CSPs. Known exponential resolution lower bounds for random instances of k-SAT are seen to imply lower bounds for equivalent random CSPs. For a more general family of random CSPs, we obtain exponential C-RES lower bounds when constraints are “loose”. Our results generalize those implied via random k-SAT in two respects: they apply to binary CSPs, and they hold for constraints which are “tighter” than propositional clauses.; We also demonstrate a width-length relationship for NG-RES. This implies that tree-NG-RES is quasi-automatizable, and may lead to an improved separation between NG-RES and RES.