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

姜松岩，廖晓鹃，陈光柱

（成都理工大学 计算机与网络安全学院，成都 610059）

0 引言

计算机系统中日常要处理的任务越来越复杂，任务量也日益庞大，同时计算机系统本身的处理器数量也在逐步增加，并行计算的重要性也越来越明显。任务调度问题作为并行计算的关键问题一直受到广泛关注。具有通信延迟的任务图在一组相同处理器上调度是任务调度问题中的一个经典问题，该问题在经典的α|β|γ［1］描述中可以表示为Pm|pred|Cmax，其中：α域为Pm，表示机器环境为m个相同机器；β域为pred，表示约束限制中包含优先约束；γ域为Cmax，表示优化的目标为完工时间。在该问题形式化过程中，通常会以带有权值的有向无环图（Directed Acyclic Graph，DAG）作为任务图表示在并行系统中要执行的程序，程序中的任务以DAG 中的节点表示，任务间的依赖关系使用DAG 中的边表示，任务的执行时间与任务间的通信延迟分别以节点和边的权重表示。Sarkar［2］已经证明，求解并行处理器上带有通信延迟的任务图上的最小的完成时间的调度问题是NP（Nondeterministic Polynomial）困难问题。

目前的国内外研究中，解决这类调度问题的方法主要可以分为启发式算法和精准算法两类。由于并行处理器上任务图调度问题的难度会随着任务数量的增加呈指数增长［3］，因此通过牺牲一定精度来获取更快求解速度的启发式算法十分受欢迎。例如，张架鹏等［4］通过优化蜂群搜索策略来解决同类机调度的问题；翟文正等［5］以任务高度和粒子位置构造优先级列表的思想，提出一种面向DAG 任务模型的微粒群优化调度算法；马晓梅等［6］使用改进后的遗传算法对印刷生产过程中的调度问题进行了抽象并求解；杨小东等［7］提出了一种以帝国竞争算法为基础，并在同化操作中融入遗传算法中的杂交算子和变异算子的混合的启发式算法来解决车间调度问题。这类启发式算法能在较短时间内获得问题的近似解，从而满足许多实时应用场景的需求。但不可否认的是，在某些应用场景中，获得问题的最优解有着十分重要的意义，比如在评价启发式算法优劣时需要利用最优解来计算启发式算法获得的近似解的准确率和误差，以及在某些对于时间精度要求较高的实际问题中，启发式算法获得的近似解往往不能满足要求，既无法保证解的全局最优性，也很难保证求解的质量［3］。

在精准算法的方向上有以下几种方法较为常见：一种是基于混合整数线性规划（Mixed Integer Linear Programming，MILP）的方法，首先将求解问题抽象为MILP 公式，然后使用求解器在公式的解空间内进行搜索，从而获得最优解［8-10］。另一种是基于布尔可满足性（Boolean Satisfiability，SAT）的方法，将调度问题抽象为命题逻辑公式的可满足性问题，通过循环调用SAT 求解器来确定使命题逻辑式可满足的最优解，展示出了SAT 求解器强大的计算能力［11-12］；但由于SAT求解器只能处理由布尔逻辑运算与、或、非连接布尔变量所构成的布尔逻辑公式，在描述调度问题特征和约束条件时的编码较为困难。目前还有一种常见的方法是基于可满足性模理论（Satisfiability Modulo Theory，SMT）的方法［13-15］。SMT方法与SAT 方法类似，都是将问题抽象为逻辑公式，通过验证其可满足性来搜索最优解，两者主要区别在于：SAT 方法只能使用布尔集合上的逻辑运算（逻辑与、或、非），而SMT方法支持更丰富的变量类型和运算，能有效处理由变量、量词、函数、谓词符号和逻辑运算构成的一阶逻辑公式，因此可以更加便捷高效地描述问题特征和约束条件。Malik 等［13］提出了一种SMT 约束公式，利用SMT 求解器对公式的可满足性进行判断，通过二分搜索法确定带延迟的任务图调度问题的最优解，并证实在带延迟的任务图最优调度上，SMT 方法比MILP 方法更具优势，但该优势仅在处理器数量较少时表现明显，随着处理器数量的增加，SMT 和MILP 方法的效率十分接近。这是因为Malik 等［13］引入布尔变量来描述任务和处理器的映射关系，当处理器数量增加时，布尔变量的数目急剧上升，带来编码规模膨胀问题。除此之外，我们注意到，Malik 等［13］提出的SMT 方法在循环调用求解器进行最优解查找时没有优化搜索空间，导致搜索空间中存在无效解，浪费了求解器的计算资源。本文在Malik 等［13］提出的SMT 方法（即原始SMT 方法）的基础上进行优化，提出了改进的SMT方法。与原始SMT 方法相比，改进的SMT 方法主要有以下优势：1）改进的SMT 方法使用整型变量来表达任务节点与处理器的映射关系，减少了约束编码所需的变量数目；2）为具有相互独立关系的任务增加新的约束条件，从而限制任务在处理器上的分配位置，达到优化求解器搜索空间的目的。

实验结果表明，在20 s 超时实验中，对于超时数量，改进SMT 算法与原始SMT 方法相比减少了11.4%，与两种MILP方法相比分别减少25.3%和26.5%；对于限时完成的任务求解时间，改进的SMT 算法与原始SMT 方法和MILP 方法的相比，平均求解时间均减少了65%以上，并且随着处理器数量的增加，改进的SMT 算法的优势会愈加明显，这提高了SMT方法在求解带通信延迟的任务图调度问题上的优势地位。

1 问题模型

任务图G(V，E)以带权的有向无环图（DAG）表示，其中V={v1，v2，…，vn}是任务节点的集合；E⊆V×V是任务节点之间依赖关系与通信关系的集合。任务间的关系分为独立关系和依赖关系，独立关系指两个任务之间无法连通，依赖关系又分为直接依赖关系和间接依赖关系。直接依赖关系指两个任务节点被一条有向边相连，其中有向边指向的任务被称为另一个任务的后置任务，而另一个任务称为前者的前置任务；间接依赖关系指两个任务之间可以连通但不直接相连。任务图中任务节点出边的条数称为该节点的出度，入边的条数称为该节点的入度。多处理器平台P={p1，p2，…，pm}由m个互相可以通信的相同处理器组成，其中每个处理器均可以与其他处理相互通信。在任务图调度过程中，具有依赖关系的一对任务必须按照其先后顺序进行调度，任务在执行过程中不会发生抢占，每个任务都可以在任何一个处理器上运行，且只会被安排到唯一的一个处理器上。任务v∈V的执行时间表示为t(v)，具有直接依赖关系的任务对(vi，vj) ∈E的通信延迟表示为c(vi，vj)。如果一对具有直接依赖关系的任务被分配到了同一个处理器，则它们可以通过共享本地内存中的数据完成通信，因此不会产生通信延迟；如果它们被分配到了不同的处理器，则需要进行处理器间的通信完成数据传输，从而产生通信延迟c(vi，vj)。

在这个问题中，所有的任务运行时间、通信时间以及任务关系和处理数量都是已知的。调度的目标是获得任务图G(V，E)在P上的完成时间m(G)的最小值，同时还要获得在min(m(G))时任务节点与处理器的映射关系，以及每个任务节点开始的时间s(v)。

2 改进的SMT方法

SMT 问题指在特定理论下判定一阶逻辑公式可满足性的问题，针对这类问题的判定算法被称为SMT 求解器。SMT的应用领域广泛，例如：多核问题、程序缺陷检测验证、优化问题求解、程序验证等［16-18］。这些领域中待解决的实际问题都可以建模为约束可满足问题，SMT 在这类问题的表述和求解上有突出优势。

2.1 方法描述

本文提出一种改进SMT 方法来解决带通信延迟的任务图的调度问题。为了刻画任务与处理器间的映射关系，引入整型变量q(v)（q(v) ∈{1，2，…，m}）表示执行任务v的处理器编号，调度目标为获得任务图G的最小的完成时间min(m(G))。

SMT 约束公式的定义如下，G+=(V，E+)为任务图G的传递闭包，其中E+包含了任务图中所有的传递关系，t(v)为任务节点的权重即执行时间，c(vi，vj)为边的权重即通信延迟时间，⊃表示逻辑运算中的蕴含运算。

C1 所有任务都会被分配在唯一的处理器上。

1 ≤q(v) ≤m；∀v∈V

C2 所有入度为0 的任务（没有前置任务的任务）的开始时间不小于0。

C3 如果两个任务被分配到不同的处理器上，则后置任务的开始执行时间一定不早于前置任务的完成时间加上两个处理器之间的通信延迟（c(vi，vj)）。

C4 如果两个任务被分配到相同的处理器上执行，则后置任务可以在前置任务完成后立即执行。

约束C3 和C4 共同约束了具有直接依赖关系的两个任务的执行顺序即在一对具有直接依赖关系的任务中，后置任务必须在前置任务执行完成后才能开始执行。

C5 如果两个相互独立的任务被分配到相同处理器上，则一方需要等待另一方完成后才能开始执行。

C6 所有任务都在时间m(G)内执行完毕。

上述的约束公式只与任务图和处理器数量有关，在调度问题的求解过程中不会改变。通过将所有约束条件输入SMT 求解器（如Z3 求解器）就能判断对于一个给定的时间m(G)，是否所有的约束条件都能被满足。如果求解器在计算后输出一个非空模型，则表明所有任务都能在m(G)时间内完成；如果求解器输出的模型为空，则表明当前设定的m(G)值过小，不能在该时间内完成所有任务。为了找到使SMT 求解器输出非空模型的最小m(G)，本文使用二分搜索法在可行解的范围内进行查找，其中搜索的初始上界(Tup)为假设所有任务在同一个处理上顺序执行的总时间：

初始下界(Tdown)为在假设所有任务并行执行的时间：

为了减少搜索空间，引入一个新约束C7，定义如下：

约束C7 表示对于两个相互独立的任务，如果它们的执行时间之和大于本次搜索设定的完成时间m(G)，则这两个任务必须分配在不同的处理器，否则SMT 求解器输出的模型必定为空。在二分搜索的过程中，如果某次求解的模型结果不为空（即模型为可满足的），则在之后的搜索过程中保留约束C7；如果某次求解的模型结果为空（即不可满足），则删除约束C7，不会影响之后的搜索过程。

二分搜索的算法流程如下，其中Assert（）函数用于获得SMT 约束集合，以任务图为输入，返回根据SMT 约束公式C1～C7 生成的约束集合；CallSMTSolver（）函数用于调用SMT求解器，以约束集合为输入，返回求解器的求解模型，如果输出的模型非空，表示输入求解器的所有约束条件都是可满足的，否则，表示不存在满足所有约束条件的模型；add（）与delete（）函数分别用于向约束集中添加和删除约束。

在上述算法中，首先将任务图的信息进行编码作为约束添加到求解器中，之后根据搜索的上下界确定中值，并根据本次搜索的中值添加约束C7。此后对求解器进行求解，如果求解的结果为可满足，则继续判断是否搜索结束，如果没有结束，则修改搜索上界为中值；如果求解结果为不可满足，则更新下界为中值。同时由于C7 只有在模型可满足时才可以保证成立，因此要将此次添加的C7 删除。

通过上述的二分搜索的过程就可以获得m(G)的最小值与取得最小值时的调度模型，m(G)的最小值为Tup=Tdown时的值。

为了更加直观地展示改进SMT 方法，本文以图1 所示的任务图为例，展示如何利用改进SMT 方法求解在两个处理器上的任务调度问题。

图1 任务图示例Fig.1 Task graph example

对于图1 所示任务图在两个处理器上的调度问题，使用本文所提出的SMT 公式描述结果如下：

将上述约束添加到SMT 求解器中之后将进行二分求解。二分求解的具体过程如表1 所示，具体过程如下：

表1 任务图的二分求解流程Tab.1 Binary solution process of task graph

第1 轮次中，Tup=16，Tdown=9，Tmid=12，向求解器添加约束m(G)=12，因为t(v2)+t(v3)=13 ＞Tmid，向求解器中添加约束q(v2) ≠q(v3)。求解得到结果为模型可满足，将Tup修改为12 并将约束m(G)=12 删除后继续下一次求解。

第2 轮次中，Tup=12，Tdown=9，Tmid=10，向模型添加约束m(G)=10，因为t(v2)+t(v3)=13 ＞Tmid，向模型中添加约束q(v2) ≠q(v3)。对模型进行求解得到结果为模型不可满足，将Tdown修改为11 并将约束m(G)=10 与本次求解中添加的q(v2) ≠q(v3)删除，继续下一次求解。

第3 轮次中，Tup=12，Tdown=11，Tmid=11，向模型添加约束m(G)=11，因为t(v2)+t(v3)=13 ＞Tmid，向模型中添加约束q(v2) ≠q(v3)。求解模型得到的结果为模型不可满足，将Tdown修改为12 并将约束m(G)=11 与本次求解中添加的q(v2) ≠q(v3)删除，继续下一次求解。

第4 轮次中，Tup=12，Tdown=12，Tmid=12，向模型添加约束m(G)=12，因为t(v2)+t(v3)=13 ＞Tmid，向模型中添加约束q(v2) ≠q(v3)。进行求解得到结果为模型可满足，此时Tup=Tdown，二分搜索结束，获得最小的任务完成时间为12。该任务图的最优的调度通过本次求解结果模型中变量q(v)与s(v)的值获得。

2.2 理论分析

本文提出的SMT 方法与原始SMT 方法相比主要作出了以下的改进：

1）原始SMT 中使用一组布尔型变量b(v，p)作为决策变量，b(v，p)=1 表示任务(v)由处理器(p)执行，b(v，p)=0 表示任务v不在处理器p上执行。显然，当处理器数目为m时，每个任务需要m个布尔变量来表达该任务和处理器的映射关系。改进的SMT 方法使用整型变量q(v)来表达这一映射关系，显著减少了变量的数量。与此同时，在表达一组符合条件的任务的C3、C4、C5 时原始SMT 因为使用布尔变量的原因表达C3 需要m× (m-1)条约束，表达C4 与C5 需要m条约束。改进的SMT 方法因为使用整型变量，因此在表达C3、C4、C5 时都只需要1 条约束，显著减少了约束数量。

2）与原始SMT 方法相比，改进的SMT 方法在二分搜索过程中增加了一个新约束C7，C7 通过比较两个相互独立的任务执行时间和与m(G)的关系，对相互独立的任务的分配情况进行约束，将待搜索空间中的无效解去除，从而达到减少求解器搜索空间、提高求解效率的目的。

3 实验与结果分析

本章将使用Malik 等［13］提出的原始SMT 方法以及Venugopalan 等［19］提出的两种MILP 方法（MILP-BASIC 方法和MILP-RELAXED 方法）作为对照与本文提出的SMT 方法进行比较。实验使用的SMT 方法的求解器为4.8.10 版本的Z3［20］，使用的MILP 方法的求解器为9.1.1 版本的Gurobi［21］求解器。所有实验均在具有2 GB 内存的Ubuntu 64 位系统的虚拟机中进行。为了消除两种求解器对于多CPU 资源利用效率不同的影响，虚拟机设定为单CPU。

3.1 数据集

本节实验中使用到的527 幅任务图，均为加权的有向无环图，这些任务图全部来自于文献［13］中所使用过的数据集，这些任务图的结构包含有：Independent、ForkJoin、Pipeline、SeriesParale、Random 等10 种结构，具体结构分布情况如表2 所示。这些任务图中包含10 任务、21 任务、30 任务三种不同任务数量任务图。本节实验将这527 幅任务图分别设定在2、4、8、16 处理器上进行调度，即每种方法将会得到527 × 4=2 108 个运行结果。

表2 任务图结构分布情况Tab.2 Distribution of task graph structure

3.2 MILP方法对比

混合整数线性规划（MILP）是解决组合优化问题中常用的方法。为了更为广泛评价所提改进SMT 方法的性能，将使用了MILP 的方法与本文方法进行比较。文献［19］和文献［13］中总共涉及6 种不同的MILP 方法，其中有三种通过去除自反解来减少求解时间的方法，在文献［13］中已经被证明在求解时间方面整体效果更差，因此在另外效果较好的三种方法中，本文选取了其中比较有代表性的两种方法（MILPBASIC 方法［19］和MILP-RELAXED 方法［19］）与改进SMT 方 法进行比较。

MILP 方法的求解过程主要如下：首先将调度问题抽象为MILP 公式；然后，将根据问题抽象出的MILP 公式添加到相应的求解器中；最后，使用求解器求解。与SMT 方法的求解器不同，使用MILP 的求解器Gurobi 能自动求解Min-Max问题，因此不需要二分搜索的过程就可以求出最优解。

3.3 结果与分析

首先对四种方法在20 s 超时时间内能成功求解的任务图数量进行比较。如果任务图在某个数量的处理器上能够完成求解过程则称这幅任务图在某个数量处理器上限时完成。527 张图在4 种处理器数量的设定下20 s 限时完成任务图数量如表3 所示。

表3 20 s超时时间内限时完成任务图数量对比Tab.3 Comparison of number of task graphs completed within 20 seconds timeout

通过表3 中限时完成数量的对比可以看出，改进后的SMT 方法限时完成的数量明显多于另外三种方法，即改进后的SMT 在20 s 超时时间的限定下可以获得更多任务图的最优解。

在统计并对比了各方法限时数量的基础上，对四种方法在限时20 s 内完成的任务的求解时间的分布进行统计，结果如图2 所示。横坐标表示完成任务的时间区间，纵坐标表示在该区间时间内完成任务的数量。

图2 限时完成任务求解时间分布Fig.2 Time distribution of task graphs completed within time limit

通过图2 可以看出，改进SMT 方法所需的求解时间分布整体比其他三种方法靠前。例如，在求解时间不超过0.5 s的区间内，改进SMT 方法成功求解超过1 000 幅任务图，而两种MILP 方法能求解的任务图数量不超过800，原始SMT 方法的求解数量最少，约500 幅任务图。这表明改进SMT 方法在简单问题上所需要的求解时间更少。另一方面，在超过10 s 的时间区间内，改进SMT 方法完成的任务图数量较另三种方法明显更少。这表明，在求解相对复杂的任务图时，改进SMT 方法与另外三种方法相比更具优势。

表4 是四种方法在超时时间20 s 内完成任务图的平均求解时间，每种方法的平均求解时间计算公式为：Tavg=Ttotal/N，其中Ttotal为某方法在限时20 s 内完成任务图的求解时间的总和，N为该方法在限时完成的任务图数量。从表4可以看出，改进的SMT 方法在超时时间内完成的任务数量最多，因此在统计平均求解时间时改进的SMT 方法中包含了更多相对不易求解的复杂的任务图的运行时间。尽管如此，改进的SMT 方法在平均求解时间上仍具有巨大优势，与原始SMT 方法相比平均求解时间减少了65.9%，与MILP-BASIC方法相比减少了69.2%，与MILP-RELAXED 方法相比减少了69.1%。这表明在平均求解时间上改进的SMT 方法与另外三种方法相比具有极大的优势。

表4 20 s超时时间内完成任务的平均求解时间 单位：sTab.4 Average solving time of task graphs completed within 20 seconds timeout unit：s

为了更加充分地验证这几种方法在数据集上的表现，将超时时间扩大到了1 min 再次进行了实验，获得了20 s 超时时间相似的结果，具体的限时完成数量与平均求解时间如表5 所示。

表5 1 min超时时间内完成任务的平均求解时间Tab.5 Average solving time of task graphs completed within one minute timeout

由表4 和表5 对比可以看出在扩大限时时限到1 min 之后四种方法的表现基本与20 s 的限时实验中的表现相似，改进SMT 方法在完成数量与求解时间上均具有一定优势。

图3 统计了在20 s 超时时间内，每种方法在四种不同处理器数量上的表现，由于在该数据集较大且超时数量较少，为了更加直观对比随处理器变化情况这里采用了对比超时任务对数量来评估在不同数量的处理器的表现。

图3 超时任务数量随处理器数量变化比较Fig.3 Comparison of number of timeout tasks varying with number of processors

从图3 可以直观地看出，随着处理器数量的增长，所有方法的超时任务图数量均呈现下降趋势，说明处理器越多，越容易在规定时间内获得最优解。这是因为这两类方法都是使用单纯形（simplex）求解器去求解数值方程，随着处理器数量的增加，单纯形中有更多的松弛空间［13］。

图3 也清晰地反映出随着处理器数量的增加，改进SMT方法优势愈加明显。当处理器数量为2 时，改进SMT 的超时任务数量比原始SMT 减少4.02%，比MILP-BASIC 减少了15.66%，比MILP-RELAXED 减少了17.33%；当处理器个数为16 时，改进SMT 方法的超时数量比原始SMT 减少了41.67%，比MILP-BASIC 与MILP-RELAXED 均减少了约54.35%。这一现象表明，随着处理器数量的增加，改进SMT方法更具优势。这一优势主要来自于对问题模型进行约束编码过程中变量数量与约束数量的减少。在变量数量方面，改进SMT 方法引入整型变量q(v)来表达任务-处理器映射关系，随着处理器增加，该变量的取值范围发生改变，但是并不会改变此类变量的数量；而原始SMT 方法采用布尔变量b(v，p)作为决策变量来表示是否将任务v调度至处理器p上执行，因此对于包含n个任务节点的任务图在m个处理器上调度的问题，共需要m×n个布尔型变量才能完成任务，随着m数值的增加，这一变量的数量也在快速增加。因此，在处理器数目增多时，与两种MILP 方法相比，原始SMT 方法的性能优势不再明显，而改进SMT 方法始终能保持求解效率的巨大优势。在约束条件的数量方面，对两种SMT 方法对问题模型进行编码过程中的约束数量统计如表6 所示。

表6 两种SMT方法不同处理器数量时的平均约束数量对比Tab.6 Comparison of average number of constraints of two SMT methods with different numbers of processors

通过表6 可以看出，改进的SMT 方法的约束数量不会随处理器数量变化而变化，而原始SMT 方法的约束数量会随处理器数量增长而快速增长。这是因为对于每一对符合要求的任务，改进后的SMT 方法在描述C3、C4 与C5 时都只需要1条约束。原始的SMT 方法中，实现C3 需要m× (m-1)条约束，实现C4 和C5 分别需要m条约束。因此，随着m数值的增加，相关的约束条件数量也在快速增长，从而导致问题规模膨胀，造成求解器的搜索空间扩增。

由于本文提出的改进SMT 方法中包含了变量优化和添加新约束两个方面的改进，下面进行消融实验来确定求解性能优化与这两者的关系。20 s 超时的消融实验结果如表7 所示。其中，“添加约束”指与原始SMT 方法相比只在二分求解过程添加新约束，“改进变量”指与原始SMT 方法相比只将变量变更为整型，“改进SMT 方法”为两者皆有。

表7 改进变量与添加约束的有效性对比Tab.7 Comparison of effectiveness of improving variables and adding constraints

从表7 中可以看出本文中针对SMT 方法的两处改进都是有效的，其中在二分求解过程中添加新约束的改进效果较为一般；而将变量更改为整型所带来的改进效果比较明显，这也是改进SMT 方法优势的主要来源，这一结论同时反映在限时完成数量以及平均求解时间两个方面。

4 结语

本文在研究了带有通信延迟的任务图在一组相同处理器上的调度问题。基于前人的SMT 的方法设计，本文使用新的决策变量来表达任务节点与处理器的映射关系，并引入了新的约束公式来描述问题中相互独立的任务之间的调度约束条件。实验结果表明，与原始SMT 方法和MILP 方法相比，改进的SMT 方法在限时完成数量和平均完成时间等性能指标上均有显著优势；随着处理器数量增长，改进的SMT 方法在求解效率方面的优势更加明显；但在问题规模扩大时求解模型规模仍然会快速膨胀，导致很难在短时间内求得大规模问题的最优解。

未来的研究工作将聚焦于更加符合生产实际条件的智能制造车间调度等问题上，在多约束、多目标的车间调度问题上，SMT 方法的应用尚有待开发，具有广阔的研究前景。