Local consistency in weighted CSPs and inference in Max-SAT

Abstract

Weighted constraint satisfaction problems (WCSP) and Max-SAT are optimization versions of the CSP framework and SAT repectively. They have many practical applications. Most current state-of-the-art complete solvers for WCSP and Max-SAT problems can be described as a basic depth-first branch and bound search that computes a lower bound during the search that can be used together with the cost of the best solution found in order to prune entire search subtrees. Recently, a collection of local consistency properties such as NC*, AC*, DAC*, FDAC* and EDAC* have been proposed for WCSP in order to simplify the problem. In Max-SAT we have recently proposed inference rules to detect unfeasible assignments. Resolution in Max-SAT is an extension of classical resolution for the SAT problem: (x ∨ A, u), (x̄ ∨ B, w) ⇒ {(A ∨ B, m) (x ∨ A, u Θ m) (x̄ ∨ B, w Θ m), (x ∨ A ∨ B̄, m) (x̄ ∨ Ā ∨ B, m) where A and B are arbitrary disjunctions of literals and m = min{u, w}. We use the notation [P,⋯,Q] ⇒ [R,⋯, S], where P, Q,⋯ are weighted clauses. It means that if there are some weighted clauses matching with [R,⋯, Q] (left side). they can be replaced by [R,⋯, S] (right side). We define the neighborhod resolution rule (NRES) as RES restricted to the A = B case. We also present the novel weighted modus ponens rule (MP) as: (x ∨ y, u), (x̄, w) ⇒ {(y, m) (x ∨ y, u Θ m) x̄, w Θ m) (x̄, ∨ ȳ, m) where m = min(u, w}. It is important to realize that this rule can be obtained by replacing B = false and y = A in the generic resolution rule (RES). Finally, we are studying the relation between the inference rules and the local consistency properties. For example, given an extension of the DPLL algorihtm for Max-SAT if it applies NRES0 rule at each node of the search tree then it enforces the NC* property. If DPLL applies both NRES0 and NRES1 at each node, it enforces AC*. NRESk denote NRES restricted to |A| = k with k >= 0. We present the equivalence of the other local consistency properties for WCSP w.r.t. the new inference rules for Max-SAT. © Springer-Verlag Berlin Heidelberg 2005.