1
$\begingroup$

Many modern SAT and SMT solvers offer a feature where they can report why a problem is unsatisfiable, something called an "unsat core."

Are there any optimization solvers (in my case, specifically MILP and LP) that can report the minimal infeasible constraint set? What is the name of this, equivalent to "unsat core?"

$\endgroup$
2
  • $\begingroup$ The tag I just added is your answer. :) But let me clarify that such a set is typically not unique. $\endgroup$
    – RobPratt
    Apr 14, 2023 at 17:14
  • $\begingroup$ Please give that was an answer and I'll gladly accept it. $\endgroup$
    – Nate
    Apr 14, 2023 at 17:38

2 Answers 2

4
$\begingroup$

In the optimization community, this is called an irreducible infeasible set (IIS), and many solvers support this functionality. The "irreducible" part means that the set is minimal in the sense that removing any constraint yields a feasible set. Such a set is typically not unique, and removing one member does not necessarily make the original problem feasible, so you might need to find and repair an IIS multiple times. The problem of finding a minimum-cardinality infeasible set is much more difficult.

$\endgroup$
2
  • $\begingroup$ Please explain "removing one member does not necessarily make the original problem feasible". Do you mean by "member", a (one) constraint, in which case that appears to contradict "removing any constraint yields a feasible set.? $\endgroup$ Apr 15, 2023 at 23:26
  • 1
    $\begingroup$ @MarkL.Stone Removing any constraint from the IIS yields a feasible subsystem of that IIS, but removing that same constraint from the original problem does not necessarily yield a feasible problem. $\endgroup$
    – RobPratt
    Apr 15, 2023 at 23:51
0
$\begingroup$

FindMUS in MiniZinc might be of interest:

https://www.minizinc.org/doc-2.5.3/en/find_mus.html

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.