Improved Algorithm of Unsatisfiability-based Maximum Satisfiability.

Recently, the Maximum Satisfiability (MaxSAT) discovers a rapidly increasing number of practical applications in a wide range of different areas. Unsatisfiability-based MaxSAT algorithms have been put forward aimed at improving the performance of solving MaxSAT problem. In these algorithms, several excellent Boolean Satisfiability (SAT) solvers are employed to iteratively identify unsatisfiable sub-formulas and the additional blocking variables are also applied to relax some of initial clauses or encode Boolean constraints into a CNF formula. Firstly, this paper proposes two novel optimizations to reduce the search space: finding all disjoint unsatisfiable cores with the original clauses removed and no blocking variables added; avoiding generating the largest number of blocking variables’ clauses with heuristic strategy. Moreover, in order to reduce the number of satisfying iterations, the partial assignment is introduced into satisfiability-based framework as the tight bound accelerator which could find a smaller number of blocking variables. Experimental results show that the unsatisfiability-based algorithm with these optimizations results in an improved and more effective solver for MaxSAT problem than previous algorithms. In addition,this results in consistent performance gains in most cases and on average 1.5 times speed-up for MaxSAT with state-of-the-art algorithms.