| 基于符号模拟和变量划分的SAT算法 |
| |
| 作者姓名： | 闫炜 吴尽昭 高新岩 |
| |
| 作者单位： | 1. 电子科技大学,计算机科学与工程学院,四川,成都610054
2. 电子科技大学,计算机科学与工程学院,四川,成都610054;中国科学院,成都计算机应用研究所,四川,成都610041
3. 中国科学院,成都计算机应用研究所,四川,成都610041 |
| |
| 基金项目： | 国家自然科学基金
,
国家重点基础研究发展计划(973计划) |
| |
| 摘 要： | 针对SAT算法中回溯次数较多的问题,采用基于符号模拟和变量划分的方法来解决其不足.基于符号模拟和变量划分的SAT算法将一个较大的CNF分解为两个子集,每个子集所包含的变量又划分为两个互不相交的子集,仅对那些无法判断的子集,赋以符号值,从而限定了赋予符号值的变量范围,即可减少算法的回溯次数,又能降低内存占用率.理论及实验结果均证明,该算法是合理且有效的.
|
| 关 键 词： | SAT 符号模拟 合取范式 变量划分 |
| 文章编号： | 1009-3087(2008)03-0121-05 |
| 收稿时间： | 2007-01-24 |
| 修稿时间： | 2007-01-24 |
| 本文献已被 维普 万方数据 等数据库收录！ |
| 点击此处可从《四川大学学报(工程科学版)》浏览原始摘要信息 |
|
点击此处可从《四川大学学报(工程科学版)》下载全文 |
|
