TítolImproving 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
Volume7514
EditorSpringer
Conference LocationQuébec, Canada
Paginació86-101
Date Published08/10/2012
Paraules clauMaxSAT
Resum

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.