TitleImproving SAT-Based Weighted MaxSAT Solvers
Publication TypeConference Paper
Year of Publication2012
AuthorsAnsótegui C, Bonet MLuisa, Gabàs J, Levy J
EditorMilano M
Conference NameProc. of the 18th Int. Conf. on Principles and Practice of Constraint Programming, CP'12
Conference LocationQuébec, Canada
Date Published08/10/2012

In the last few years, there has been a significant effort in designing and developing efficient Weighted MaxSAT solvers. We study in detail the WPM1 algorithm identifying some weaknesses and proposing solutions to mitigate them. Basically, WPM1 is based on iteratively calling a SAT solver and adding blocking variables and cardinality constraints to relax the unsatisfiable cores returned by the SAT solver. We firstly identify and study how to break the symmetries introduced by the blocking variables and cardinality constraints. Secondly, we study how to prioritize the discovery of higher quality cores. We present an extensive experimental investigation comparing the new algorithm with state-of-the-art solvers showing that our approach makes WPM1 much more competitive.