Open-WBO

Awards:

  • MaxSAT Evaluation 2017: 2 gold medals, 1 silver medal

  • MaxSAT Evaluation 2016: 1 gold medal, 1 silver medal, 1 bronze medal

  • Pseudo-Boolean Evaluation 2016: 2 silver medals, 2 bronze medals

  • MaxSAT Evaluation 2015: 1 gold medal, 1 silver medal

  • MaxSAT FLoC Olympic Games 2014: 2 gold medals

  • MaxSAT Evaluation 2014: 1 gold medal, 1 silver medal

    • News:

  • 26 October 2017 - Version 2.0 released in Github. Includes:

    • 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.

     

    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: Miguel Neves, Saurabh Joshi, Mikolas Janota

    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.