Solving Many-Valued SAT Encodings with Local Search
Carla Pedro Gomes · 2002
In this paper we present MV-SAT, which is a many-valued constraint programming language that bridges the gap be-tween 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 for-mal 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 comple-tion, graph coloring, all interval series, and sports schedul-ing. 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 es-cape from local minima. Finally, we report on an empirical evaluation that provides experimental evidence of the com-petitiveness of the MV-SAT problem solving approach.