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 two complementary approaches for solving MaxSAT, namely an unsatisfiability-based algorithm and linear search algorithm. Open-WBO can solve all MaxSAT variants, namely, unweighted MaxSAT, partial MaxSAT, and weighted partial MaxSAT. Moreover, Open-WBO is particularly effective for solving industrial benchmarks and has two main advantages over other state-of-the-art MaxSAT solvers:
Open-WBO uses the most recent techniques for unsatisfiability-based and linear search algorithms. Open-WBO significantly outperforms the old version of WBO and it is competitive with other state-of-the-art MaxSAT solvers. In the current version, it is possible to choose the SAT solver to be used as backend from a pool of 10 SAT solvers.
Open-WBO Team:Authors: Ruben Martins, Vasco Manquinho, Inês Lynce
Contributors: Saurabh Joshi
The source code is made available under MiniSAT's original license.
To contact the authors please send an email to: