张丽¹,王以松^1,2,谢仲涛¹,冯仁艳¹

¹（贵州大学计算机科学与技术学院 贵阳 550025）；²（公共大数据国家重点实验室(贵州大学) 贵阳 550025) (gs.lizhang18@gzu.edu.cn)

出版日期: 2021-11-01


基金资助:国家自然科学基金项目(61976065，U1836205)

Computing Propositional Minimal Models: MiniSAT-Based Approaches

Zhang Li¹, Wang Yisong^1,2, Xie Zhongtao¹, Feng Renyan¹

¹（College of Computer Science and Technology, Guizhou University, Guiyang 550025);²(State Key Laboratory of Public Big Data (Guizhou University), Guiyang 550025)

Online: 2021-11-01


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

摘要/Abstract

摘要： 计算命题公式的极小模型在人工智能推理系统中是一项必不可少的任务.然而，即使是正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则更稳定.

参考文献

相关文章 2

[1]	徐旖旎,欧阳丹彤,刘梦,张立明,张永刚. 结合故障输出结构特征的极小冲突求解算法[J]. 计算机研究与发展, 2018, 55(11): 2386-2394.
[2]	欧阳丹彤,周建华,刘伯文,张立明. 基于模型诊断中结合问题特征的新方法[J]. 计算机研究与发展, 2017, 54(3): 502-513.

PDF全文下载地址:

https://crad.ict.ac.cn/CN/article/downloadArticleFile.do?attachType=PDF&id=4532