Old techniques in new ways: Clause weighting, unit propagation and hybridization for maximum satisfiability

摘要

Maximum Satisfiability (MaxSAT) is a basic and important constraint optimization problem. When dealing with both hard and soft constraints, the MaxSAT problem is referred to as Partial MaxSAT, which has been used to effectively solve many combinatorial optimization problems in real world. The local search method and the SAT-based method are two popular methods for Partial MaxSAT. Nevertheless, local search algorithms have been dominated by SAT-based algorithms on industrial benchmarks. This work develops an effective local search algorithm for industrial benchmarks, which for the first time is competitive with SAT-based algorithms on industrial MaxSAT benchmarks.