摘要：Partial maximum Boolean satisfiability (Partial MaxSAT or PMSAT) is an optimization variant of BooleanSatisability (SAT). It asks to find a variable assignment that satisfies all hard clauses and the maximumnumber of soft clauses in a Boolean formula. Several exact PMSAT solvers have been developed sincethe introduction of the MaxSAT evaluations in 2006, based mainly on the Davis- Putnam-Logemann-Loveland (DPLL) procedure and branch and bound (B&B) algorithms. One recent approach that providesan alternative to B&B algorithms is based on unsatisfiable (UNSAT) core identification. All PMSATalgorithms based on UNSAT identification are dependent on two essential external components: (1) acardinality constraint encoder for encoding AtMost-1 constraints into conjunctive normal form (CNF);and (2) a SAT solver. Ensuring the effectiveness of both components directly affects the performance ofthe PMSAT solver. Whereas great advances have been made in PMSAT algorithms based on UNSAT coreidentification, only a few research work has been conducted to understand the in.uence of CNF encodingmethods on the performance of PMSAT solvers. In this paper, we investigate the in.uence of three CNFencoding methods for AtMost-1 constraints on an UNSAT-based PMSAT solver. We implement the solverusing the pairwise, parallel, and sequential encodings, and evaluate its performance on industrial instances.The experimental results show the impact of the CNF encoding method on the performance of the PMSATsolver. Overall, the best results were obtained with the sequential encoding
