计算机应用

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

单位：成都理工大学 计算机与网络安全学院，成都 610059

关键词：并行计算,任务调度,可满足性模理论,线性规划,有向无环图

基金：国家自然科学基金资助项目（61806171）；四川省科技计划重点研发项目（2022YFG0198）。

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

来源：2023年第1期

《计算机应用》期刊编辑部

查看计算机应用杂志2023年第1期