| 加强约束的布尔可满足硬件求解器 |
| |
| 引用本文： | 马柯帆,肖立权,张建民,黎铁军,周善祥. 加强约束的布尔可满足硬件求解器[J]. 国防科技大学学报, 2018, 40(6): 105-111 |
| |
| 作者姓名： | 马柯帆 肖立权 张建民 黎铁军 周善祥 |
| |
| 作者单位： | 国防科技大学 计算机学院， 湖南 长沙 410073,国防科技大学 计算机学院， 湖南 长沙 410073,国防科技大学 计算机学院， 湖南 长沙 410073,国防科技大学 计算机学院， 湖南 长沙 410073,国防科技大学 计算机学院， 湖南 长沙 410073 |
| |
| 基金项目： | 国家自然科学基金资助项目（61103083，61133007，61572509）；国家重点基础研究发展计划资助项目（2016YFB0200203） |
| |
| 摘 要： | 利用现场可编程门阵列固有的并行性和灵活性,提出在硬件可编程平台上基于随机局部搜索算法的布尔可满足性求解器,用于求解大规模的布尔可满足性问题。相对其他求解器,该求解器的预处理技术能极大提高求解效率;其变元加强策略避免了同一变元被反复连续翻转,降低了搜索陷入局部最优的可能。评估结果表明,求解器最多能处理32 000个变元/128 000个子句的实例。相比当前同类型的求解器,其求解效率明显提高。
|
| 关 键 词： | 现场可编程门阵列；布尔可满足性；加强约束；不完全算法 |
| 收稿时间： | 2017-09-18 |
Hardware Boolean satisfiability solver with enhanced constraint |
| |
| MA Kefan,XIAO Liquan,ZHANG Jianmin,LI Tiejun and ZHOU Shanxiang. Hardware Boolean satisfiability solver with enhanced constraint[J]. Journal of National University of Defense Technology, 2018, 40(6): 105-111 |
| |
| Authors: | MA Kefan XIAO Liquan ZHANG Jianmin LI Tiejun ZHOU Shanxiang |
| |
| Affiliation: | College of Computer, National University of Defense Technology, Changsha 410073, China,College of Computer, National University of Defense Technology, Changsha 410073, China,College of Computer, National University of Defense Technology, Changsha 410073, China,College of Computer, National University of Defense Technology, Changsha 410073, China and College of Computer, National University of Defense Technology, Changsha 410073, China |
| |
| Abstract: | Taking advantage of parallelism and flexibility of field-programmable gate array, a novel Boolean satisfiability solver based on an improved local search algorithm on the reconfigurable hardware platform was proposed to solve large scale Boolean satisfiability problems. In comparison with the past solver, the preprocessing technology can strongly improve the efficiency of solver; the strategy of strengthening the variable selection can avoid the same variable flipped continuously and repeatedly. It can reduce the possibility of search falling into local optimum. The experimental results indicate that the solver can solve problems of up to 32k variables/128k clauses, and has better performance than previous works. |
| |
| Keywords: | field-programmable gate array Boolean satisfiability enhanced constraint incomplete algorithm |
| 本文献已被 CNKI 等数据库收录！ |
| 点击此处可从《国防科技大学学报》浏览原始摘要信息 |
|
点击此处可从《国防科技大学学报》下载免费的PDF全文 |
|
