Optimal MUS extraction with delayed optimization;
We investigate the problem of providing the simplest explanation for explaining over-constrained – and hence – unsatisfiable problems to a user.
Computing a simple explanation can be seen as computing a minimal unsatisfiable subset (MUS) of facts.
If simplicity is defined by the size of the explanation, then many applications aim to find the smallest MUS.
While some techniques can extract the smallest MUSes given a set of unsatisfiable constraints, we have developed a technique to compute the optimal MUS (OMUS).
The optimality criterion refers to a given objective function.
In this paper, we describe a novel hybrid approach for solving the OMUS problem harnassing the power of both SAT solvers and MIP solvers.
Preliminary results show that the bottleneck of our algorithm lies in the expensive calls to the MIP solver.
Inspired by recent work on MaxSAT solving, we observe that we can improve the efficiency of our algorithm by postponing the calls to the MIP solver, without affecting the correctness of the approach.
Periode7 sep 2020
Mate van erkenningInternational