ISSN 1000-1239 CN 11-1777/TP

Journal of Computer Research and Development ›› 2018, Vol. 55 ›› Issue (6): 1273-1281.doi: 10.7544/issn1000-1239.2018.20160809

Previous Articles     Next Articles

Solving Minimal Hitting Sets Method with SAT Based on DOEC Minimization

Wang Rongquan,Ouyang Dantong,Wang Yiyuan,Liu Siguang, Zhang Liming   

  1. (College of Computer Science and Technology, Jilin University, Changchun 130012) (Key Laboratory of Symbolic Computation and Knowledge Engineering (Jilin University), Ministry of Education, Changchun 130012)
  • Online:2018-06-01

Abstract: 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.

Key words: model-based diagnosis, minimal hitting sets, satisfiability problem (SAT), hitting minimization, set-covering

CLC Number: