加强约束的布尔可满足硬件求解器

Hardware Boolean satisfiability solver with enhanced constraint

利用现场可编程门阵列固有的并行性和灵活性,提出在硬件可编程平台上基于随机局部搜索算法的布尔可满足性求解器,用于求解大规模的布尔可满足性问题。相对其他求解器,该求解器的预处理技术能极大提高求解效率;其变元加强策略避免了同一变元被反复连续翻转,降低了搜索陷入局部最优的可能。评估结果表明,求解器最多能处理32 000个变元/128 000个子句的实例。相比当前同类型的求解器,其求解效率明显提高。

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.