Modeling and solving Semiring Constraint Satisfaction Problems by transformation to Weighted Semiring Max-SAT

We present a variant of the Weighted Maximum Satisfiability Problem(Weighted Max-SAT), which is a modeling of the Semiring Con- straint Satisfaction framework. We show how to encode a Semiring Con- straint Satisfaction Problem (SCSP) into an instance of a propositional Weighted Max-SAT, and call the encoding Weighted Semiring Max-SAT (WS-Max-SAT). The clauses in our encoding are highly structured and we exploit this feature to develop two algorithms for solving WS-Max- SAT: an incomplete algorithm based on the well-known GSAT algorithm for Max-SAT, and a branch-and-bound algorithm which is complete. Our preliminary experiments show that the translation of SCSP into WS- Max-SAT is feasible, and that our branch-and-bound algorithm performs surprisingly well. We aim in future to combine the natural exible rep- resentation of the SCSP framework with the inherent efficiencies of SAT solvers by adjusting existing SAT solvers to solve WS-Max-SAT.