###
DOI:
工程科学与技术:2008,40(3):121-125
本文二维码信息
码上扫一扫!
基于符号模拟和变量划分的SAT算法
(1.电子科技大学 计算机科学与工程学院,四川 成都610054;2.中国科学院 成都计算机应用研究所,四川 成都610041)
SAT Algorithm Based on Symbolic Simulation and Variable Partitions
摘要
图/表
参考文献
相似文献
本文已被:浏览 2477次   下载 222
投稿时间:2007-01-24    
中文摘要: 针对SAT算法中回溯次数较多的问题,采用基于符号模拟和变量划分的方法来解决其不足。基于符号模拟和变量划分的SAT算法将一个较大的CNF分解为两个子集,每个子集所包含的变量又划分为两个互不相交的子集,仅对那些无法判断的子集,赋以符号值,从而限定了赋予符号值的变量范围,即可减少算法的回溯次数,又能降低内存占用率。理论及实验结果均证明,该算法是合理且有效的。
中文关键词: SAT  符号模拟  合取范式  变量划分
Abstract:To solve the problem that SAT solvers usually has excessive backtraces during assigning binary values to an unassigned variables, a new SAT solver based on symbolic simulation and variable partition, which lower not only the number of backtrack but the memory blow-up, was presented. The SAT solver partitions a big CNF into two smaller subset A and B, then divides the set of variables into three disjoint set. Through the constraint that the symbolic values are only assigned to the variable in the set which occur in both A and B, the symbolic simulation based SAT solver get both the low backtrack number and memory occupation. Experimental result showed the SAT solver is sound and efficient.
文章编号:20080323     中图分类号:    文献标志码:
基金项目:国家自然科学基金资助项目(60373113);国家973计划资助项目(2004CB318000)
作者简介:
引用文本:
闫炜,吴尽昭,高新岩.基于符号模拟和变量划分的SAT算法[J].工程科学与技术,2008,40(3):121-125.
.SAT Algorithm Based on Symbolic Simulation and Variable Partitions[J].Advanced Engineering Sciences,2008,40(3):121-125.