结合DOEC极小化策略的SAT求解极小碰集方法

在基于模型诊断中，诊断解通常是根据极小冲突集合簇进行相应的计算得到所有的极小碰集，所以提高极小碰集的求解效率是模型诊断的核心问题.因此提出结合基于元素覆盖集合度(degree of element coverage, DOEC)极小化策略的SAT求解极小碰集的方法SAT-MHS(satisfiability problem-minimal hitting sets).首先，方法SAT-MHS将碰集求解问题转换成SAT问题,即把所有的冲突集合以子句形式表示成SAT的输入CNF进行迭代求解.其次,提出比现有的基于子超集检测极小化策略(sub-superset detecting minimization, SSDM)更为高效的DOEC极小化策略进行极小化处理.由实验数据可见，与SSDM极小化策略相比，其优点是缩减了求解空间和迭代求解次数，尤其当求解规模较大问题时，其极小化效率越高.主要是因为其极小化不会随着待求解问题规模的增加而增加，而是只与冲突集合簇的大小相关，因此时间复杂度较低.实验结果表明，对于一些较大的实例，与目前效率最好的Boolean方法相比，SAT-MHS方法高效且易于实现，求解速度能提高10~20倍，DOEC极小化策略对比传统SSDM极小化策略能达到40倍左右.

Solving Minimal Hitting Sets Method with SAT Based on DOEC Minimization

In the model-based diagnosis, the minimal conflict sets is employed to find all corresponding minimal hitting sets. Therefore, how to improve the efficiency of obtaining all minimal hitting sets is a great important issue. In this paper, we propose a new method called SAT-MHS, which is mainly based on the transform method and the set-degree of element coverage(DOEC) strategy. There are two main innivations of this paper. Firstly, SAT-MHS transforms a hitting set problem into the SAT problem, which is a new direction to solve this problem. All the minimal conflict sets are expressed in the form of clauses as the input CNF of the SAT. Secondly, compared with the previous sub-superset detecting minimization (SSDM) strategy, the proposed DOEC strategy can effectively reduce both of solution space and the number of iterations. In details, the time consumption of DOEC is along with the number of all minimal conflict sets, not depending on the size of the given problem.Experimental results show that SAT-MHS outperforms the previous state-of-the-art method and the time speed ratio of SAT-MHS rises to 10-20 times, especially for some large instances. Moreover, we also carry out extensive experiments to demonstrate that the performance of DOEC strategy is better than SSDM, even up to about 40 times.