基于可满足性模理论的多处理机通信延迟优化调度方法

作者：姜松岩; 廖晓鹃; 陈光柱

来源：计算机应用, 2022, 1-9.

• 并行计算
• 任务调度
• 可满足性模理论
• 线性规划
• 有向无环图

在一组相同处理器上调度带有通信延迟的任务图，以实现其最短的执行时间，在并行计算的调度理论和实践中具有重要的意义。针对具有通信延迟的任务图调度问题，提出了一种基于可满足性模理论（Satisfiability Modulo Theory，SMT）的最优化算法。首先，将处理器映射约束和任务执行顺序等约束条件进行编码，将任务图调度问题转化为SMT问题；然后，调用SMT求解器对可行解空间进行搜索，从而确定问题最优解。在约束编码阶段，使用整型变量来表示任务和处理器的映射关系，降低处理器约束编码的复杂程度；在求解器调用阶段，通过添加独立任务的约束条件来减小求解器的搜索空间，进一步提升最优解的查找效率。实验结果表明，与现有的原始SMT算法相比，改进的SMT算法在20 s和1 min超时实验中的平均求解时间分别减少了65.9%与53.8%，并且在处理器数量较多时取得更大的效率优势。因此，改进的SMT算法可以有效求解带通信延迟的任务图调度问题，尤其适用于处理器数量较多的调度场景。

• 单位
  成都理工大学