Exploiting Resolution-based Representations for MaxSAT Solving, SAT 2015


This paper presents Open-WBO, a new MaxSAT solver. Open-WBO has two main features. First, it is an open-source solver that can be easily modified and extended. Most MaxSAT solvers are not available in open-source, making it hard to extend and improve current MaxSAT algorithms. Second, Open-WBO may use any MiniSAT-like solver as the underlying SAT solver. As many other MaxSAT solvers, Open-WBO relies on successive calls to a SAT solver. Even though new techniques are proposed for SAT solvers every year, for many MaxSAT solvers it is hard to change the underlying SAT solver. With Open-WBO, advances in SAT technology will result in a free improvement in the performance of the solver. In addition, the paper uses OPEN-WBO to evaluate the impact of using different SAT solvers in the performance of MaxSAT algorithms

International Conference on Theory and Applications of Satisfiability Testing, Springer.