Page 394 - 《软件学报》2024年第4期
P. 394

1972                                                       软件学报  2024  年第  35  卷第  4  期


                 表  subMUS  真子集中的节点.
                    接下来, 假设剩余节点存在代表与           subMUS  之间无包含关系的集合的节点, 任取其中一个与               subMUS  无包含
                 关系的集合    S, 那么至少存在一个元素       i 使得   i ∈ S  且  i < subMUS. 由  i < subMUS  可知  i 必属于用于构造  subMUS  的
                 每一个关键    MSS, 故当第   1  个关键  MSS  被求解出来时, 通过对此关键       MSS  所在节点做    BlockDown  操作已经使得
                 此关键   MSS  的全部子集所在节点被剪枝, 因此不存在这样的集合                S, 故该假设不成立.
                    性质  3. 若  subMUS  是不可满足的, 则  subMUS  本身是该问题唯一的       MUS.
                    证明: 假设   subMUS  是不可满足的, 那么一定存在一个         subMUS  的非空子集, 集合    subMUS'是一个   MUS. 由性
                 质  1  可知, subMUS  一定是  MUS  的子集. 那么, 集合  subMUS  自身是一个    MUS. 又由于   MUS  具有极小性, 因此
                 subMUS  的严格超集都不会是      MUS, 故  subMUS  是唯一的  MUS. 另外, 也可以通过性质      2  来解释性质   3, 由于经过
                 关键  MSS  的剪枝后, 哈斯图中剩余未探索节点所表示的集合一定是                  subMUS  的超集, 当  subMUS  不可满足时, 由
                 于未探索节点中没有代表         subMUS  真子集的节点, 故哈斯图中代表         subMUS  的节点是极小未探索子集, 因此无需
                 收缩操作, 直接将     subMUS  输出为一个   MUS, 同时对其全部超集作        BlockUp  操作, 故哈斯图中剩余节点全部被阻
                 塞, 哈斯图中无未探索节点, 算法结束, 因此我们通过性质               2  也证明了性质    3  的正确性.
                    性质  4. 在仅考虑在关键     MSS  下的剪枝的前提下, 算法每找到一个关键            MSS, 使用  ABC  策略后将会多剪枝一
                 个节点, 该节点为代表      subMUS  集合的节点.
                    证明: 若要证明此性质, 只需证明对          subMUS  所在的节点做    BlockDown  操作只剪枝一个节点即      subMUS  本身,
                 只需证明在做此      BlockDown  操作前  subMUS  的全部真子集所在的节点均已被剪枝. 而根据性质                2  可知, 在当前
                 subMUS  下最后一个关键     MSS  被求出时, 哈斯图中    subMUS  的真子集所在的节点均已被剪枝掉, 因此得证.
                    根据性质    1  和性质  2  可知, 通过关键极大可满足子集可以构造出一个子极小不可满足子集, 将整个搜索空间
                 从  C  的幂集缩减为子极小不可满足子集的全部超集. 性质                 3  则反映出在一种较特殊的情况下, 即子句集中的
                 MSS  均为关键   MSS  时, 使用本文所提出的      ABC  策略可以直接求解出子句集中唯一的             MUS  并结束算法的执行,
                 对比不使用该策略的情况可以提前一轮迭代结束算法, 减少一次对收缩操作的调用, 避免了这一部分的时间损耗.
                 性质  4  则反映出在绝大多数情况下策略的优化效果, 即每搜索到一个关键                     MSS  比不使用该策略的情况下多剪枝
                 一个节点, 如图    2(b) 所示. 该策略结合极大化模型可以使得求解效率更高, 这是由于使用极大化模型可以保证算
                 法优先选择哈斯图中顶层节点开始遍历, 而关键                 MSS  具有其基数为子句个数减一的特点, 这一特点使得关键
                 MSS  一定位于哈斯图的第       2  顶层, 这也意味着关键     MSS  可以尽早被发现, 从而在算法执行的前期加速剪枝过程,
                 有效缩减算法的搜索空间.

                                     1,2,3,4,5                                   1,2,3,4,5
                       cMSS                                        cMSS
                       1,2,3,4  1,2,3,5  1,2,4,5  1,3,4,5  2,3,4,5  1,2,3,4  1,2,3,5  1,2,4,5  1,3,4,5  2,3,4,5

                  1,2,3  1,2,4  1,2,5  1,3,4  1,3,5  1,4,5  2,3,4  2,3,5  2,4,5  3,4,5  1,2,3  1,2,4  1,2,5  1,3,4  1,3,5  1,4,5  2,3,4  2,3,5  2,4,5  3,4,5


                     1,2  1,3  1,4  1,5  2,3  2,4  2,5  3,4  3,5  4,5  1,2  1,3  1,4  1,5  2,3  2,4  2,5  3,4  3,5  4,5

                            1    2    3    4    5                       1    2    3    4    5  subMUS
                                      ø                                           ø
                       (a) 使用关键 MSS 进一步剪枝策略前的搜索空间                  (b) 使用关键 MSS 进一步剪枝策略后的搜索空间
                       图 2 给定子句集使用       ABC  剪枝策略前后哈斯图所代表的搜索空间 (虚线节点和边代表被剪枝)

                    例  2. 假设对子句集    C={1, 2, 3, 4, 5}求解  MUS, 搜索到一个  MSS  为{1, 2, 3, 4}时, 根据定义  15  可知, 该例中
                 的  subMUS  为{5}, 算法的搜索空间可以缩减为仅剩下哈斯图中那些为                 subMUS  的超集所对应的节点, 如图       2(a)
                 所示, 在使用   ABC  策略的情况下将比不使用该策略的情况下多剪枝一个代表集合{5}的节点. 若下一轮迭代中搜
   389   390   391   392   393   394   395   396   397   398   399