News:

  • 2 January 2015 - Version 1.3.0 released. Includes:
    • The algorithms that won several awards in the MaxSAT Evaluation 2014
    • Incremental MaxSAT algorithms
    • Incremental encodings
  • 9 September 2014 - Paper on incremental MaxSAT solving:
  • 17 July 2014 - Open-WBO is the best unweighted MaxSAT solver in the MaxSAT Evaluation 2014:
    • 1st industrial unweighted MaxSAT
    • 2nd industrial partial MaxSAT

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 source:

    The source code is publicly available and can be easily modified and extended.
  • uses a MiniSAT-like solver as a black box:

    Any MiniSAT-like solver (e.g. Glucose) may be used in Open-WBO. Advances in SAT technology will result in a free improvement in the performance of Open-WBO.

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.

 

If you use Open-WBO in your research work please cite the following paper:

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:


For the old version of WBO, please visit the WBO webpage.

We have also developed a multicore parallel Boolean optimization solver.
For our parallel solver, please visit the PWBO homepage.