IIS日志


IIS日志

回想一下,不可约不可行子系统(IIS)是不可行模型中的约束和变量边界的子集,具有以下属性:

  • 这仍然是不可行的,而且
  • 如果移除单个约束或约束,子系统就变得可行。
识别IIS的过程是一个加法和减法的过程。该算法生成一组已知是IIS的一部分的约束和边界,以及已知不是IIS的一部分的约束和边界。您可以在IIS日志中跟踪此进程的进度。
计算不可约不一致子系统(IIS)…约束| |范围运行时最小最大猜|最小最大的猜测  | -------------------------------------------------------------------------- 0 17509 - 0 4 - 0 0 12996 - 0 4 - 5 0 10398 9749 0 0 - 10 0 0 0 - 15 s 1 9584 9576 0 0 - 20年代4 0 0 - 25 s 6 9406 8432 40 0 0 0 - 30年代8 0 - 35 s 11 8422 40 0 0 - 40年代15 8413 60 0 0 - 45 s 18 8241 600 0 - 50年代21 7908 50 0 0 - 55 24 7735 50 0 0 - 60年代……
前两列显示了IIS中约束集的最小和最大大小。第四列和第五列给出了变量边界集合的相同信息。最后一列显示经过的运行时。

IIS日志中的第三列和第六列提供了IIS最终大小的猜测。计算IIS非常耗时,了解结果的大小通常是很有用的。在某些情况下,这些猜测可能相当准确,但不幸的是,有一些模型可以欺骗我们的启发式。你应该把这些当作非常粗略的估计。

当进程完成时,算法输出IIS的大小(不可约子系统中的约束和边界的数量):

IIS计算:102约束,0限制IIS运行时:129.91秒
注意,在本例中,早期的猜测大约是50个约束,但IIS包含102个。

如果你提前终止这个过程,你会得到一个非最小的不可行的子系统:

非最小IIS计算:3179约束,0限制IIS运行时:120.29秒