Solving Many-Valued SAT Encodings with Local Search

Contents

In this paper we present MV-SAT, which is a many-valued constraint programming language that bridges the gap between Boolean Satisfiability and Constraint Satisfaction. Our overall goal is to extend the SAT formalism with many-valued sets and deal with more compact and natural encodings, as in CSP approaches, while retaining the efficiencies of SAT solvers operating on uniform encodings. After some formal definitions, we first discuss the logical and complexity advantages of MV-SAT compared to SAT and other many-valued problem modeling languages. Second, we define MV-SAT encodings, and analyze their complexity, for a number of combinatorial problems: quasigroup with holes completion, graph coloring, all interval series, and sports scheduling. Third, we describe MV-WalkSAT: a local search strategy adapted from the Boolean WalkSAT procedure that we have implemented and that incorporates several heuristics to escape from local minima. Finally, we report on an empirical evaluation that provides experimental evidence of the competitiveness of the MV-SAT problem solving approach.