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

摘要

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