| 基于MiniSAT的命题极小模型计算方法 |
| |
| 引用本文： | 张丽,王以松,谢仲涛,冯仁艳.基于MiniSAT的命题极小模型计算方法[J].计算机研究与发展,2021,58(11):2515-2523. |
| |
| 作者姓名： | 张丽 王以松 谢仲涛 冯仁艳 |
| |
| 作者单位： | 贵州大学计算机科学与技术学院 贵阳 550025;贵州大学计算机科学与技术学院 贵阳 550025;公共大数据国家重点实验室(贵州大学) 贵阳 550025 |
| |
| 基金项目： | 国家自然科学基金;国家自然科学基金 |
| |
| 摘 要： | 计算命题公式的极小模型在人工智能推理系统中是一项必不可少的任务.然而,即使是正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则更稳定.
|
| 关 键 词： | 极小模型 SAT求解器 CNF公式 极小归约 极小模型分解 |
Computing Propositional Minimal Models:MiniSAT-Based Approaches |
| |
| 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. |
| |
| Authors: | Zhang Li Wang Yisong Xie Zhongtao Feng Renyan |
| |
| Abstract: | |
| |
| Keywords: | |
| 本文献已被 万方数据 等数据库收录！ |
|
