WPM3: An (in)complete algorithm for weighted partial MaxSAT

Maximum Satisfiability (MaxSAT) has been used to solve efficiently many combinatorial optimization problems. At recent editions of international MaxSAT Evaluation (MSE), the best performing solvers for real world (industrial) problems were those implementing SAT-based algorithms. These algorithms re...

Full description

Saved in:
Bibliographic Details
Published in:Artificial intelligence 2017-09, Vol.250, p.37-57
Main Authors: Ansótegui, Carlos, Gabàs, Joel
Format: Article
Language:English
Subjects:
Algorithms
Boolean algebra
Combinatorial analysis
Computational mathematics
Gold
MaxSAT
Optimization
Optimization algorithms
Pseudo-Boolean
SAT
Solvers
Studies
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:Maximum Satisfiability (MaxSAT) has been used to solve efficiently many combinatorial optimization problems. At recent editions of international MaxSAT Evaluation (MSE), the best performing solvers for real world (industrial) problems were those implementing SAT-based algorithms. These algorithms reformulate the MaxSAT optimization problem into a sequence of SAT decision problems where Pseudo-Boolean (PB) constraints may be introduced. In order to identify the most suitable PB constraints, some algorithms (core-guided) analyze the unsatisfiable cores retrieved from the previous SAT problems in the sequence while refining the lower bound. In this paper, we first conduct a comprehensive study on the complete core-guided algorithms Eva and OLL, that inspired the best performing solvers on industrial instances at MSE-2014. Despite of its apparently different foundations, we show how they are intimately related and identify how to improve them. In this sense, we present our complete core-guided algorithm WPM3. We show how to further exploit the analysis of unsatisfiable cores by being aware of their global structure, i.e., how the cores are interrelated. This is used to encode more efficient PB constraints and enables the algorithm to obtain assignments and refine also the upper bound. Therefore, WPM3 can also work as an incomplete algorithm. At MSE-2015, it showed a competitive performance on industrial instances. It got one out of three gold medals at the complete track and dominated at the incomplete track.
ISSN:0004-3702
1872-7921
DOI:10.1016/j.artint.2017.05.003