Max-SAT is an optimization version of SAT that can represent a wide variety of important optimization problems. We introduce a new approach for solving Max-SAT, that exploits both a SAT solver and a Mixed Integer Programming (MIP) solver in a hybrid approach. Each solver generates information used by the other solver in a series of iterations that terminates when an optimal solution is found. Empirical results indicate that a bottleneck in this process is the time required by the MIP solver, arising from the large number of times it is invoked. We present two enhancements of the basic algorithm, that address this bottleneck. First, we enrich the constraints given to the MIP solver. Second, we postpone the calls to the MIP solver by substituting non-optimal solutions for the optimal ones computed by the MIP solver, whenever possible. We present empirical results that show that the resulting solver, MaxHS, is the most robust existing solver for Max-SAT.

свернуть