| 基于格局检测的并行模型计数方法 |
| |
| 引用本文： | 李壮,刘磊,张桐搏,吕帅.基于格局检测的并行模型计数方法[J].吉林大学学报(工学版),2020,50(4):1443-1448. |
| |
| 作者姓名： | 李壮 刘磊 张桐搏 吕帅 |
| |
| 作者单位： | 吉林大学计算机科学与技术学院,长春130012;吉林大学计算机科学与技术学院,长春130012;吉林大学计算机科学与技术学院,长春130012;吉林大学计算机科学与技术学院,长春130012 |
| |
| 基金项目： | 吉林大学研究生创新项目;吉林省自然科学基金;国家重点研发计划;国家自然科学基金 |
| |
| 摘 要： | 在经典的可满足性问题求解中,针对处理模型数较少的实例,SWcc迭代法和SWcc优化增量法与完备的模型计数方法相比,求解适用性更高,但SWcc迭代法和SWcc优化增量法均为串行求解方法,没有对解空间进行剪枝、化简等处理。本文基于此设计了基于格局检测的并行模型计数算法。该算法以化简解空间和启发式为核心,将原解空间分解成为若干子空间并对原子句集进行化简后,并行处理各个子空间。实验结果表明:对于模型个数较少、公式规模较大的问题,该算法比原算法更具有适用性。
|
| 关 键 词： | 自动推理 局部搜索 模型计数 格局检测 并行框架 |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
|
