2024-03-28T23:46:01Zhttp://digital.csic.es/dspace-oai/requestoai:digital.csic.es:10261/1554972018-05-28T07:52:49Zcom_10261_60com_10261_4col_10261_313
Exploiting subproblem optimization in SAT-based MaxSAT algorithms
Ansotegui, Carlos
Gabas, Joel
Levy, Jordi
Ministerio de Economía y Competitividad (España)
Satisfiability
Maximum Satisfiability
Constraint optimization
The Maximum Satisfiability (MaxSAT) problem is an optimization variant of the Satisfiability (SAT) problem. Several combinatorial optimization problems can be translated into a MaxSAT formula. Among exact MaxSAT algorithms, SAT-based MaxSAT algorithms are the best performing approaches for real-world problems. We have extended the WPM2 algorithm by adding several improvements. In particular, we show that by solving some subproblems of the original MaxSAT instance we can dramatically increase the efficiency of WPM2. This led WPM2 to achieve the best overall results at the international MaxSAT Evaluation 2013 (MSE13) on industrial instances. Then, we present additional techniques and heuristics to further exploit the information retrieved from the resolution of the subproblems. We exhaustively analyze the impact of each improvement what contributes to our understanding of why they work. This architecture allows to convert exact algorithms into efficient incomplete algorithms. The resulting solver had the best results on industrial instances at the incomplete track of the latest international MSE. © 2015, Springer Science+Business Media New York.
2017-09-22T11:18:31Z
2017-09-22T11:18:31Z
2016
2017-09-22T11:18:31Z
artículo
Journal of Heuristics 22: 1- 53 (2016)
http://hdl.handle.net/10261/155497
10.1007/s10732-015-9300-7
http://dx.doi.org/10.13039/501100003329
eng
Sí
MINECO/TIN2013-48031-C4-4-P
closedAccess
Springer