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