Journal of Guangxi Normal University(Natural Science Edition) ›› 2021, Vol. 39 ›› Issue (4): 47-54.doi: 10.16088/j.issn.1001-6600.2020082701

Previous Articles     Next Articles

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)

172

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

CLC Number: 

  • 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] LU Miao, HE Dengxu, QU Liangdong. Grey Wolf Optimization Algorithm Based on Elite Learning for Nonlinear Parameters [J]. Journal of Guangxi Normal University(Natural Science Edition), 2021, 39(4): 55-67.
[2] XU Lunhui,HUANG Baoshan,ZHONG Haixing. Time Window Model and Algorithm with AGV System Path Planning [J]. Journal of Guangxi Normal University(Natural Science Edition), 2019, 37(3): 1-8.
[3] SHI Ya-bing, HUANG Yu, QIN Xiao, YUAN Chang-an. K-Means Clustering Algorithm Based on a Novel Approach for Improved Initial Seeds [J]. Journal of Guangxi Normal University(Natural Science Edition), 2013, 31(4): 33-40.
[4] WENG Shi-zhou, LÜ Yue-jin, MO Jing-lan. Ranking Model and Its Order-preserving Reduction Theory Based on Dominance Relations [J]. Journal of Guangxi Normal University(Natural Science Edition), 2013, 31(3): 37-44.
[5] CAO Yong-chun, SHAO Ya-bin, TIAN Shuang-liang, CAI Zheng-qi. A Clustering Method Based on Immune Genetic Algorithm [J]. Journal of Guangxi Normal University(Natural Science Edition), 2013, 31(3): 59-64.
[6] ZHANG Chao-qun, ZHENG Jian-guo, LI Tao-shen. Effect of Scout Bees on the Performance of Artificial Bee Colony Algorithm [J]. Journal of Guangxi Normal University(Natural Science Edition), 2013, 31(3): 72-80.
[7] ZHOU Yan-cong, GU Jun-hua, DONG Yong-feng. Converse Binary Anti-collision Algorithm and Hardware Implementation Based on FPGA [J]. Journal of Guangxi Normal University(Natural Science Edition), 2013, 31(3): 94-99.
[8] XIE Guang-qiang, ZHANG Yun, LI Yang, ZENG Qi-jie. Research of Krause's Multi-Agent Consensus Model [J]. Journal of Guangxi Normal University(Natural Science Edition), 2013, 31(3): 106-113.
[9] HUANG Min, JIN Ting, ZHONG Sheng, MA Yu-chun. Ant Colony Algorithm for Solving Continuous Function Optimization Problem Based on Pheromone Distributive Function [J]. Journal of Guangxi Normal University(Natural Science Edition), 2013, 31(2): 34-38.
[10] ZHAI Ying, YI Zhong, XIE Zheng-wei, DENG Pei-min, LI Yue. Garden of Eden Configurations of a Particular Hybrid Transformation of Two-dimensional Cellular Automata [J]. Journal of Guangxi Normal University(Natural Science Edition), 2013, 31(1): 37-43.
[11] CUI Yao-dong, ZHOU Mi, YANG Liu. Strategies for Solving the 1D Cutting Stock Problem of Multiple Stock Lengths [J]. Journal of Guangxi Normal University(Natural Science Edition), 2012, 30(3): 149-153.
[12] MA Ning, YU Hong-zhi. Image Watermarking Algorithm Based on DCT Transform and ArnoldTransform [J]. Journal of Guangxi Normal University(Natural Science Edition), 2011, 29(3): 163-167.
[13] YE Qing, HUANG Qiang, NIE Bin, LI Huan. An Adaptive High-Dimensional Outlier Recognition Method [J]. Journal of Guangxi Normal University(Natural Science Edition), 2020, 38(2): 107-114.
[14] WANG Junjie, WEN Xueyan, XU Kesheng, YU Ming. An Improved Stack Algorithm Based on Local Sensitive Hash [J]. Journal of Guangxi Normal University(Natural Science Edition), 2020, 38(4): 21-31.
[15] HU Juntao, SHI Xiaohu, MA Deyin. Nursing Workers Scheduling Based on Mean Shift and Genetic Algorithm [J]. Journal of Guangxi Normal University(Natural Science Edition), 2021, 39(3): 27-39.
Viewed
Full text


Abstract

Cited
  Shared   
  Discussed   
[1] LI Yuhui, CHEN Zening, HUANG Zhonghao, ZHOU Qihai. Activity Time Budget of Assamese macaque (Macaca assamensis) during Rainy Season in Nonggang Nature Reserve, Guangxi, China[J]. Journal of Guangxi Normal University(Natural Science Edition), 2018, 36(3): 80 -86 .
[2] QIN Yingying, QI Guangchao, LIANG Shichu. Effects of Eichhornia crassipes Aqueous Extracts on Seed Germination of Ottelia acuminata var. jingxiensis[J]. Journal of Guangxi Normal University(Natural Science Edition), 2018, 36(3): 87 -92 .
[3] BAO Jinping, ZHENG Lianbin, YU Keli, SONG Xue, TIAN Jinyuan, DONG Wenjing. Skinfold Thickness Characteristics of Yi Adults in Daliangshan,China[J]. Journal of Guangxi Normal University(Natural Science Edition), 2018, 36(3): 107 -112 .
[4] WANG Mengfei, HUANG Song. Spatial Linkage of Tourism Economy of Cities in West River Economic Belt in Guangxi, China[J]. Journal of Guangxi Normal University(Natural Science Edition), 2018, 36(3): 144 -150 .
[5] LIU Guolun, SONG Shuxiang, CEN Mingcan, LI Guiqin, XIE Lina. Design of Bandwidth Tunable Band-Stop Filter[J]. Journal of Guangxi Normal University(Natural Science Edition), 2018, 36(3): 1 -8 .
[6] TENG Zhijun, LÜ Jinling, GUO Liwen, XU Yuanyuan. Coverage Strategy of Wireless Sensor Network Based on Improved Particle Swarm Optimization Algorithm[J]. Journal of Guangxi Normal University(Natural Science Edition), 2018, 36(3): 9 -16 .
[7] LIU Ming, ZHANG Shuangquan, HE Yude. Classification Study of Differential Telecom Users Based on SOM Neural Network[J]. Journal of Guangxi Normal University(Natural Science Edition), 2018, 36(3): 17 -24 .
[8] MIAO Xinyan, ZHANG Long, LUO Yantao, PAN Lijun. Study on a Class of Alternative Competition-Cooperation Hybrid Population Model[J]. Journal of Guangxi Normal University(Natural Science Edition), 2018, 36(3): 25 -31 .
[9] HUANG Kaijiao, XIAO Feiyan. A Stochastic Predator-prey System with Beddington-DeAngelis Functional Response[J]. Journal of Guangxi Normal University(Natural Science Edition), 2018, 36(3): 32 -40 .
[10] HUANG Rongli, LI Changyou, WANG Minqing. Bernstein's Theorem for a Class of Ordinary Differential Equations Ⅱ[J]. Journal of Guangxi Normal University(Natural Science Edition), 2018, 36(3): 50 -55 .
Copyright © Journal of Guangxi Normal University(Natural Science Edition), All Rights Reserved.
Tel: 0773-5857325　E-mail: gxsdzkb@mailbox.gxnu.edu.cn
Powered by Beijing Magtech Co. Ltd