Sequential Encodings from Max-CSP into Partial Max-SAT

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

• Type: Conference
• Year: 2009
• Where: SAT
• Authors: Josep Argelich, Alba Cabiscol, Inês Lynce, Felip Manyà
• Keywords: Cardinality Constraint, Fewer Clauses, Hardware, SAT 2009, Sequential Sat