M.: Boosting Weighted CSP Resolution with Shared BDDs

Abstract. We present a new approach for solving Weighted Constraint Satisfaction Problems (WCSP). The method is based on encoding the violation cost of soft constraints as a pseudo-Boolean objective function, and successively calling a decision procedure bounding the maximum al-lowable cost. The novelty of our approach consists in building a Binary Decision Diagram (BDD) for the objective function, using state-of-the-art generalized arc-consistent SAT encodings for it. Moreover, with our approach we maximize the reuse of the BDDs for the objective function between successive calls to the decision procedure by creating a shared BDD. The method has been incorporated into the WCSP solving system WSimply, based on reformulation into SMT, with preliminary encourag-ing results.