“Core-Guided MaxSAT With Soft Cardinality Constraints”, 2014 (; backlinks):
Maximum Satisfiability (Max SAT) is a well-known optimization variant of propositional Satisfiability (SAT). Motivated by a growing number of practical applications, recent years have seen the development of different Max SAT algorithms based on iterative SAT solving. Such algorithms perform well on problem instances originating from practical applications.
This paper proposes a new core-guided Max SAT algorithm. This new algorithm builds on the recently proposed unclasp algorithm for ASP optimization problems, but focuses on reusing the encoded cardinality constraints. Moreover, the proposed algorithm also exploits recently proposed weighted optimization techniques.
Experimental results obtained on industrial instances from the most recent Max SAT evaluation, indicate that the proposed algorithm achieves increased robustness and improves overall performance, being capable of solving more instances than state-of-the-art Max SAT solvers.