基于子句的动态检查强制文字的SAT求解器

检查强制文字是一种重要的预处理方法。结合学习子句,提出一种在求解过程中使用的策略—基于子句的动态检查强制文字(CNL),并且设计了一种易实现低成本的数据结构。分别实现了两个不同版本的求解器:Glucose_PRE和Glucose_CNL,前者在求解初始时将检查强制文字作为预处理,后者实现了基于子句的动态检查强制文字策略。实验测试结果表明,与Glucose_PRE和Glucose3.0求解器相比,求解器Glucose_CNL在求解2015年和2016年SAT竞赛的应用类型的实例时,求解实例个数更多,耗时更少,说明所提策略和所设计的数据结构均可提高求解器的求解性能。

A clause-based dynamical necessaryliteral checking SAT solver

Necessary literal checking is an important preprocessing technique. by learning clauses, this paper proposes a clause based dynamical necessary literal checking strategy (CNL) used in the solving process, and designs a low cost data structure. We implement two solvers, Glucose_PRE and Glucose_CNL. The former adopts the necessary literal checking as the preprocessing technique at the beginning of the solving process, and the latter implements the proposed clause based dynamical necessary literal checking strategy. Experimental results show that the Glucose_CNL solves more instances with less time than the Glucose_PRE and Glucose 3.0 when solving the application type instances in 2015 and 2016 SAT competitions, demonstrating the significance of the proposed strategy and data structure.