-
摘要:
极小不可满足子集(minimal unsatisfiable subset,MUS)的求解是理论计算机科学的重要问题. 由于极小不可满足子集的个数随问题规模呈指数级增长,现有算法致力于在合适的时间限制内尽求解出可能多的MUS.在庞大的搜索空间中,选择合适的节点来扩展可以大幅减小收缩和扩充操作的时间开销,从而提高算法的求解效率. 提出一种基于增量信息交互的MUS求解算法MARCO-MSS4MUS,利用MUS、极小修正集(minimal correction set,MCS)和极大可满足子集(maximal satisfiable subset,MSS)之间的对偶和互补关系,采用MARCO算法框架增量求解MSS 和MUS的过程中,根据已求解的MSS的交集和并集信息辅助选择节点来扩展,即通过增量的MSS信息启发用于扩展节点选择以加速MUS枚举,这一过程同时利于算法找到更多的MSS,在枚举过程中新识别出的MSS又能辅助下一轮扩展节点的选择,从而实现了增量信息的有效交互. 针对交互的增量信息提出2个定理及2个推论,从理论角度分析了MARCO-MSS4MUS算法的可行性,并通过MUS标准测试用例上的实验验证了算法相较于当前先进算法的优越性,在部分测试用例上的结果显示新算法的枚举效率和枚举获胜个数较已有算法均有显著的提高.
Abstract:Enumerating minimal unsatisfiable subsets (MUS) is an important issue in theoretical computer science. Given an unsatisfiable Boolean formula, the number of its MUS is exponentially related to the formula’s scale. Contemporary methods aim to identify as many MUSes as possible within appropriate time limits. Dealing with the huge search space, choosing a suitable node to expand can markedly reduce the time consumption on shrink and grow operations, thereby the algorithm could obtain better performance. This paper introduces an incremental information interaction-based MUS solving method, denoted as MARCO-MSS4MUS, which utilizes the duality and complementary relationships among MUS, minimal correction sets (MCS), and maximal satisfiable subsets (MSS). Based on the framework of MARCO algorithm, the proposed method selects a more suitable node to expand via intersection and union information of previously identified MSSes during the search, i.e., the incremental MSS information is employed as a heuristic for node selection to accelerate the enumeration of MUS. This process also benefits in identifying more MSSes, in turn, the incremental MSS information help select a better node for next exploration, thereby achieving an interaction of incremental information. The paper presents two theorems and two corollaries regarding interactive incremental information, analyzing the feasibility of our MARCO-MSS4MUS algorithm theoretically. Experiments on standard MUS benchmark instances show the superiority of the proposed algorithm over state-of-the-art methods. Both the enumeration efficiency and the number of enumerated wins of the proposed method are significantly improved compared to existing methods.
-
极小不可满足子集(minimal unsatisfiable subset,MUS)的求解是布尔可满足性问题(satisfiability,SAT)[1-4]的重要扩展问题之一. 给定一个布尔逻辑公式,当公式被判定为不可满足时,则需要进一步分析出哪些子句之间起了冲突导致公式不可满足. 而这些“冲突”正是该布尔逻辑公式所对应的极小不可满足子集. 由于MUS是基于数理逻辑表达的,因此该问题广泛应用于采用逻辑语言描述且含有冲突的系统中,其作用在于定位冲突进而解决冲突,使得系统恢复一致性. 在计算机领域,MUS求解对于电子设计自动化、形式化验证等方向具有重要意义. 例如,在软件工程领域,对一个正在开发的系统进行需求分析时,需要首先将需求使用逻辑语言进行形式化描述,再进行需求的一致性检查,即确保所有需求间具有一致性(可满足)且没有冗余,若检查出不一致(不可满足)或冗余,则最好以最小化的形式向用户展示,以暴露需求中的核心问题,从而对其做出相应的修改使得所有需求可以同时被满足,将需求形式化描述所得公式的MUS就是不一致需求的极小集合;在基于模型的诊断问题[5-7]中,当电路的实际输出与期望输出不一致时,就需要对电路中的组件进行故障诊断,将电路的系统描述、组件和输入输出信息形式化描述为一个不可满足的逻辑公式,对该公式求解其MUS即对应于电路的极小冲突集,代表着电路中存在冲突的组件集合的最小单位,而该公式的极小修正集(minimal correction set,MCS)对应于电路的诊断解,意味着去掉MCS中的组件后电路的输出正常,电路的剩余部分具有一致性. 除此之外,MUS的枚举在很多领域都有广泛的应用,如描述逻辑中的公理定位问题[8-9]、本体中的不一致检测[10-11]、软硬件验证问题[12-13]等.
本文的主要贡献为以下3个方面:
1)所提算法采用了极大可满足子集(maximal satisfiable subset,MSS)的交集和并集作为启发信息,定义了新的启发式帮助指导选择下一次扩展的节点.
2)提出了2个定理及其推论. 从理论层面分析了增量式求解MSS和MUS的过程中,MSS的交集和并集信息对于枚举MUS的效率提升的可行性.
3)提供多种时间限制下的对比实验,在MUS标准测试用例上的实验结果表明,本文所提算法MARCO-MSS4MUS可以有效利用MSS信息以加速对MUS的枚举过程,在部分用例上的枚举效率有数倍的提升效果.
1. 相关工作
MUS的枚举算法目前主要分为2类:基于碰集对偶性的方法和基于种子缩减的方法. 第1类方法主要利用了MUS和MCS互为碰集的对偶性特点,以及MSS与MCS互为补集的特点,首先计算出全部的MSS,再求其补集得到全部的MCS,最后对全部的MCS构成的集合簇求碰集得出全部的MUS,代表算法有CAMUS[14-15], DAA[16]. 第2类方法主要依赖对搜索空间的剪枝来识别MUS,代表算法有MARCO[17]及其变体[18-20]、TOME[21]算法、ReMUS[22]算法和UNIMUS[23]算法等. 其中,MARCO算法利用哈斯图结构,每找到一个节点必会将其收缩成一个MUS或扩充成一个MSS,再对搜索空间中的无解空间进行剪枝;TOME算法则将哈斯图结构看作纵向的链式结构,找寻每一条链的可满足节点和不可满足节点的交界处,收集这些节点来识别出真正的MSS和MUS;ReMUS算法则以递归的方式计算当前节点所表示集合的MUS;UNIMUS算法则是在原有搜索空间的基础上定义了一个动态的子搜索空间,使用识别出的MUS的并集的幂集与未探索空间的交集作为新的搜索空间来选择节点进行扩展. 尽管ReMUS和UNIMUS展现出良好的求解效率,但这2种算法致力于极致的MUS枚举,无法识别出任何的MSS. 尽管MSS的计算较MUS更容易,但MSS的枚举同样有着不可替代的意义[24-26]. 因此,本文将继续针对MARCO类算法框架提出新的枚举算法,充分利用搜索过程中识别出的MSS交集和并集等信息作为选择扩展节点的启发信息,辅助算法选择更合适的节点进行扩展,在此过程中利用增量的MSS信息不断优化节点选择,使得MSS和MUS之间信息的有效交互,进一步促进MUS的枚举.
2. 预备知识
本节将首先介绍不可满足的布尔逻辑公式中的3种特殊集合——MUS, MCS, MSS的概念,以及三者之间的对偶和互补关系. 之后介绍在枚举此类集合的算法中普遍采用的对搜索空间的刻画方法.
2.1 3种特殊子集及关系
定义1. 极小不可满足子集[15]. 给定一个不可满足的布尔逻辑公式F,称集合U是F的一个MUS,当且仅当 U $ \subseteq $ F,且U不可满足,$ \forall $ c $ \in $ U,U\{c}可满足.
定义2. 极大可满足子集[15]. 给定一个不可满足的布尔逻辑公式F,称集合S是F的一个MSS,当且仅当 S $ \subseteq $ F,且S可满足,$ \forall $ c $ \in $ F\S,S $ \cup ${c}不可满足.
定义3. 极小修正集[15]. 给定一个不可满足的布尔逻辑公式F,称集合C是F的一个MCS,当且仅当C $ \subseteq $ F,且F\C可满足,$ \forall $ c $ \in $ C,F\{C\{c}}不可满足.
定义4. 碰集[4]. 称集合H是集合簇Q的碰集,当且仅当H同时满足:H $ \subseteq \cup $Q′ $ \in $ Q Q′;对于 $ \forall $Q′ $ \in $ Q ,$H \cap Q' \ne \varnothing $,其中Q′代表集合簇Q中的集合.
定义5. 极小碰集[4]. 称集合簇Q的一个碰集H是极小的,当且仅当H是Q的碰集且H的任意真子集都不是Q的碰集.
从问题定义中可以看出,MSS和MCS的定义是互补的,因此布尔逻辑公式F的每个MSS在F下的补集都是F的一个MCS. 此外,MUS代表了导致公式F不可满足的子句的极小集合,而MCS代表从公式F中去除该部分后不一致性被修复的子句集合,故MCS和MUS都对应着与公式的不可满足性相关的子句集合. 已有文献[27]证明了MUS与MCS之间互为碰集的对偶关系.
2.2 搜索空间的表示
针对MUS枚举问题,给定一个含有n个子句的布尔逻辑公式F,其幂集就构成了算法的整个搜索空间,用1个节点表示F的1个子集,那么搜索空间中就有2n个节点. MARCO算法采用子句映射的方式,将每个子句映射为1个新的变量,从而形成1个新的布尔逻辑公式map来刻画搜索空间. 向上剪枝操作BlockUp和向下剪枝操作BlockDown就是向map中添加相应的子句从而对搜索空间进行剪枝. 判断一个节点是否被扩展过只需要对map中该节点所含子句所对应的映射变量赋值后进行可满足性检查. 公式map可被可视化为哈斯图,如图1所示(图示为含有4个子句的布尔逻辑公式F所对应的搜索空间). 可以看出,相比于传统方式存储2n个节点及节点之间的联系,使用逻辑公式map刻画的搜索空间大大减小了内存消耗又保证了搜索效率.
3. MARCO算法及已有变体
MARCO算法作为MUS枚举问题的经典算法,近年来已有多个改进版本. 经典MARCO算法的具体描述如算法1所示. 首先,第①行将给定的公式进行子句到变量的映射形成一个新的公式map用于表示搜索空间. 之后开始在搜索空间中寻找MUS,第②行执行一个while循环,当哈斯图中还有未探索的节点时,map为可满足的,循环终止的条件是map不可满足,即搜索空间中所有的节点都已探索过(或已被剪枝). 在循环中,算法通过调用函数getUnexplored(map)在map中找到一个未探索的节点seed,检查其可满足性. 当seed可满足时,说明seed所表示的集合是公式F的一个可满足子集,于是将seed扩展为一个MSS,并将seed所表示集合的全部子集对应的节点从哈斯图中剪枝;当seed不可满足时,意味着seed所表示的集合是F的一个不可满足子集,于是将seed收缩为一个MUS,并将seed所表示集合的全部超集对应的节点剪枝,重复此过程直到所有节点均被探索或剪枝,算法停止,所有的MUS和MSS被输出.
MARCO的现有变体主要有以下3种:第1种[18],对算法1的第③行进行改进,更改为选择一个极大的未探索节点,这样算法更偏向于先搜索不可满足的seed,且这种方式下找到的seed若可满足则一定是MSS,可以省去Grow操作;第2种[19],对循环中每轮选择的seed个数进行改进,增加一个基数为seed所代表集合一半的它的子集对应的节点作为第2个seed参与搜索,这样的改进使得算法偏向于中上层的节点优先探索;第3种[20],找到一类特殊的MSS根据其特性计算出当前可确定的全部MUS的子集,将其对应的节点剪枝,这类改进可以进一步对搜索空间进行剪枝,在一定程度上加速对MUS的枚举效率.
算法1. MARCO算法.
输入:给定的布尔逻辑公式F;
输出:已识别的MSS 集合SMSS和MUS 集合SMUS.
① map←F中子句映射为变量形成的新公式;
② while map可满足do
③ seed←getUnexplored (map);
④ if seed是可满足的
⑤ SMSS←Grow (seed)/*扩充操作*/
⑥ 输出SMSS;
⑦ map←map∧BlockDown (seed);
⑧ else /*seed不可满足*/
⑨ SMUS←Shrink (seed);/*收缩操作*/
⑩ 输出SMUS;
⑪ map←map∧BlockUp (seed);
⑫ end if
⑬ end while
4. MARCO-MSS4MUS
基于第3节对MARCO已有改进的分析,本文在结合上述改进的基础上提出新的算法MARCO-MSS4MUS. 本节首先介绍所提算法的思想与理论依据,之后给出算法的详细描述,如算法2所示.
由于MUS, MSS, MCS这3种集合之间均存在紧密的联系,在算法枚举的过程中可以充分利用MSS的信息来促进MUS的枚举. 具体而言,由于MSS与MCS互为补集,而MCS又与MUS互为碰集,于是可以利用MCS建立起MSS与MUS之间信息传递的桥梁. 基于上述思想,结合增量式求解碰集的特点,给出以下定理、推论及证明过程. 其中,定理1和定理2对应于问题的全部MSS和全部MUS均被找出时的情况,而推论1和推论2则对应于部分MSS和部分MUS被找出时的情况.
定理1. 令集合SIMSS表示所求出的MSS的交集,当全部的MSS被求出时,出现在集合SIMSS中的元素一定不会出现在任何MUS中.
证明. 反证法. 假设存在一个元素a∈SIMSS且出现在MUS集合 U1中. 已知a∈U1,由于MUS与MCS互为极小碰集,根据极小碰集的定义,则必有一个MCS集合 C1,满足a∈C1∩U1. 于是一定有a∈C1. 而已知a∈SIMSS,于是对任意的MSS集合 S,都有a∈S,根据MSS与MCS互补的性质,对任意的MCS集合 C,都有a $ \notin $ C,与a∈C1相矛盾. 故原假设不成立,不存在这样的元素a既出现在SIMSS中又出现在某一MUS中. 证毕.
推论1. 令集合SIMSS表示所求出的MSS的交集,在增量式得到MSS的过程中,当前集合SIMSS中的元素一定不会出现在部分MUS中.
证明. 反证法. 类似地,假设存在一个元素a∈SIMSS且a出现在全部MUS中. 根据a∈SIMSS,有a∈当前找到的所有MSS,又由于MSS与MCS互补,有a$ \notin $当前找到的任意MCS. 根据a出现在全部MUS中及MUS与MCS互为极小碰集的关系,有{a}必是一个MCS,与前面根据a∈SIMSS的条件推断出a$ \notin $当前找到的任意MCS的结论相矛盾,故原假设不成立. 证毕.
定理2. 令集合SUMSS表示所求出的MSS的并集,令集合SCoUMSS为SUMSS的补集. 当全部的MSS被求出时,对任意元素u∈SCoUMSS,一定存在一个MUS集合 U满足u∈U.
证明. 对于任意元素u∈SCoUMSS,必有u$ \notin $SUMSS,于是有u$ \notin $任意MSS S. 由于MSS与MCS互为补集,于是有u ∈所有MCS集合 C. 由于MCS与MUS互为极小碰集,则根据极小碰集的定义,对任意u∈C,必存在一个MUS集合 U1,满足u∈U1. 证毕.
推论2. 令集合SUMSS表示所求出的MSS的并集,令集合SCoUMSS为SUMSS的补集. 在增量式得到MSS的过程中,当前集合SCoUMSS中的元素一定出现在部分MUS中.
证明. 反证法. 假设存在一个元素a∈SCoUMSS且a不会出现在任何MUS中. 根据a∈SCoUMSS,有a$ \notin $SUMSS,有a$ \notin $当前找到的任意MSS,又由于MSS与MCS互为补集,有a∈当前找到的全部MCS,又由于MUS与MCS互为极小碰集,根据碰集定义可知,一定存在一个MUS集合 U′ 满足a∈U′ ,与假设中a不会出现在任何MUS中相矛盾. 故假设不成立. 证毕.
基于定理1及其推论1对MSS交集的理论分析、定理2和其推论2对MSS并集的补集的理论分析,在算法每轮选择扩展节点seed时,引入一个新的启发式在原本的seed基础上做出相应调整:将seed与MSS的交集即集合SIMSS做差集后,再与MSS的并集的补集即集合SCoUMSS做并集,得到新的扩展节点seed′. 判断新节点是否未被探索过:若未探索则扩展seed′而非seed;否则,扩展seed. 在实验中发现如果seed与集合SIMSS直接做差集得到的seed′节点会过小,位于哈斯图的较底部,使得算法将过于偏向对MSS的枚举,于是调整为seed与集合SIMSS的子集做差集,子集选择基数为集合SIMSS基数1/3的任意子集. 引入启发式后的seed′更加符合MUS的特点,从一定程度上减小收缩操作的时间消耗,更快收缩为一个MUS.
算法2. MARCO-MSS4MUS算法.
输入:给定的布尔逻辑公式F;
输出:已识别的MSS集合 SMSS和MUS集合 SMUS.
① map←F中子句映射为变量形成的新公式;
② while map可满足do
③ seed←getUnexploredMax (map);
④ if seed是可满足的
⑤ SMSS←seed;
⑥ 输出SMSS;
⑦ SIMSS←SIMSS ∩ SMSS;
⑧ SUMSS←SUMSS ∪ SMSS;
⑨ map←map∧BlockDown (seed);
⑩ if seed 是关键MSS
⑪ SMCS←co (seed);
⑫ subU←subU∪SMCS;
⑬ map←map∧BlockDown (subU);
⑭ end if
⑮ else /*seed不可满足*/
⑯ seed′ ←seed – sub (SIMSS)∪co (SUMSS);
⑰ if seed′ 未被探索
⑱ if seed′ 可满足
⑲ SMSS←Grow (seed′);
⑳ 输出SMSS;
㉑ SIMSS←SIMSS ∩ SMSS;
㉒ SUMSS←SUMSS ∪ SMSS;
㉓ map←map∧BlockDown (seed′);
㉔ else /* seed′ 不可满足*/
㉕ SMUS←Shrink (seed′);
㉖ 输出SMUS;
㉗ map←map∧BlockUp (seed′);
㉘ end if
㉙ else /*seed′已被探索*/
㉚ SMUS←Shrink (seed);
㉛ 输出SMUS;
㉜ map←map∧BlockUp (seed);
㉝ end if
㉞ end if
㉟ end while
算法2是本文所提算法MARCO-MSS4MUS的伪代码描述. 在经典MARCO算法的基础上,第③行选择seed节点使用的是已有改进中的第1种,即选择极大未探索的seed版本;第⑩~⑭行使用的是已有改进中的第3种,找到一类特殊的MSS即关键MSS,由于关键MSS对应的MCS为单元素集合,将关键MSS的补集元素加入集合subU中,将subU对应的节点剪枝. 其中,co (seed)指seed的补集,sub (seed)指seed的子集. 本文的改进主要体现在:1)第⑦⑧行、第
2122 行,算法每找到一个新的MSS时,更新MSS交集SIMSS和MSS并集SUMSS;2)在算法找到的待探索节点seed不可满足时,不直接执行下一步收缩操作Shrink (seed),而是通过新的启发式在seed的基础上先与SIMSS的子集作差集,再与SUMSS的补集作并集,得到新的探索节点seed′(第⑯行). 若seed′已探索,则还是选择seed来探索;否则,使用seed′代替seed作为探索节点. MARCO-MSS4MUS算法没有改变经典MARCO算法及其变体的剪枝方式,而是进一步利用了搜索过程中获取的MSS信息来改进所选择的探索节点,从减少收缩和扩充操作的执行时间的角度加速了MUS的枚举效率.5. 实 验
本节将所提出的新算法MARCO-MSS4MUS与当前最先进的算法MARCO+, MARCO-MAM, MARCO-ABC进行对比. 对比算法MARCO+源代码来自网页http://www.iwu.edu/∼mliffito/marco/,MARCO-MAM和MARCO-ABC源代码来自网页https://github.com/jiangluyu1998/ABC-scheme-for-MUS. 实验设备为1台60 GB RAM、Intel Xeon E5-2690v4 2.6 GHz的CPU、64位Ubuntu 18.04版本Linux操作系统的主机. 算法所用的编程语言均为Python 3.7版本,可满足性检查过程调用的MiniSAT求解器[28]为C++语言编写. 采用标准测试用例SAT11中的MUS实例(下载网址:http://www.cril.univ-artois.fr/SAT11/)对算法进行测试,并对每组实验设置了3种时间限制,分别为0.5 h, 1 h, 2 h.
表1、表2、表3分别对应0.5 h, 1 h, 2 h时间限制下各个算法所枚举出的MUS个数的对比结果,表中枚举个数最多的结果采用加粗表示. 实验结果显示,在算法执行的前期,所提算法枚举MUS的效率在部分实例上并没有已有的先进算法表现好,但随着运行时间的增加,所提算法对MUS的枚举效率出现了显著的提升,在大部分实例上的结果远远优于对比算法. 这样的现象应用本文的理论分析也是可解释的:由于算法是基于极大化版本的MARCO算法,因此在搜索初期,算法优先从哈斯图的顶层选择节点来扩展,因此在算法初期找到的MSS往往偏大,这就使得MSS的交集可能偏大,MSS的并集也偏大,MSS并集的补集则偏小. 于是,所提算法的启发式即在原先选择的待探索节点基础上先与MSS交集做差集,再与MSS并集的补集做并集得到的新的待扩展节点就会偏小,使得算法在初期更倾向于对MSS的枚举,当算法找到的MSS数量逐渐积累后,结合其交集和并集得到的启发式的信息才会更偏向于MUS,此时,算法将大量搜索出MUS,这也与本文的实验结果相吻合. 综上,本文所提算法的特点是在搜索初期会更偏向于搜索MSS,在搜索到的MSS逐渐积累后,算法对MUS的枚举效率会呈现显著提升.
测试用例 本文算法 MARCO+[18] MARCO-
MAM[19]MARCO-
ABC[20]fdmus_b14_134 491 158 181 173 fdmus_b14_141 53 82 83 84 fdmus_b14_210 1 80 78 80 fdmus_b15_291 54 51 52 53 fdmus_b15_294 51 47 44 47 fdmus_b15_304 1 32 33 31 fdmus_b15_421 1 151 142 157 fdmus_b15_463 2 174 191 189 fdmus_b17_ 1037 1 338 539 500 fdmus_b17_ 1324 2 58 77 57 fdmus_b17_ 1456 2 195 178 186 fdmus_b17_420 197 158 154 161 fdmus_b20_141 1 16 17 18 fdmus_b20_171 1 20 19 21 fdmus_b20_238 145 44 48 45 fdmus_b20_341 945 188 190 176 fdmus_b20_349 1 33 31 33 fdmus_b20_381 1 29 32 31 fdmus_b20_492 215 38 40 40 fdmus_b20_498 520 61 65 65 fdmus_b21_111 1 14 13 14 fdmus_b21_112 1 14 13 15 fdmus_b21_167 1 35 31 34 fdmus_b21_481 115 31 28 31 fdmus_b21_96 94 115 118 118 fdmus_b22_102 1 34 36 36 fdmus_b22_113 1 12 12 12 fdmus_b22_133 1 46 40 54 fdmus_b22_172 1 21 22 23 fdmus_b22_241 61 29 27 30 fdmus_b22_356 1 14 14 14 fdmus_b22_488 480 51 47 51 fdmus_b22_600 1 15 14 20 fdmus_b22_662 1 23 23 20 加粗数值表示MUS枚举个数的最优结果. 测试用例 本文算法 MARCO+[18] MARCO-
MAM[19]MARCO-
ABC[20]fdmus_b14_134 1367 513 574 584 fdmus_b14_141 484 199 194 203 fdmus_b14_210 4 205 183 204 fdmus_b15_291 345 102 109 108 fdmus_b15_294 190 100 93 100 fdmus_b15_304 175 59 53 63 fdmus_b15_421 395 294 305 327 fdmus_b15_463 2 369 420 405 fdmus_b17_ 1037 938 338 1082 1085 fdmus_b17_ 1324 188 117 149 116 fdmus_b17_ 1456 2 386 383 374 fdmus_b17_420 537 318 323 327 fdmus_b20_141 1 32 35 36 fdmus_b20_171 1 38 35 38 fdmus_b20_238 500 93 92 92 fdmus_b20_341 2424 629 600 639 fdmus_b20_349 1 66 68 63 fdmus_b20_381 1 66 71 67 fdmus_b20_492 806 88 89 86 fdmus_b20_498 1528 179 176 200 fdmus_b21_111 1 27 29 29 fdmus_b21_112 1 26 26 27 fdmus_b21_167 1 70 63 70 fdmus_b21_481 924 64 63 65 fdmus_b21_96 987 300 309 311 fdmus_b22_102 1 63 67 70 fdmus_b22_113 1 23 23 25 fdmus_b22_133 3 100 98 108 fdmus_b22_172 1 42 41 42 fdmus_b22_241 313 60 60 60 fdmus_b22_356 1 28 27 27 fdmus_b22_488 1524 110 106 122 fdmus_b22_600 1 26 34 29 fdmus_b22_662 1 47 44 38 加粗数值表示MUS枚举个数的最优结果. 测试用例 本文算法 MARCO+[18] MARCO-
MAM[19]MARCO-
ABC[20]fdmus_b14_134 2852 1566 1486 1664 fdmus_b14_141 1422 642 598 642 fdmus_b14_210 467 637 611 609 fdmus_b15_291 587 231 252 253 fdmus_b15_294 762 224 208 218 fdmus_b15_304 468 143 124 144 fdmus_b15_421 1398 581 689 673 fdmus_b15_463 2 764 787 823 fdmus_b17_ 1037 3593 338 2362 2356 fdmus_b17_ 1324 473 228 290 229 fdmus_b17_ 1456 2 766 746 750 fdmus_b17_420 1082 738 664 673 fdmus_b20_141 1 67 70 71 fdmus_b20_171 1 74 74 74 fdmus_b20_238 952 222 219 236 fdmus_b20_341 5424 1562 1496 1623 fdmus_b20_349 3 141 157 149 fdmus_b20_381 3 162 170 158 fdmus_b20_492 3043 352 375 322 fdmus_b20_498 3091 552 510 518 fdmus_b21_111 1 55 57 60 fdmus_b21_112 1 53 52 53 fdmus_b21_167 24 153 151 148 fdmus_b21_481 2343 224 152 175 fdmus_b21_96 1837 715 710 738 fdmus_b22_102 4 136 135 133 fdmus_b22_113 1 45 47 49 fdmus_b22_133 259 226 223 229 fdmus_b22_172 1 88 89 86 fdmus_b22_241 898 145 136 142 fdmus_b22_356 1 63 58 62 fdmus_b22_488 3426 428 390 476 fdmus_b22_600 1 62 62 69 fdmus_b22_662 1 81 76 75 加粗数值表示MUS枚举个数的最优结果. 为更清晰地可视化实验结果,对表1、表2、表3的结果分别计算获胜个数并绘制成柱状图,如图2所示. 每个算法在每种时间限制下的获胜个数即在各个测试用例下,若该算法枚举MUS个数最多则记为获胜1次,统计所有测试用例下的总获胜次数. 从图2中可以看出,所提算法的获胜个数仅在0.5 h的时间限制下没有超过对比算法MARCO-ABC,但在1 h和2 h的时间限制下的实验结果中,本文所提算法MARCO-MSS4MUS的获胜个数均优于其他对比算法. 这也印证了在前文中的分析,MARCO-MSS4MUS算法的启发式引导它在搜索的前期更偏向于收集更多的MSS,从而导致MUS的枚举个数极少,但在其收集到足够多的MSS后,充分利用已有MSS的信息将引导算法逐渐偏向于搜索MUS,使得算法枚举MUS的效率呈现出显著的增长.
6. 结 论
本文提出了一种针对MUS枚举问题的新算法MARCO-MSS4MUS. 基于经典MARCO框架及已有改进,在增量式求解MUS和MSS的过程中,进一步利用了搜索过程中枚举出的MSS的交集和并集作为启发式信息,指导算法对于待扩展节点的选择,从而引导搜索逐渐朝着偏向MUS的方向进行,减少收缩和扩充操作的耗时以达到加速MUS枚举的目的. 提出2个新的定理及其推论为所提算法的有效性提供了理论依据,从理论角度说明了在MSS交集中的元素不一定出现在MUS中,在MSS并集的补集中的元素一定出现在部分MUS中,因此基于以上信息对待扩展节点进行相应的集合运算操作得到新的待扩展节点将更倾向于找到一个MUS. 最后,标准测试用例的实验表明,所提出的算法MARCO-MSS4MUS在枚举获胜个数和枚举效率2方面均较已有算法有显著的提高.
作者贡献声明:蒋璐宇提出了算法思路和实验方案,负责代码编写、攥写并修改论文;欧阳丹彤负责确定选题及指导论文写作;张奇负责文献资料的查阅和整理;太然负责整理实验数据;张立明负责对论文提出修改意见.
-
表 1 0.5 h时间限制下各算法枚举的MUS个数对比
Table 1 Compared Results on the Number of MUS Under 0.5 h Time Limit
测试用例 本文算法 MARCO+[18] MARCO-
MAM[19]MARCO-
ABC[20]fdmus_b14_134 491 158 181 173 fdmus_b14_141 53 82 83 84 fdmus_b14_210 1 80 78 80 fdmus_b15_291 54 51 52 53 fdmus_b15_294 51 47 44 47 fdmus_b15_304 1 32 33 31 fdmus_b15_421 1 151 142 157 fdmus_b15_463 2 174 191 189 fdmus_b17_ 1037 1 338 539 500 fdmus_b17_ 1324 2 58 77 57 fdmus_b17_ 1456 2 195 178 186 fdmus_b17_420 197 158 154 161 fdmus_b20_141 1 16 17 18 fdmus_b20_171 1 20 19 21 fdmus_b20_238 145 44 48 45 fdmus_b20_341 945 188 190 176 fdmus_b20_349 1 33 31 33 fdmus_b20_381 1 29 32 31 fdmus_b20_492 215 38 40 40 fdmus_b20_498 520 61 65 65 fdmus_b21_111 1 14 13 14 fdmus_b21_112 1 14 13 15 fdmus_b21_167 1 35 31 34 fdmus_b21_481 115 31 28 31 fdmus_b21_96 94 115 118 118 fdmus_b22_102 1 34 36 36 fdmus_b22_113 1 12 12 12 fdmus_b22_133 1 46 40 54 fdmus_b22_172 1 21 22 23 fdmus_b22_241 61 29 27 30 fdmus_b22_356 1 14 14 14 fdmus_b22_488 480 51 47 51 fdmus_b22_600 1 15 14 20 fdmus_b22_662 1 23 23 20 加粗数值表示MUS枚举个数的最优结果. 表 2 1 h时间限制下各算法枚举的MUS个数对比
Table 2 Compared Results on the Number of MUS Under 1 h Time Limit
测试用例 本文算法 MARCO+[18] MARCO-
MAM[19]MARCO-
ABC[20]fdmus_b14_134 1367 513 574 584 fdmus_b14_141 484 199 194 203 fdmus_b14_210 4 205 183 204 fdmus_b15_291 345 102 109 108 fdmus_b15_294 190 100 93 100 fdmus_b15_304 175 59 53 63 fdmus_b15_421 395 294 305 327 fdmus_b15_463 2 369 420 405 fdmus_b17_ 1037 938 338 1082 1085 fdmus_b17_ 1324 188 117 149 116 fdmus_b17_ 1456 2 386 383 374 fdmus_b17_420 537 318 323 327 fdmus_b20_141 1 32 35 36 fdmus_b20_171 1 38 35 38 fdmus_b20_238 500 93 92 92 fdmus_b20_341 2424 629 600 639 fdmus_b20_349 1 66 68 63 fdmus_b20_381 1 66 71 67 fdmus_b20_492 806 88 89 86 fdmus_b20_498 1528 179 176 200 fdmus_b21_111 1 27 29 29 fdmus_b21_112 1 26 26 27 fdmus_b21_167 1 70 63 70 fdmus_b21_481 924 64 63 65 fdmus_b21_96 987 300 309 311 fdmus_b22_102 1 63 67 70 fdmus_b22_113 1 23 23 25 fdmus_b22_133 3 100 98 108 fdmus_b22_172 1 42 41 42 fdmus_b22_241 313 60 60 60 fdmus_b22_356 1 28 27 27 fdmus_b22_488 1524 110 106 122 fdmus_b22_600 1 26 34 29 fdmus_b22_662 1 47 44 38 加粗数值表示MUS枚举个数的最优结果. 表 3 2 h时间限制下各算法枚举的MUS个数对比
Table 3 Compared Results on the Number of MUS Under 2 h Time Limit
测试用例 本文算法 MARCO+[18] MARCO-
MAM[19]MARCO-
ABC[20]fdmus_b14_134 2852 1566 1486 1664 fdmus_b14_141 1422 642 598 642 fdmus_b14_210 467 637 611 609 fdmus_b15_291 587 231 252 253 fdmus_b15_294 762 224 208 218 fdmus_b15_304 468 143 124 144 fdmus_b15_421 1398 581 689 673 fdmus_b15_463 2 764 787 823 fdmus_b17_ 1037 3593 338 2362 2356 fdmus_b17_ 1324 473 228 290 229 fdmus_b17_ 1456 2 766 746 750 fdmus_b17_420 1082 738 664 673 fdmus_b20_141 1 67 70 71 fdmus_b20_171 1 74 74 74 fdmus_b20_238 952 222 219 236 fdmus_b20_341 5424 1562 1496 1623 fdmus_b20_349 3 141 157 149 fdmus_b20_381 3 162 170 158 fdmus_b20_492 3043 352 375 322 fdmus_b20_498 3091 552 510 518 fdmus_b21_111 1 55 57 60 fdmus_b21_112 1 53 52 53 fdmus_b21_167 24 153 151 148 fdmus_b21_481 2343 224 152 175 fdmus_b21_96 1837 715 710 738 fdmus_b22_102 4 136 135 133 fdmus_b22_113 1 45 47 49 fdmus_b22_133 259 226 223 229 fdmus_b22_172 1 88 89 86 fdmus_b22_241 898 145 136 142 fdmus_b22_356 1 63 58 62 fdmus_b22_488 3426 428 390 476 fdmus_b22_600 1 62 62 69 fdmus_b22_662 1 81 76 75 加粗数值表示MUS枚举个数的最优结果. -
[1] Cai Shaowei, Zhang Xindi. Deep cooperation of CDCL and local search for SAT[C]//Proc of the 24th Int Conf on Theory and Applications of Satisfiability Testing. Berlin: Springer, 2021: 64−81
[2] Cai Shaowei, Zhang Xindi, Fleury M, et al. Better decision heuristics in CDCL through local search and target phases[J]. Journal of Artificial Intelligence Research, 2022, 74: 1515−1563 doi: 10.1613/jair.1.13666
[3] Zheng Jiongzhi, He Kun, Zhou Jianrong, et al. BandMaxSAT: A local search MaxSAT solver with multi-armed bandit[C]//Proc of the 31st Int Joint Conf on Artificial Intelligence. Freiburg: IJCAI, 2022: 1901–1907
[4] 王荣全,欧阳丹彤,王艺源,等. 结合DOEC极小化策略的SAT求解极小碰集方法[J],计算机研究与发展,2018,55(6):1273–1281 Wang Rongquan, Ouyang Dantong, Wang Yiyuan, et al. Solving minimal hitting sets method with SAT based on DOEC minimization[J]. Journal of Computer Research and Development, 2018, 55(6): 1273–1281 (in Chinese)
[5] Metodi A, Stern R, Kalech M, et al. A novel sat-based approach to model based diagnosis[J]. Journal of Artificial Intelligence Research, 2014, 51: 377−411 doi: 10.1613/jair.4503
[6] 田乃予,欧阳丹彤,刘梦,等. 基于子集一致性检测的诊断解极小性判定方法[J],计算机研究与发展,2019,56(7):1396–1407 Tian Naiyu, Ouyang Dantong, Liu Meng, et al. A method of minimality-checking of diagnosis based on subset consistency detection[J]. Journal of Computer Research and Development, 2019, 56(7): 1396–1407 (in Chinese)
[7] Zhou Huisi, Ouyang Dantong, Zhao Xiangfu, et al. Two compacted models for efficient model-based diagnosis[C]//Proc of the 36th AAAI Conference on Artificial Intelligence. Palo Alto, CA: AAAI, 2022: 3885–3893
[8] Ouyang Dantong, Liao Mengting, Ye Yuxin. Lightweight axiom pinpointing via replicated driver and customized SAT-solving[J]. Frontiers of Computer Science, 2023, 17(2): 172315 doi: 10.1007/s11704-022-1360-x
[9] Arif M F, Mencía C, Marques-Silva J. Efficient MUS enumeration of Horn formulae with applications to axiom pinpointing[C]//Proc of the 18th Int Conf on Theory and Applications of Satisfiability Testing. Berlin: Springer, 2015: 324–342
[10] Hunter A, Konieczny S. On the measure of conflicts: Shapley inconsistency values[J]. Artificial Intelligence, 2010, 174(14): 1007−1026 doi: 10.1016/j.artint.2010.06.001
[11] Xiao Guohui, Ma Yue. Inconsistency measurement based on variables in minimal unsatisfiable subsets[C]//Proc of the 20th European Conf on Artificial Intelligence. Ohmsha: IOS Press, 2012: 864–869
[12] Shazli S Z, Tahoori M B. Using Boolean satisfiability for computing soft error rates in early design stages[J]. Microelectronics Reliability, 2010, 50(1): 149−159 doi: 10.1016/j.microrel.2009.08.006
[13] Andraus Z, Liffiton M, Sakallah K. Reveal: A formal verification tool for Verilog designs[C]//Proc of the 15th Int Conf on Logic for Programming Artificial Intelligence and Reasoning. Berlin: Springer, 2008: 343–352
[14] Liffiton M, Sakallah K. On finding all minimally unsatisfiable subformulas[G]//LNCS 3569: Proc of the 8th Int Conf on Theory & Applications of Satisfiability Testing. Berlin: Springer, 2005: 173–186
[15] Liffiton M, Sakallah K. Algorithms for computing minimal unsatisfiable subsets of constraints[J]. Journal of Automated Reasoning, 2008, 40(1): 1−33 doi: 10.1007/s10817-007-9084-z
[16] Bailey J, Stuckey P. Discovery of minimal unsatisfiable subsets of constraints using hitting set dualization[C]//Proc of the 7th Int Workshop on Practical Aspects of Declarative Languages. Berlin: Springer, 2005: 174–186
[17] Liffiton M, Malik A. Enumerating infeasibility: Finding multiple MUSes quickly[C]//Proc of the 10th Int Conf on AI and OR Techniques in Constriant Programming for Combinatorial Optimization Problems. Berlin: Springer, 2013: 160–175
[18] Liffiton M, Previti A, Malik A, et al. Fast, flexible MUS enumeration[J]. Constraints, 2016, 21(2): 223−250 doi: 10.1007/s10601-015-9183-0
[19] 欧阳丹彤,高菡,田乃予,等. 基于双模型的MUS求解方法[J],计算机研究与发展,2019,56(12):2623−2631 Ouyang Dantong, Gao Han, Tian Naiyu, et al. MUS enumeration based on double-model[J]. Journal of Computer Research and Development, 2019, 56(12): 2623–2631 (in Chinese)
[20] 蒋璐宇,欧阳丹彤,董博文,等. 针对MUS求解问题的加强剪枝策略[J],软件学报,2024,35(4):1964−1979 Jiang Luyu, Ouyang Dantong, Dong Bowen, et al. Enhanced pruning scheme for enumerating MUS[J]. Journal of Software, 2024, 35(4): 1964−1979 (in Chinese)
[21] Bendík J, Benes N, Cerna I, et al. Tunable online MUS/MSS enumeration[G]//LIPIcs 65: Proc of the 36th IARCS Annual Conf on Foundations of Software Technology and Theoretical Computer Science. Dagstuhl, Germany: Schloss Dagstuhl--Leibniz-Zentrum für Informatik, 2016: 50: 1–50: 13
[22] Bendík J, Cerna I, Benes N. Recursive online enumeration of all minimal unsatisfiable subsets[G]//LNCS 11138: Proc of the 16th Int Symp on Automated Technology for Verification and Analysis. Berlin: Springer, 2018: 143–159
[23] Bendík J, Cerna I. Replication-guided enumeration of minimal unsatisfiable subsets[C]//Proc of the 26th Int Conf on Principles and Practice of Constraint Programming. Berlin: Springer, 2020: 37–54
[24] Bendík J, Cerna I. Rotation based MSS/MCS enumeration[C]//Proc of the 23rd Int Conf on Logic for Programming, Artificial Intelligence and Reasoning. Stockport, UK: EasyChair, 2020: 120–137
[25] Bendík J, Meel K. Counting maximal satisfiable subsets[C]//Proc of the 35th AAAI Conf on Artificial Intelligence. Palo Alto, CA: AAAI, 2021: 3651–3660
[26] Bendík J. On Decomposition of maximal satisfiable subsets[C]//Proc of the 21st Conf on Formal Methods in Computer Aided Design. Piscataway, NJ: IEEE, 2021: 212−221
[27] Previti A, Marques-Silva J. Partial MUS enumeration[C]//Proc of the 27th AAAI Conf on Artificial Intelligence. Palo Alto, CA: AAAI, 2013: 818–825
[28] Een N, Sorensson N. An extensible SAT-solver[G]//LNCS 2919: Proc of the 6th Int Conf on Theory and Applications of Satisfiability Testing. Berlin: Springer, 2004: 502–518