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

王金艳; 胡春; 高健

doi:10.16088/j.issn.1001-6600.2020082701

广西师范大学学报（自然科学版） ›› 2021, Vol. 39 ›› Issue (04) : 47 -54. DOI: 10.16088/j.issn.1001-6600.2020082701

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

王金艳, 胡春, 高健

作者信息 +

Author information +

文章历史 +

PDF

摘要

知识编译作为人工智能的重要方向,在实时查询和推理中起重要作用。有序二元决策图(ordered binary decision diagram, OBDD)是知识编译领域中一个主要的编译目标语言,已被广泛用于编译诸多实际的可满足性问题(SAT)。近年来,OBDD的构造技术得到了深入研究,其目的是减少目标OBDD的大小并且缩短编译时间。OBDD的构造方式是影响编译效率的重要因素,为了提高编译时间效率,本文提出一种改进的OBDD构造算法,该算法将SAT问题的子句编译成OBDD的表示形式,并将这些OBDD合并成一个整体。不同于传统的合并算法逐一将OBDD合并到目标OBDD中,本文将一些OBDD先进行合并,然后再整合到目标OBDD中。对随机生成的SAT实例和产品配置问题的实验表明,本文提出的OBDD构造算法的性能优于原始算法。