基于树状线性规划搜索的单调速率优化设计

改善单调速率（rate monotonic，简称RM）可调度性判定算法的效率，是过去40年计算机实时臣统设计的重要问题。最近，研究人员把可调度性判定问题扩展到了更一般的优化设计问题，即，如何调节在区间可选择情况下的任务运行时间，使得：（1）系统RM可调度；（2）系统的某个性能（如CPU利用率）达到最优。在已有的求解实时系统RM优化设计问题的方法中，都是先把原问题建模成广义约束优化问题，然后再对广义约束优化问题进行求解，但现有方法的求解速度较慢，任务数较多时不再适用。提出一种求解优化问题的方法——基于树状的线性规划搜（1inear programming search，简称LPS）方法。该方法先将实时系统RM优化设计问题建模成广义约束优化问题，再将其分拆成若干线性规划子问题，然后构造线性规划搜索树，利用剪枝搜索算法求解部分线性规划子问题，最后得到优化解。实验结果表明：LPS方法相比于已有的方法能够节省20％～70％的求解时间，任务数越多，节省时间越多。该研究成果可以与计算机可满足性模定理（satisfiability modulo theories，简称SMT）领域的多个研究热点问题联系起来，并可望改善SMT问题的求解效率。