结合DOEC极小化策略的SAT求解极小碰集方法
2018-06-08王荣全欧阳丹彤王艺源刘思光张立明
王荣全 欧阳丹彤 王艺源 刘思光 张立明
(吉林大学计算机科学与技术学院 长春 130012) (符号计算与知识工程教育部重点实验室(吉林大学) 长春 130012) (wangrongquanjlu@163.com)
人工智能专家Console等人[1]指出基于模型诊断(model based diagnosis, MBD)的研究对整个人工智能领域的研究有着重要的作用.学者Struss[2]称基于模型诊断是人工智能领域极富有挑战性和具有检验性的课题.基于模型诊断的核心步骤是根据系统的描述和观测,得到极小冲突集合簇[3],然后以其为输入并利用碰集(hitting set, HS)的求解方法计算得到系统所对应的极小诊断解即极小碰集(minimal hitting set, MHS),因此求解MHS问题是模型诊断中比较核心的问题之一[4].此外很多的实际和理论问题都可以转化为MHS问题[5-6],如极小集合覆盖和极小顶点覆盖等极小覆盖问题均是极小碰集的特殊形式、师生选课问题、蕴涵推理问题以及智能规划的核心问题.
碰集(hitting set, HS)问题最早是由加州大学伯克利分校的计算机专家Karp在1972年提出,随后MBD专家Reiter[7]首次提出了一种求解极小碰集的方法HS-Tree,但该方法基于枚举树并遍历整棵枚举树导致效率较低,且会因剪枝丢失解.因此,Greiner等人[8]提出HS-DAG方法,优化并改进了HS-Tree方法的剪枝策略,虽然解决因剪枝而丢失解,但因新的剪枝规则的应用导致计算复杂度大幅度增加.随着对极小碰集问题的深入探索研究,许多新的求解方法陆续被提出.2001年,Wotawa[9]通过改进HS-Tree方法提出了HST-Tree方法,虽然效率提升,但其通用性降低,并未彻底解决丢解的问题,空间复杂度较高;2003年,姜云飞等人[10]提……
