The Maximum Satisfiability (MaxSAT) problem is an optimization version of the Propositional Satisfiability (SAT) problem which consists in finding an assignment to the variables of the CNF formula such that the number of unsatisfied (satisfied) clauses is minimized (maximized).
Open-WBO is an open source MaxSAT solver initially based on WBO. Open-WBO implements a variety of algorithms for solving Maximum Satisfiability (MaxSAT) and Pseudo-Boolean (PB) formulas. The algorithms used in Open-WBO are based on a sequence of calls to a SAT solver. Open-WBO can use any MiniSAT-like solver as a black-box. The key novelties of Open-WBO are: (i) incremental MaxSAT solving and (ii) partitioning-based MaxSAT solving. Open-WBO is particularly efficient for partial MaxSAT and has been one of the best solvers in the MaxSAT Evaluations of 2014, 2015, 2016 and 2017.
Open-WBO Team:Authors: Ruben Martins,Vasco Manquinho, Inês Lynce
Contributors: Miguel Neves, Saurabh Joshi, Mikolas Janota
The source code is made available under MiniSAT's original license.