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

作者：马柯帆; 肖立权^*; 张建民; 黎铁军; 周善祥

来源：国防科技大学学报, 2018, 40(06): 105-111.

• 现场可编程门阵列
• 布尔可满足性
• 加强约束
• 不完全算法

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

• 单位
  国防科技大学