• 中国精品科技期刊
  • 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)
    • 相关文章
    • 施引文献(24)

  • 期刊类型引用(12)

    1. 李晓静，杨秀杰. 云计算环境下多模态异构网络数据安全存储方法. 现代电子技术. 2025(06): 63-67 . 百度学术
    2. 李林，左天才，杜泽新，谢志奇. 基于LSM树的在线监测数据安全存储系统设计. 电子设计工程. 2024(07): 63-67 . 百度学术
    3. 闫丽飞，褚宇宁，赵维伟，何壮壮，刘晓强. 大规模非结构化数据资源快速存储方法研究. 集成电路与嵌入式系统. 2024(04): 77-81 . 百度学术
    4. 何博宇，潘洪志. 大数据环境下位置轨迹安全存储系统研究与实现. 电脑知识与技术. 2024(10): 77-80 . 百度学术
    5. 巢成，蒲非凡，许建秋，高云君. 基于空间位置关系的轨迹数据高效降维和查询算法. 计算机研究与发展. 2024(07): 1771-1790 . 本站查看
    6. 王芳，王建民，邵芬红. 多信道无线通信网络动态数据完整性存储仿真. 计算机仿真. 2024(07): 451-455 . 百度学术
    7. 张铠，黄晋，汪希. 基于区块链技术的网络信息安全访问控制方法. 信息技术与信息化. 2024(09): 197-200 . 百度学术
    8. 马明扬，杨洪勇，刘飞. 基于强化学习的双人博弈差分隐私保护研究. 复杂系统与复杂性科学. 2024(04): 107-114 . 百度学术
    9. 李玉光，郗海龙. 物联网异构数据库分层访问算法仿真. 计算机仿真. 2023(03): 490-493+498 . 百度学术
    10. 吕舰. 基于国密算法的网络通信传输数据安全存储方法. 长江信息通信. 2023(04): 171-174 . 百度学术
    11. 王辉，陈宇，申自浩，刘沛骞. 结合对比监督和排序树的轨迹数据差分隐私保护方案. 计算机工程与科学. 2023(10): 1797-1805 . 百度学术
    12. 王爱兵. 基于区块链的社区矫正系统数据分布式安全存储方法. 电脑知识与技术. 2023(28): 63-65 . 百度学术

    其他类型引用(12)

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

目录

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

    /

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

    微信订阅号
    （实时资讯）

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

    微信服务号
    （同步网站）

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

    微信视频号
    （视频分享）

    CCF<br/>（扫码入会）

    CCF
    （扫码入会）

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

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