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

• • 上一篇    下一篇

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

王金艳1,2*, 胡春2, 高健3   

  1. 1.广西多源信息挖掘与安全重点实验室(广西师范大学), 广西 桂林 541004;
    2.广西师范大学 计算机科学与工程学院, 广西 桂林 541004;
    3.大连海事大学 信息科学技术学院, 辽宁 大连 116026
  • 收稿日期:2020-08-27 修回日期:2020-11-18 出版日期:2021-07-25 发布日期:2021-07-23
  • 通讯作者: 王金艳(1982—), 女, 广西桂林人, 广西师范大学教授, 博士。E-mail: wangjy612@gxnu.edu.cn
  • 基金资助:
    国家自然科学基金(61763003); 广西多源信息挖掘与安全重点实验室系统性研究课题(19-A-02-01); 广西研究生教育创新计划(XYCSZ2020072); 广西高等学校千名中青年骨干教师培育计划; “八桂学者”工程专项; 广西区域多源信息集成与智能处理协同创新中心项目

An OBDD Construction Method for Knowledge Compilation

WANG Jinyan1,2*, HU Chun2, GAO Jian3   

  1. 1. Guangxi Key Lab of Multisource Information Mining and Security (Guangxi Normal University), Guilin Guangxi 541004, China;
    2. School of Computer Science and Engineering, Guangxi Normal University, Guilin Guangxi 541004, China;
    3. School of Information Science and Technology, Dalian Maritime University, Dalian Liaoning 116026, China
  • Received:2020-08-27 Revised:2020-11-18 Online:2021-07-25 Published:2021-07-23

PDF (PC)

116

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

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

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

Key words: artificial intelligence, knowledge compilation, ordered binary decision diagram, satisfiability problem, off-line preprocessing, on-line reasoning

中图分类号: 

  • TP301
[1]谷文祥, 赵晓威, 殷明浩. 知识编译研究[J]. 计算机科学, 2010, 37(7): 20-26. DOI:10.3969/j.issn.1002-137X.2010.07.005.
[2]CAPELLI F. Knowledge compilation languages as proof systems[C]// Theory and Applications of Satisfiability Testing-SAT 2019: LNCS Volume 11628. Cham, Switzerland: Springer Nature Switzerland AG, 2019: 90-99. DOI:10.1007/978-3-030-24258-9_6.
[3]CAPELLI F. Understanding the complexity of #SAT using knowledge compilation[C]// 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). Piscataway, NJ: IEEE Press, 2017: 1-10. DOI:10.1109/LICS. 2017.8005121.
[4]CADOLI M, DONINI F M, LIBERATORE P, et al. Preprocessing of intractable problems[J]. Information and Computation, 2002, 176(2): 89-120. DOI:10.1006/inco.2001.3043.
[5]ITSYKSON D, KNOP A, ROMASHCHENKO A, et al. On OBDD-based algorithms and proof systems that dynamically change order of variables[J].The Journal of Symbolic Logic, 2020, 85(2): 632-670. DOI:10.1017/jsl.2019.53.
[6]BURY M. Randomized OBDD-based graph algorithms[J]. Theoretical Computer Science, 2018, 751: 24-45. DOI:10.1016/ j.tcs.2016.11.028.
[7]BUSS S, ITSYKSON D, KNOP A, et al. Reordering rule makes OBDD proof systems stronger[C]// 33rd Computational Complexity Conference (CCC 2018). Wadern, Germany: Schloss Dagstuhl-Leibniz Center for Informatics, 2018: 16. DOI:10.4230/LIPIcs.CCC.2018.16.
[8]BOVA S, SLIVOVSKY F. On compiling structured CNFs to OBDDs[J]. Theory of Computing Systems, 2017, 61(2): 637-655. DOI:10.1007/s00224-016-9715-z.
[9]MARQUIS P. Knowledge compilation using theory prime implicates[C]// Proceedings of the Fourteenth International Joint Conference on Artificial Intelligence. San Mateo, CA: Morgan Kaufmann, 1995: 837-843.
[10]JABBOUR S, MA Y, RADDAOUI B, et al. Quantifying conflicts in propositional logic through prime implicates[J]. International Journal of Approximate Reasoning, 2017, 89: 27-40. DOI:10.1016/j.ijar.2016.12.017.
[11]SALHI Y. Approaches for enumerating all the essential prime implicants[C]// Artificial Intelligence: Methodology, Systems, and Applications: LNCS Volume 11089. Cham, Switzerland: Springer Nature Switzerland AG, 2018: 228-239. DOI:10.1007/978-3-319-99344-7_21.
[12]SELMAN B, KAUTZ H A. Knowledge compilation and theory approximation[J]. Journal of the ACM, 1996, 43(2): 193-224. DOI:10.1145/226643.226644.
[13]BOLLIG B, FARENHOLTZ M. On the relation between structured d-DNNFs and SDDs[J]. Theory of Computing Systems, 2021, 65(2): 274-295. DOI:10.1007/s00224-020-10003-y.
[14]LAGNIEZ J, MARQUIS P. An improved decision-DNNF compiler[C]// Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence. San Francisco, CA: International Joint Conferences on Artificial Intelligence, 2017: 667-673. DOI:10.24963/ijcai.2017/93.
[15]BOVA S, CAPELLI F, MENGEL S, et al. On compiling CNFs into structured deterministic DNNFs[C]// Theory and Applications of Satisfiability Testing-SAT 2015: LNCS Volume 9340. Cham, Switzerland: Springer International Publishing AG Switzerland, 2015: 199-214. DOI:10.1007/978-3-319-24318-4_15.
[16]DE UÑA D, GANGE G, SCHACHTE P, et al. Compiling CP subproblems to MDDs and d-DNNFs[J]. Constraints: An International Journal, 2019, 24(1): 56-93. DOI:10.1007/s10601-018-9297-2.
[17]BOVA S. SDDs are exponentially more succinct than OBDDs[C]// Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence. Menlo Park, CA: AAAI Press, 2016: 929-935.
[18]LAI Y, LIU D Y, YIN M H. New canonical representations by Julmenting OBDDs with conjunctive decomposition[J].Journal of Artificial Intelligence Research, 2017, 58: 453-521. DOI:10.1613/jair.5271.
[19]牛当当, 刘磊, 吕帅. EPCCL理论的求交知识编译算法[J]. 软件学报, 2017, 28(8): 2096-2112. DOI:10.13328/j.cnki.jos.005125.
[20]牛当当, 刘磊, 吕帅. EPCCL理论的并行知识编译算法[J]. 电子学报, 2018, 46(3): 537-543. DOI:10.3969/j.issn.0372-2112.2018.03.004.
[21]刘磊, 牛当当, 吕帅. 基于超扩展规则的知识编译方法[J]. 计算机学报, 2016, 39(8): 1681-1696.
[22]刘大有, 赖永, 林海. C2E:一个高性能的EPCCL编译器[J]. 计算机学报, 2013, 36(6): 1254-1260. DOI:10.3724/SP.J.1016.2013.01254.
[23]谷文祥, 王金艳, 殷明浩. 基于MCN和MO启发式策略的扩展规则知识编译方法[J]. 计算机研究与发展, 2011, 48(11): 2064-2073.
[24]BOOTH S, MUISE C, SHAH J. Evaluating the interpretability of the knowledge compilation map: communicating logical statements effectively[C]// Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence. San Francisco:International Joint Conferences on Artificial Intelligence, 2019: 5801-5807. DOI:10.24963/ijcai.2019/804.
[25]SINZ C. Knowledge compilation for product configuration[C]// Proceedings of the ECAI 2002 Workshop on Configuration.Amsterdam: IOS Press, 2002: 23-26.
[26]SUBBARAYAN S. Integrating CSP decomposition techniques and BDDs for compiling configuration problems[C]// Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems: LNCS Volume 3524. Berlin: Springer, 2005: 351-365. DOI:10.1007/11493853_26.
[27]NARODYTSKA N, WALSH T. Constraint and variable ordering heuristics for compiling configuration problems[C]// Proceedings of the 20th International Joint Conference on Artificial Intelligence.San Mateo, CA: Morgan Kaufmann, 2007: 149-154.
[28]GRUMBERG O, LIVNE S, MARKOVITCH S. Learning to order BDD variables in verification[J]. Journal of Artificial Intelligence Research, 2003, 18: 83-116. DOI:10.1613/jair.1096.
[29]RUDELL R. Dynamic variable ordering for ordered binary decision diagrams[C]// Proceedings of 1993 IEEE/ACM International Conference on Computer-Aided Design.Los Alamitos, CA: IEEE Computelr Society Press, 1993: 42-47. DOI:10.1109/ICCAD.1993.580029.
[30]MATTHES B, ZENGLER C, KÜCHLIN W. An improved constraint ordering heuristics for compiling configuration problems[C]// Proceedings of the Workshop on Configuration at ECAI 2012. Amsterdam: IOS Press, 2012: 36-40.
[31]HUANG J B, DARWICHE A. Using DPLL for efficient OBDD construction[C]// Theory and Applications of Satisfiability Testing: LNCS Volume 3542. Berlin: Springer, 2005: 157-172. DOI:10.1007/11527695_13.
[32]BRYANT R E. Graph-based algorithms for Boolean function manipulation[J]. IEEE Transactions on Computers, 1986, C-35(8): 677-691. DOI:10.1109/tc.1986.1676819.
[33]MITCHELL D, SELMAN B, LEVESQUE H. Hard and easy distributions of SAT problems[C]// Proceedings of the 10th National Conference on Artificial Intelligence. Menlo Park, CA: AAAI Press, 1992: 459-465.
[34]PENNOCK D M, STOUT Q F. Exploiting a theory of phase transitions in three-satisfiability problems[C]// Proceedings of the Thirteenth National Conference on Artificial Intelligence. Menlo Park, CA: AAAI Press, 1996: 253-258.
[1] 张仁津, 唐翠芳, 刘彬. 基于人工神经网络游戏程序的研究和设计[J]. 广西师范大学学报（自然科学版）, 2011, 29(2): 119-124.
Viewed
Full text


Abstract

Cited
  Shared   
  Discussed   
[1] 李钰慧, 陈泽柠, 黄中豪, 周岐海. 广西弄岗熊猴的雨季活动时间分配[J]. 广西师范大学学报（自然科学版）, 2018, 36(3): 80 -86 .
[2] 覃盈盈, 漆光超, 梁士楚. 凤眼莲组织浸提液对靖西海菜花种子萌发的影响[J]. 广西师范大学学报（自然科学版）, 2018, 36(3): 87 -92 .
[3] 包金萍, 郑连斌, 宇克莉, 宋雪, 田金源, 董文静. 大凉山彝族成人皮褶厚度特征[J]. 广西师范大学学报（自然科学版）, 2018, 36(3): 107 -112 .
[4] 王梦飞, 黄松. 广西西江经济带的城市旅游经济空间关联研究[J]. 广西师范大学学报（自然科学版）, 2018, 36(3): 144 -150 .
[5] 刘国伦, 宋树祥, 岑明灿, 李桂琴, 谢丽娜. 带宽可调带阻滤波器的设计[J]. 广西师范大学学报（自然科学版）, 2018, 36(3): 1 -8 .
[6] 滕志军, 吕金玲, 郭力文, 许媛媛. 基于改进粒子群算法的无线传感器网络覆盖策略[J]. 广西师范大学学报（自然科学版）, 2018, 36(3): 9 -16 .
[7] 刘铭, 张双全, 何禹德. 基于改进SOM神经网络的异网电信用户细分研究[J]. 广西师范大学学报（自然科学版）, 2018, 36(3): 17 -24 .
[8] 苗新艳, 张龙, 罗颜涛, 潘丽君. 一类交替变化的竞争—合作混杂种群模型研究[J]. 广西师范大学学报（自然科学版）, 2018, 36(3): 25 -31 .
[9] 黄开娇, 肖飞雁. 具有Beddington-DeAngelis型功能性反应的随机捕食—被捕食系统[J]. 广西师范大学学报（自然科学版）, 2018, 36(3): 32 -40 .
[10] 黄荣里, 李长友, 汪敏庆. 一类常微分方程的伯恩斯坦定理Ⅱ[J]. 广西师范大学学报（自然科学版）, 2018, 36(3): 50 -55 .
版权所有 © 广西师范大学学报（自然科学版）编辑部
地址：广西桂林市三里店育才路15号　邮编：541004
电话：0773-5857325　E-mail: gxsdzkb@mailbox.gxnu.edu.cn
本系统由北京玛格泰克科技发展有限公司设计开发