• 中国精品科技期刊
  • CCF推荐A类中文期刊
  • 计算领域高质量科技期刊T1类
高级检索

基于MiniSAT的命题极小模型计算方法

张丽, 王以松, 谢仲涛, 冯仁艳

张丽, 王以松, 谢仲涛, 冯仁艳. 基于MiniSAT的命题极小模型计算方法[J]. 计算机研究与发展, 2021, 58(11): 2515-2523. DOI: 10.7544/issn1000-1239.2021.20200370
引用本文: 张丽, 王以松, 谢仲涛, 冯仁艳. 基于MiniSAT的命题极小模型计算方法[J]. 计算机研究与发展, 2021, 58(11): 2515-2523. DOI: 10.7544/issn1000-1239.2021.20200370
shu
Zhang Li, Wang Yisong, Xie Zhongtao, Feng Renyan. Computing Propositional Minimal Models: MiniSAT-Based Approaches[J]. Journal of Computer Research and Development, 2021, 58(11): 2515-2523. DOI: 10.7544/issn1000-1239.2021.20200370
Citation: Zhang Li, Wang Yisong, Xie Zhongtao, Feng Renyan. Computing Propositional Minimal Models: MiniSAT-Based Approaches[J]. Journal of Computer Research and Development, 2021, 58(11): 2515-2523. DOI: 10.7544/issn1000-1239.2021.20200370
shu
张丽, 王以松, 谢仲涛, 冯仁艳. 基于MiniSAT的命题极小模型计算方法[J]. 计算机研究与发展, 2021, 58(11): 2515-2523. CSTR: 32373.14.issn1000-1239.2021.20200370
引用本文: 张丽, 王以松, 谢仲涛, 冯仁艳. 基于MiniSAT的命题极小模型计算方法[J]. 计算机研究与发展, 2021, 58(11): 2515-2523. CSTR: 32373.14.issn1000-1239.2021.20200370
shu
Zhang Li, Wang Yisong, Xie Zhongtao, Feng Renyan. Computing Propositional Minimal Models: MiniSAT-Based Approaches[J]. Journal of Computer Research and Development, 2021, 58(11): 2515-2523. CSTR: 32373.14.issn1000-1239.2021.20200370
Citation: Zhang Li, Wang Yisong, Xie Zhongtao, Feng Renyan. Computing Propositional Minimal Models: MiniSAT-Based Approaches[J]. Journal of Computer Research and Development, 2021, 58(11): 2515-2523. CSTR: 32373.14.issn1000-1239.2021.20200370
shu

基于MiniSAT的命题极小模型计算方法

  • 1(贵州大学计算机科学与技术学院 贵阳 550025)

  • 2(公共大数据国家重点实验室(贵州大学) 贵阳 550025) (gs.lizhang18@gzu.edu.cn)

基金项目: 国家自然科学基金项目(61976065，U1836205)
详细信息

  • 中图分类号: TP3-05; TP301.6

Computing Propositional Minimal Models: MiniSAT-Based Approaches

  • 1(College of Computer Science and Technology, Guizhou University, Guiyang 550025)

  • 2(State Key Laboratory of Public Big Data (Guizhou University), Guiyang 550025)

Funds: This work was supported by the National Natural Science Foundation of China (61976065, U1836205).

摘要

    摘要
  • 摘要: 计算命题公式的极小模型在人工智能推理系统中是一项必不可少的任务.然而，即使是正CNF(conjunctive normal form)公式，其极小模型的计算和验证都不是易处理的.当前，计算CNF公式极小模型的主要方法之一是将其转换为析取逻辑程序后用回答集程序(answer set programming, ASP)求解器计算其稳定模型/回答集.针对计算CNF公式的极小模型的问题，提出一种基于可满足性问题(satisfiability problem, SAT)求解器的计算极小模型的方法MMSAT；然后结合最近基于极小归约的极小模型验证算法CheckMinMR，提出了基于极小模型分解的计算极小模型方法MRSAT；最后对随机生成的大量的3CNF公式和SAT国际竞赛上的部分工业基准测试用例进行测试.实验结果表明：MMSAT和MRSAT对随机3CNF公式和SAT工业测试用例都是有效的，且计算极小模型的速度都明显快于最新版的clingo，并且在SAT工业实例上发现了clingo有计算出错的情况，而MMSAT和MRSAT则更稳定.
    Abstract: Computing minimal models is an essential task in many reasoning systems in artificial intelligence. However, even for a positive conjunctive normal form (CNF) formula, the tasks of computing and checking its minimal model are not tractable. To compute a minimal model of a clause theory, one of the current main methods is to convert the clause theory into a disjunction logic program and use an answer set programming (ASP) solver to compute its stable model. This paper proposes a method MMSAT for computing minimal models based on SAT(satisfiability problem) solvers. In terms of the recently proposed minimal reduct based minimal checking algorithm CheckMinMR, a minimal model decomposing based minimal model computing algorithm MRSAT is proposed. Finally, the two algorithms are evaluated by a large number of randomly generated 3CNF formulas and industrial benchmarks from the SAT international competition. Experimental results show that the two methods proposed in this paper compute minimal models at about three times faster than clingo for random 3CNF formulas and slightly faster than clingo for industrial SAT benchmarks. Thus, they are effective. In addition, it also reveals that clingo sometimes incorrectly computes a minimal model. Thus, the two proposed methods in this paper are more stable than clingo.
    • HTML全文
    • 参考文献(0)
    • 相关文章
    • 施引文献(14)

  • 期刊类型引用(10)

    1. 崔玉礼，黄丽君. 基于图卷积神经网络的WSN零动态攻击检测方法. 太原学院学报(自然科学版). 2025(01): 78-84 . 百度学术
    2. 何戡，陈金喆，宗学军，齐济，孙永超. 基于油气集输半实物仿真平台的工控网络安全测试研究. 化工自动化及仪表. 2024(02): 274-283 . 百度学术
    3. 李卫峰，冯光辉. 基于动态特征选择的恶意网络行为检测仿真. 计算机仿真. 2024(02): 410-414 . 百度学术
    4. 马佳利，郭渊博，方晨，陈庆礼，张琦. 基于数字孪生的工业互联网安全检测与响应研究. 通信学报. 2024(06): 87-100 . 百度学术
    5. 李一鑫. 面向工业网络场景的基于1DLA-CNN和DCNN-IDS算法的网络安全检测模型研究. 自动化与仪器仪表. 2024(07): 138-142 . 百度学术
    6. 过珺. 基于优先级诊断树的工控网络入侵数据关联挖掘方法. 齐齐哈尔大学学报(自然科学版). 2024(04): 11-16 . 百度学术
    7. 王泽鹏 ，马超 ，张壮壮 ，吴黎兵 ，石小川 . 动态决策驱动的工控网络数据要素威胁检测方法. 计算机研究与发展. 2024(10): 2404-2416 . 本站查看
    8. 刘奇旭，陈艳辉，尼杰硕，罗成，柳彩云，曹雅琴，谭儒，冯云，张越. 基于机器学习的工业互联网入侵检测综述. 计算机研究与发展. 2022(05): 994-1014 . 本站查看
    9. 赵明明，司红星，刘潮. 基于数据挖掘与关联分析的工控设备异常运行状态自动化检测方法分析. 信息安全与通信保密. 2022(04): 2-10 . 百度学术
    10. 刘广睿，张伟哲，李欣洁. 基于边缘样本的智能网络入侵检测系统数据污染防御方法. 计算机研究与发展. 2022(10): 2348-2361 . 本站查看

    其他类型引用(4)

    • 资源附件(0)
计量
  • 文章访问数:  350
  • HTML全文浏览量:  6
  • PDF下载量:  182
  • 被引次数: 14
出版历程
  • 发布日期:  2021-10-31

目录

摘要
HTML全文
    参考文献(0)
    相关文章
    施引文献(14)
    资源附件(0)

    /

    返回文章
    返回
    邮件订阅 RSS
    微信订阅号<br/>（实时资讯）

    微信订阅号
    （实时资讯）

    微信服务号<br/>（同步网站）

    微信服务号
    （同步网站）

    微信视频号<br/>（视频分享）

    微信视频号
    （视频分享）

    CCF<br/>（扫码入会）

    CCF
    （扫码入会）

    版权所有 © 《计算机研究与发展》编辑部

    本系统由北京仁和汇智信息技术有限公司开发  百度统计