@conference {4880, title = {Improving SAT-Based Weighted MaxSAT Solvers}, booktitle = {Proc. of the 18th Int. Conf. on Principles and Practice of Constraint Programming, CP{\textquoteright}12}, volume = {7514}, year = {2012}, month = {08/10/2012}, pages = {86-101}, publisher = {Springer}, organization = {Springer}, address = {Qu{\'e}bec, Canada}, abstract = {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.}, keywords = {MaxSAT}, author = {Carlos Ans{\'o}tegui and Mar{\'\i}a Luisa Bonet and Joel Gab{\`a}s and Jordi Levy}, editor = {Michela Milano} }