| 一种增加了对称破缺的改进子集可满足性算法 |
| |
| 引用本文： | 唐玉兰,张惠国,于宗光.一种增加了对称破缺的改进子集可满足性算法[J].江苏大学学报(自然科学版),2010,31(3). |
| |
| 作者姓名： | 唐玉兰 张惠国 于宗光 |
| |
| 作者单位： | 1. 江南大学,信息工程学院,江苏,无锡,214122
2. 江南大学,信息工程学院,江苏,无锡,214122;中国电子科技集团公司第五十八研究所,江苏,无锡,214035 |
| |
| 基金项目： | 江苏省自然科学基金资助项目(BK2007026);;江苏省“333高层次人才培养工程”专项基金资助项目(2007124) |
| |
| 摘 要： | 为了消除子集可满足性算法在布线过程中带来运行时间增加的负面影响,提出了一种新的布线流程.针对子集可满足性算法在求解同时增加额外的变量和字句,而使得对称数量按指数级增长的问题,选用增加静态对称破缺的方法对合取范式(CNF)进行预处理,侦测并破缺其中的对称,从而达到减少搜索路径的目的.用简化图自同构的方法侦测所有对称,在增加合适的对称破缺判定(SBPs)后,限制搜索在空间的非对称领域进行,从而减少了搜索空间,而不影响CNF公式的可满足性.然后把预处理过的CNF送入布尔可满足性(SAT)解法器进行求解.试验结果表明,这种方法可以显著减少运行时间,加速求解过程.
|
| 关 键 词： | 基准 布尔函数 现场可编程门阵列 布线算法 对称 |
An improved sub-SAT algorithm of adding symmetry-breaking |
| |
| Tang Yulan,Zhang Huiguo,Yu Zongguang.An improved sub-SAT algorithm of adding symmetry-breaking[J].Journal of Jiangsu University:Natural Science Edition,2010,31(3). |
| |
| Authors: | Tang Yulan Zhang Huiguo Yu Zongguang |
| |
| Institution: | 1.School of Information Technology/a>;Jiangnan University/a>;Wuxi/a>;Jiangsu 214122/a>;China/a>;2.China Electronics Technology Group Corporation No.58 Research Institute/a>;Jiangsu 214035/a>;China |
| |
| Abstract: | In order to eliminate the negative effect of increasing running time of sub-SAT algorithm in the routing process,a new routing flow was proposed.Additional variables and clauses were introduced by sub-SAT,and the number of symmetries was made with exponential growth in the solving process.In responseto this problem,static symmetry-breaking was used to carry out pretreatment of conjunctive normalform(CNF),detect and break the symmetries therein.Consequently,the purpose of reducing the search path was achieve... |
| |
| Keywords: | benchmarking boolean functions field programmable gate arrays routing algorithms symmetry |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
|
