| 引用本文: | 马柯帆,肖立权,张建民,等.加强约束的布尔可满足硬件求解器.[J].国防科技大学学报,2018,40(6):105-111.[点击复制] |
| MA Kefan,XIAO Liquan,ZHANG Jianmin,et al.Hardware Boolean satisfiability solver with enhanced constraint[J].Journal of National University of Defense Technology,2018,40(6):105-111[点击复制] |
|
| |
|
|
| 本文已被：浏览 7317次 下载 6000次 |
| 加强约束的布尔可满足硬件求解器 |
| 马柯帆, 肖立权, 张建民, 黎铁军, 周善祥 |
|
(国防科技大学 计算机学院， 湖南 长沙 410073)
|
| 摘要: |
| 利用现场可编程门阵列固有的并行性和灵活性，提出在硬件可编程平台上基于随机局部搜索算法的布尔可满足性求解器，用于求解大规模的布尔可满足性问题。相对其他求解器，该求解器的预处理技术能极大提高求解效率；其变元加强策略避免了同一变元被反复连续翻转，降低了搜索陷入局部最优的可能。评估结果表明，求解器最多能处理32 000个变元/128 000个子句的实例。相比当前同类型的求解器，其求解效率明显提高。 |
| 关键词: 现场可编程门阵列 布尔可满足性 加强约束 不完全算法 |
| DOI：10.11887/j.cn.201806014 |
| 投稿日期：2017-09-18 |
| 基金项目:国家自然科学基金资助项目（61103083，61133007，61572509）；国家重点基础研究发展计划资助项目（2016YFB0200203） |
|
| Hardware Boolean satisfiability solver with enhanced constraint |
| MA Kefan, XIAO Liquan, ZHANG Jianmin, LI Tiejun, ZHOU Shanxiang |
|
(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 |
|
|
|
|
|
