一种面向知识编译的OBDD构造方法  

An OBDD Construction Method for Knowledge Compilation

作　　者：王金艳[1,2] 胡春 高健 WANG Jinyan;HU Chun;GAO Jian(Guangxi Key Lab of Multisource Information Mining and Security(Guangxi Normal University),Guilin Guangxi 541004,China;School of Computer Science and Engineering,Guangxi Normal University,Guilin Guangxi 541004,China;School of Information Science and Technology,Dalian Maritime University,Dalian Liaoning 116026,China)

机构地区：[1]广西多源信息挖掘与安全重点实验室(广西师范大学),广西桂林541004 [2]广西师范大学计算机科学与工程学院,广西桂林541004 [3]大连海事大学信息科学技术学院,辽宁大连116026

出　　处：《广西师范大学学报（自然科学版）》2021年第4期47-54,共8页Journal of Guangxi Normal University:Natural Science Edition

基　　金：国家自然科学基金(61763003);广西多源信息挖掘与安全重点实验室系统性研究课题(19-A-02-01);广西研究生教育创新计划(XYCSZ2020072);广西高等学校千名中青年骨干教师培育计划;“八桂学者”工程专项;广西区域多源信息集成与智能处理协同创新中心项目。

摘　　要：知识编译作为人工智能的重要方向,在实时查询和推理中起重要作用。有序二元决策图(ordered binary decision diagram,OBDD)是知识编译领域中一个主要的编译目标语言,已被广泛用于编译诸多实际的可满足性问题(SAT)。近年来,OBDD的构造技术得到了深入研究,其目的是减少目标OBDD的大小并且缩短编译时间。OBDD的构造方式是影响编译效率的重要因素,为了提高编译时间效率,本文提出一种改进的OBDD构造算法,该算法将SAT问题的子句编译成OBDD的表示形式,并将这些OBDD合并成一个整体。不同于传统的合并算法逐一将OBDD合并到目标OBDD中,本文将一些OBDD先进行合并,然后再整合到目标OBDD中。对随机生成的SAT实例和产品配置问题的实验表明,本文提出的OBDD构造算法的性能优于原始算法。Knowledge compilation,as a key direction of artificial intelligence,plays an important role in on-line requirement and reasoning.The ordered binary decision diagram(OBDD)is a main target language in knowledge compilation,which has been widely used to compile many real-world satisfiability(SAT)problems.The construction algorithms for OBDDs are deeply studied in the past years,and the purposes are to decrease the size of target OBDD and shorten the compilation time.The construction for OBDD is an important factor affecting the efficiency of compilation.To improve the time efficiency,an improved construction algorithm for OBDDs is proposed.The algorithm compiles the causes in SAT problem into OBDDs and then combines them into a whole OBDD.Different from the traditional algorithm which combines these OBDDs into a target OBDD one by one,this approach first combines some OBDDs into larger OBDDs and then they are merged into a garget OBDD.The experiments on randomly generated SAT instances and configuration problems indicate that the proposed OBDD construction algorithm performs better than the original algorithm.

关 键 词：人工智能 知识编译 有序二元决策图 可满足性问题 离线预处理 在线推理 

分 类 号：TP301[自动化与计算机技术—计算机系统结构] TP181[自动化与计算机技术—计算机科学与技术]