Page 212 - 《软件学报》2021年第11期

3538 Journal of Software 软件学报 Vol.32, No.11, November 2021

如表 1 所示,CT 在 5 组实例上是最快的,但是在求解某些 sat 实例时会消耗较多的时间,例如 aim-200 和
dubois;STRFDE 在 4 组实例上是最快的,并且可以求解出的实例数最多;STRFDE 与其他 fPWC 算法相比,在 8
组实例上是最快的.通过分析数据可以发现,CT 检查一个点是否满足 GAC 所用的时间较少,而 fPWC 算法检查
一个点所用的时间较长.一般来说,fPWC 算法的效率低于 GAC 算法,这是因为对某些实例,维持 fPWC 会在 GAC
的基础上进行额外的检查,从而删去更多的元组.
比较 PW-CT 与 STRFDE,PW-CT 在一些 sat 实例上具有优势.这是因为当某些约束涉及的元组较少时,使用
PW-CT 有较高的效率.但是当约束涉及大量元组时,使用 PW-CT 的效率就比较低.因此,除了一些元组较少的实
例外,STRFDE 的效率是优于 PW-CT 的.与 CT+FDE 和 STRbit+FDE 相比,STRFDE 在大部分实例上的效率有提
ori
升,并且它能求解一些 CT 和 STRbit 造成内存溢出的实例.STRFDE +FDE 在一些实例上也有较高的效率,但是
会在求解附加约束的数量远多于原始约束的实例时占用更多的内存,例如 rand-5-12-12,这是因为它为附加约束
中的因子变量存储了支持.STRFDE 与 STR2+FDE 相比有巨大的提升,就像 CT 和 STRbit 比 STR2 快一样.综上
所述,STRFDE 的效率在 fPWC 算法中是有竞争力的.
在该表中,PW-CT 的结点数比其他算法少.这是因为 PW-CT 使用原始的约束网络来维持 fPWC,其执行额外
的 PWC 检查来删除比 CT 更多的元组.如果执行 PWC 检查的速度很慢,并且只删除很少的元组,那么 PW-CT 是
低效的.这就解释了为什么 PW-CT 求解随机实例时需要花费更长的时间.后 5 种算法的结点数在一些实例上是
相同的,这意味着它们具有相同的搜索树.实际上,STRFDE 在单位时间(s)内搜索的结点比 STR2+FDE 多.
如果一个实例没有解并且没有 PW支持,那么只需在 fPWC 初始化检查时就可以确定这个实例的结果.这种
情况的结点数为 0,例如 rand-10-20-10 和 rand-5-12-12.因此在求解这类实例时,fPWC 算法比 GAC 算法更有优
势.对于至少有一个解的实例,例如 rand-8-20-5,它的每个约束都包含大量的元组,在其上维持 fPWC 将花费一定
的时间来检查每个元组是否满足 PWC.因此,在求解这类实例时,维持 GAC 比维持 fPWC 更有效率.
为了使结果更加直观,我们通过散点图(如图 3 所示)展示了 STRFDE 与不同算法求解实例的对比情况.如第
一个散点图所示,STRFDE 虽然不能优于 CT,但在求解部分实例时比 CT 的效率更高.其他散点图的大部分点位
于线 y=x 下,这表明 STRFDE 在求解大多数实例时快于对比算法.

Fig.3 Runtime comparison of STRFDE and other algorithms on all instances
图 3 STRFDE 与其他算法在所有实例上的运行时间比较