The optimization phase is necessary because there is no way to describe some solutions as more desirable than others to a SAT solver. Instead, once a solution is found, IPS adds constraints to the problem to separate less desirable choices, and to separate the current solution as well. IPS then repeatedly invokes MiniSAT and repeats the above operation until no more solutions are found. The last successful solution is taken as the best one.
The difficulty of finding a solution is proportional to the number of possible solutions. Being more specific about the desired result produces solutions more quickly.
Once the set of package FMRIs that best satisfy the posed problem is found, the evaluation phase begins.