maxsat is an optimization version of satisfiability. Since many practical problems involve optimization, there are a wide range of potential applications for effective maxsat solvers. In this paper we present an extensive empirical evaluation of a number of maxsat solvers. In addition to traditional maxsat solvers, we also evaluate the use of a state-of-the-art Mixed Integer Program (mip) solver, cplex, for solving maxsat. mip solvers are the most popular technology for solving optimization problems and are also theoretically more powerful than sat solvers. In fact, we show that cplex is quite effective on a range of maxsat instances. Based on these observations we extend a previously developed hybrid approach for solving maxsat, that utilizes both a sat solver and a mip solver. Our extensions aim to take better advantage of the power of the mip solver. The resulting improved hybrid solver is shown to be quite effective. © 2013 Springer-Verlag.
CITATION STYLE
Davies, J., & Bacchus, F. (2013). Exploiting the power of MIP solvers in MAXSAT. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7962 LNCS, pp. 166–181). https://doi.org/10.1007/978-3-642-39071-5_13
Mendeley helps you to discover research relevant for your work.