Efficient Encodings from CSP into SAT, and from MaxCSP into MaxSAT
Josep Argelich, Alba Cabiscol, Ines Lynce and Felip Manya
We first survey existing encondings from CSP into SAT, and define two new encodings: the minimal support encoding and the interval-based support encoding. Then, we study how the existing and new encodings from CSP into SAT can be extended for encoding MaxCSP into Partial MaxSAT. Finally, we report on the empirical investigation. The obtained results provide empirical evidence of the good performance profile of the new encodings on SAT solvers such as MiniSat and PrecoSAT that incorporate conflict-clause learning, as well as when they are used to encode MaxCSP into Partial MaxSAT and are solved with MaxSAT solvers such as MSUnCore, SAT4J-Maxsat and WMaxSatz.
Keywords: CSP, SAT, MaxCSP, MaxSAT, encoding