Resolution in Max-SAT and its relation to local consistency in weighted CSPs

Max-SAT is an optimization version of the well-known SAT problem. It is of great importance from both a theoretical and a practical point of view. In recent years, there has been considerable interest in finding efficient solving techniques [Alsinet et al., 2003; Xing and Zhang, 2004; Shen and Zhang, 2004; de Givry et al., 2003]. Most of this work focus on the computation of good quality lower bounds to be used within a branch and bound algorithm. Unfortunately, lower bounds are described in a procedural way. Because of that, it is difficult to realize the logic that is behind. In this paper we introduce a logical framework for Max-SAT solving. Using this framework, we introduce an extension of the Davis-Putnam algorithm (that we call Max-DPLL) and the resolution rule. Our framework has the advantage of nicely integrating branch and bound concepts such as the lower and upper bound, as well as hiding away implementation details. We show that Max-DPLL augmented with a restricted form of resolution at each branching point is an effective solving strategy. We also show that the resulting algorithm is closely related with some local consistency properties developed for weighted constraint satisfaction problems.