微信服务号

微信订阅号

2025-4-24- 19
Home > Archive>Volume 28, Issue 8, 2017 >2096-2112. DOI:10.13328/j.cnki.jos.005125
PDF HTML XML Export Cite reminder
Knowledge Compilation Algorithm Based on Computing the Intersection for EPCCL Theories
Author:
Affiliation:

Fund Project:

National Natural Science Foundation of China (61300049, 61502197, 61503044); Specialized Research Fund for the Doctoral Program of Higher Education of China (20120061120059); Key Program for Science and Technology Development of Jilin Province of China (20130206052GX); Natural Science Research Foundation of Jilin Province of China (20140520069JH, 20150101054 JC, 20150520058JH)

  • Article
    • | |
  • Metrics
    • |
  • Reference [45]
    • |
  • Related
    • | | |
  • Comments
    Abstract:

    HER (hyper extension rule) is an expansion of ER (extension rule). The results of computing the union and difference set of two sets of maximum terms which are extended by two clauses respectively based on the hyper extension rule can be saved as EPCCL (each pair of clauses contains complementary literals) theories. In this paper, a parallelizable knowledge compilation algorithm for EPCCL theories, IKCHER, is proposed based on computing the intersection of maximum terms sets. The focus is placed on the research of parallel computing the intersection sets of multiple EPCCL theories based on HER, resulting in the design of the corresponding algorithm, PIAE (parallel intersection of any number of EPCCL). Through using the origin CNF formulae of EPCCL theories, another efficient merging algorithm imp-PIAE is proposed. Based on above methods two parallel knowledge compilation algorithms P-IKCHER and impP-IKCHER are constructed for EPCCL theories, utilizing the PIAE algorithm and imp-PIAE algorithm to merge multiple EPCCL theories respectively. Experimental results show that IKCHER algorithm has the best compilation quality of all EPCCL compilation algorithms. P-IKCHER algorithm does not improve the compilation quality and compilation efficiency of IKCHER while impP-IKCHER algorithms can maintain the compilation quality of IKCHER, and improve the compilation efficiency of IKCHER. When the number of CPU cores is 4, the compilation efficiency of IKCHER can be improved twice as much in the best cases.

    Reference
    [1] Cook SA. The complexity of theorem-proving procedures. In:Harrison MA, Banerji RB, Ullman JD, eds. Proc. of the 3rd Annual ACM Symp. on the Theory of Computing (STOC'71). Shaker Heights:ACM Press, 1971. 151-158.[doi:10.1145/800157.805047]
    [2] Mitchell DG, Selman B, Levesque HJ. Hard and easy distributions of SAT problems. In:Swartout WR, ed. Proc. of the 10th National Conf. on Artificial Intelligence (AAAI'92). San Jose:AAAI Press, The MIT Press, 1992. 459-465.
    [3] Bai S, Bu DB. Analysis for phase transition of the 2-3-SAT problem. Ruan Jian Xue Bao/Journal of Software, 1998,9(11):828-832(in Chinese with English abstract). http://www.jos.org.cn/1000-9825/9/828.htm[doi:10.13328/j.cnki.jos.1998.11.006]
    [4] Cai SW, Su KL. Local search for Boolean satisfiability with configuration checking and subscore. Artificial Intelligence, 2013,204:75-98.[doi:10.1016/j.artint.2013.09.001]
    [5] Luo C, Su KL, Cai SW. More efficient two-mode stochastic local search for random 3-satisfiability. Applied Intelligence, 2014, 41(3):665-680.[doi:10.1007/s10489-014-0556-7]
    [6] Luo C, Cai SW, Wu W, Su KL. Double configuration checking in stochastic local search for satisfiability. In:Brodley CE, Stone P, eds. Proc. of the 28th AAAI Conf. on Artificial Intelligence (AAAI 2014). Québec:AAAI Press, 2014. 2703-2709.
    [7] Cai SW, Su KL. Comprehensive score:Towards efficient local search for SAT with long clauses. In:Rossi F, ed. Proc. of the 23rd Int'l Joint Conf. on Artificial Intelligence (IJCAI 2013). IJCAI/AAAI Press, 2013. 489-495.
    [8] Jeavons P, Petke J. Local consistency and SAT-solvers. Journal of Artificial Intelligence Research, 2012,43:329-351.[doi:10.1613/jair.3531]
    [9] Katsirelos G, Sabharwal A, Samulowitz H, Simon L. Resolution and parallelizability:Barriers to the efficient parallelization of SAT solvers. In:desJardins M, Littman ML, eds. Proc. of the 27th AAAI Conf. on Artificial Intelligence (AAAI 2013). Washington:AAAI Press, 2013.
    [10] Audemard G, Simon L. Lazy clause exchange policy for parallel SAT solvers. In Sinz C, Egly U, eds. Proc. of the 17th Int'l Conf. on Theory and Applications of Satisfiability Testing (SAT 2014). LNCS 8561, Vienna:Springer-Verlag, 2014. 197-205.[doi:10. 1007/978-3-319-09284-3_15]
    [11] Sonobe T, Kondoh S, Inaba M. Community branching for parallel portfolio SAT solvers. In Sinz C, Egly U, eds. Proc. of the 17th Int'l Conf. on Theory and Applications of Satisfiability Testing (SAT 2014). LNCS 8561, Vienna:Springer-Verlag, 2014. 188-196.[doi:10.1007/978-3-319-09284-3_14]
    [12] Val DA. On some tractable classes in deduction and abduction. Artificial Intelligence, 2000,116(1-2):297-313.[doi:10.1016/S0004-3702(99)00088-0]
    [13] Broeck GV, Darwiche A. On the role of canonicity in knowledge compilation. In:Bonet B, Koenig S, eds. Proc. of the 29th AAAI Conf. on Artificial Intelligence (AAAI 2015). Austin:AAAI Press, 2015. 1641-1648.
    [14] Marquis P. Existential closures for knowledge compilation. In:Walsh T, ed. Proc. of the 22nd Int'l Joint Conf. on Artificial Intelligence (IJCAI 2011). Barcelona:IJCAI/AAAI Press, 2011. 996-1001.[doi:10.5591/978-1-57735-516-8/IJCAI11-171]
    [15] Fargier H, Marquis P. Disjunctive closures for knowledge compilation. Artificial Intelligence, 2014,216:129-162.[doi:10.1016/j.artint.2014.07.004]
    [16] Darwiche A. Compiling knowledge into decomposable negation normal form. In:Dean T, ed. Proc. of the 16th Int'l Joint Conf. on Artificial Intelligence (IJCAI'99). Stockholm:Morgan Kaufmann Publishers, 1999. 284-289.
    [17] Darwiche A. Decomposable negation normal form. Journal of the ACM, 2001,48(4):608-647.[doi:10.1145/502090.502091]
    [18] Darwiche A, Marquis P. A knowledge compilation map. Journal of Artificial Intelligence Research, 2002,17:229-264.[doi:10.1613/jair.989]
    [19] Fargier H, Marquis P. Extending the knowledge compilation map:Krom, Horn, Affine and beyond. In:Fox D, Gomes CP, eds. Proc. of the 23rd AAAI Conf. on Artificial Intelligence (AAAI 2008). Chicago:AAAI Press, 2008. 442-447.
    [20] Fargier H, Marquis P, Niveau A. Towards a knowledge compilation map for heterogeneous representation languages. In:Rossi F, ed. Proc. of the 23rd Int'l Joint Conf. on Artificial Intelligence (IJCAI 2013). IJCAI/AAAI Press, 2013. 877-883.
    [21] Fargier H, Marquis P, Niveau A, Schmidt N. A knowledge compilation map for ordered real-valued decision diagrams. In:Brodley CE, Stone P, eds. Proc. of the 28th AAAI Conf. on Artificial Intelligence (AAAI 2014). Québec:AAAI Press, 2014. 1049-1055.
    [22] Koriche F, Lagniez JM, Marquis P, Thomas S. Knowledge compilation for model counting:Affine decision trees. In:Rossi F, ed. Proc. of the 23rd Int'l Joint Conf. on Artificial Intelligence (IJCAI 2013). IJCAI/AAAI Press, 2013. 947-953.
    [23] Lai Y, Liu DY, Wang SS. Reduced ordered binary decision diagram with implied literals:A new knowledge compilation approach. Knowledge and Information Systems, 2013,35(3):665-712.[doi:10.1007/s10115-012-0525-6]
    [24] Huang JB, Darwiche A. The language of search. Journal of Artificial Intelligence Research, 2007,29:191-219.[doi:10.1613/jair. 2097]
    [25] Lin H, Sun JG, Zhang YM. Theorem proving based on the extension rule. Journal of Automated Reasoning, 2003,31(1):11-21.[doi:10.1023/A:1027339205632]
    [26] Yin MH, Lin H, Sun JG. Solving #SAT using extension rules. Ruan Jian Xue Bao/Journal of Software, 2009,20(7):1714-1725(in Chinese with English abstract). http://www.jos.org.cn/1000-9825/3320.htm[doi:10.3724/SP.J.1001.2009.03320]
    [27] Lai Y, Ouyang DT, Cai DB, Lü S. Model counting and planning using extension rule. Journal of Computer Research and Development, 2009,46(3):459-469(in Chinese with English abstract).
    [28] Li Y, Sun JG, Wu X, Zhu XJ. Extension rule algorithms based on IMOM and IBOHM heuristics strategies. Ruan Jian Xue Bao/Journal of Software, 2009,20(6):1521-1527(in Chinese with English abstract). http://www.jos.org.cn/1000-9825/3420.htm[doi:10.3724/SP.J.1001.2009.03420]
    [29] Sun JG, Li Y, Zhu XJ, Lü S. A novel theorem proving algorithm based on extension rule. Journal of Computer Research and Development, 2009,46(1):9-14(in Chinese with English abstract).
    [30] Lin H, Sun JG. Knowledge compilation using the extension rule. Journal of Automated Reasoning, 2004,32(2):93-102.[doi:10.1023/B:JARS.0000029959.45572.44]
    [31] Yin MH, Lin H, Sun JG. Counting models using extension rules. In:Proc. of the 22nd AAAI Conf. on Artificial Intelligence (AAAI 2007). Vancouver:AAAI Press, 2007. 1916-1917.
    [32] Gu WX, Wang JY, Yin MH. Knowledge compilation using extension rule based on MCN and MO heuristic strategies. Journal of Computer Research and Development, 2011,48(11):2064-2073(in Chinese with English abstract).
    [33] Liu DY, Lai Y, Lin H. C2E:An EPCCL compiler with good performance. Chinese Journal of Computers, 2013,36(6):1254-1260(in Chinese with English abstract).[doi:10.3724/SP.J.1016.2013.01254]
    [34] Liu L, Niu DD, Li Z, Lü S. Dynamic online reasoning algorithm based on the hyper extension rule. Journal of Harbin Engineering University, 2015,36(12):1614-1619(in Chinese with English abstract).[doi:10.11990/jheu.201404055]
    [35] Liu L, Niu DD, Lü S. Knowledge compilation methods based on the hyper extension rule. Chinese Journal of Computers, 2016, 39(8):1681-1696(in Chinese with English abstract).[doi:10.11897/SP.J.1016.2016.01681]
    附中文参考文献:
    [3] 白硕,卜东波.2-3-SAT问题相变现象剖析及其应用.软件学报,1998,9(11):828-832. http://www.jos.org.cn/1000-9825/9/828.htm[doi:10.13328/j.cnki.jos.1998.11.006]
    [26] 殷明浩,林海,孙吉贵.一种基于扩展规则的#SAT求解系统.软件学报,2009,20(7):1714-1725. http://www.jos.org.cn/1000-9825/3320.htm[doi:10.3724/SP.J.1001.2009.03320]
    [27] 赖永,欧阳丹彤,蔡敦波,吕帅.基于扩展规则的模型计数与智能规划方法.计算机研究与发展,2009,46(3):459-469.
    [28] 李莹,孙吉贵,吴瑕,朱兴军.基于IMOM和IBOHM启发式策略的扩展规则算法.软件学报,2009,20(6):1521-1527. http://www.jos.org.cn/1000-9825/3420.htm[doi:10.3724/SP.J.1001.2009.03420]
    [29] 孙吉贵,李莹,朱兴军,吕帅.一种新的基于扩展规则的定理证明方法.计算机研究与发展,2009,46(1):9-14.
    [32] 谷文祥,王金艳,殷明浩.基于MCN和MO启发式策略的扩展规则知识编译方法.计算机研究与发展,2011,48(11):2064-2073.
    [33] 刘大有,赖永,林海.C2E:一个高性能的EPCCL理论编译器.计算机学报,2013,36(6):1254-1260.[doi:10.3724/SP.J.1016.2013. 01254]
    [34] 刘磊,牛当当,李壮,吕帅.基于超扩展规则的动态在线推理算法.哈尔滨工程大学学报,2015,36(12):1614-1619.[doi:10.11990/jheu.201404055]
    [35] 刘磊,牛当当,吕帅.基于超扩展规则的知识编译方法.计算机学报,2016,39(8):1681-1696.[doi:10.11897/SP.J.1016.2016.01681]
    Related
    Cited by
    Comments
    Comments
    分享到微博
    Submit
Get Citation

牛当当,刘磊,吕帅. EPCCL理论的求交知识编译算法.软件学报,2017,28(8):2096-2112

Copy
Share
Article Metrics
  • Abstract:
  • PDF:
  • HTML:
  • Cited by:
History
  • Received:November 24,2015
  • Revised:April 04,2016
  • Online: August 15,2017
Links:Institute of Software, CASChina Computer FederationCASNSFC
You are the first2038253Visitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address：4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code：100190
Phone：010-62562563 Fax：010-62562533 Email：jos@iscas.ac.cn
Technical Support：Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063