优化解析器结果

优化阶段很有必要，因为没有办法来描述某些解决方案比其他解决方案更适合 SAT 解析器。相反，一旦找到一个解决方案，IPS 将向问题添加约束来隔离不太合意的选择，并隔离当前解决方案。然后，IPS 重复调用 MiniSAT 并重复以上操作，直到无法确定更多的解决方案。将采用最后一个成功的解决方案作为最好的解决方案。

确定解决方案的难度和可能的解决方案的数目成比例。关于期望的结果的信息越具体，生成解决方案的速度越快。

找到最能满足所引起问题的软件包 FMRI 的集合后，评估阶段开始。