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

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

17. i←bitsup[x,a].size−1
18. index←bitsup[x,a][i].ts
19. while bitsup[x,a][i].mask & val[index]=0 do
20. i←i−1
21. if i=−1 then
22. D(x)←D(x)\{a}
23. if D(x).empty(⋅) then
24. return BackTrack
25. break
26. index←bitsup[x,a][i].ts
27. if i!=−1 then
28. residues[x,a]←i
29. Method enforceGAC(⋅):
30. deleteInvalidTuple(⋅)
31. searchSupport(⋅)
STRFDE ori 由 3 种方法构成.deleteInvalidTuple 方法使用已经被删除的值来更新当前约束的元组(第 2 行~
第 10 行),也就是使用 del 和 bitsup 来更新 val.在第 8 行,如果 u 不等于 0,这意味着当前约束的元组中存在对变
量值(x,a)的支持.由于(x,a)已经被删除,因此在第 9 行将支持(x,a)的元组删除.searchSupport 方法用于为变量的
每一个值来寻找支持(第 11 行~第 28 行).如果这个变量值不存在支持,那么就需要将其从相应的论域中移除.若
ori
ori
论域删空,则发生回溯.enforceGAC 方法是 STRFDE 的入口.实际上,只用 STRFDE 就可以求解 FDE 实例,实
验结果会在下一节中展示.
2.3 复杂性
下面我们证明 STRFDE 的空间复杂度和时间复杂度,并分析说明 STRFDE 针对 FDE 实例的实际空间复杂
度小于 CT 和 STRbit,证明我们的方法是有意义的.为了计算算法的复杂度,我们假定约束网络 N 中约束个数为
e,约束涉及变量个数为 r=r o +r f (r o 和 r f 分别为平凡变量和因子变量的个数),平凡变量论域大小为 d o ,因子变量论
域大小为 d f ,约束包含元组个数为 t,bit 位数为 w(w=64).
性质 1. STRFDE add 的最坏空间复杂度为 O(r o d o t/w).
证明:STRFDE add 采用的数据结构有 RSparseBitSet,support,last 和 residues,它们的空间复杂度分别是
O(3t/w),O(r o d o t/w),O(r o ),O(r o d o ).S val 和 S sup 空间复杂度都为 O(r o ),因此总的空间复杂度为 O(3t/w+r o d o t/w+r o +
r o d o +r o +r o )=O(r o d o t/w).证毕. □
对于附加约束,CT 算法中 support 结构的空间复杂度为 O(r o d o t/w+d f t/w),因此,CT 算法的空间复杂度为
O(r o d o t/w+d f t/w).大部分实例的因子变量论域大小 d f 要远远大于平凡变量的论域大小 d o ,因此直接使用 CT 来求
解 FDE 实例可能造成内存溢出问题.
性质 2. STRFDE add 的最坏时间复杂度为 O(r o d o t/w).
证明:STRFDE add 算法根据 CT 算法改进而来,CT 算法的时间复杂度为 O(rdt/w) [22] ,STRFDE add 算法中第 6
行和第 22 行的时间复杂度为 O(t/w),其余的算法复杂度为 O(r o d o t/w).因此,附加约束算法的时间复杂度为
O(r o d o t/w).证毕. □
ori
性质 3. STRFDE 的最坏空间复杂度为 O(r o d o t/w+r f d f t/w).
ori
证明:STRFDE 采用的数据结构有 bitsup,val,del 和 residues.对于 val,del 和 residues,它们的空间复杂度分
别是 O(t/w),O(r o d o +r f d f )和 O(r o d o +r f d f );对于因子变量,bitsup 的最坏空间复杂度为 O(r f d f t/w);对于平凡变量,bitsup
ori
的最坏空间复杂度为 O(r o d o t/w).因此,STRFDE 的最坏空间复杂度为 O(r o d o t/w+r f d f t/w).证毕. □
ori
ori
我们发现,STRFDE 和 CT 对于附加约束的最坏空间复杂度相同,但由于 STRFDE 的 bitsup 只存储不为