Sequential Encodings from Max-CSP into Partial Max-SAT

摘要

We define new encodings from Max-CSP into Partial Max-SAT which are obtained by modelling the at-most-one condition with the sequential SAT encoding of the cardinality constraint ≤ 1(x_1, ..., x_n). They have fewer clauses than the existing encodings, and the experimental results indicate that they have a better performance profile.