This note introduce a novel method for improving CDCL-based SAT solvers by relaxing backtrack and integrating local search techniques, and we use this method to improve four state of the art CDCL solvers.

译文：本文介绍了一种通过放松回溯和集成局部搜索技术来提高基于CDCL的SAT求解器性能的新方法，并对现有的四种CDCL求解器进行了改进。

主要技术：

1.  relaxing the backtracking 松弛回溯

2.  CCAnr solver——一种随机局部搜索求解器

S. Cai, C. Luo, and K. Su, “CCAnr: A configuration checking based local search solver for non-random satisfiability,” in Proceedings of18th
International Conference on Theory and Applications of Satisfiability Testing, SAT 2015, Austin, TX, USA, September 24-27, 2015, 2015, pp.1–8.

3.  两者结合改进2018年的四个CDCL求解器

1.关于松弛回溯

 （1）基本思想

The idea is to relax the backtrack process,by allowing some promising branches to be extended to
the leaf (corresponding to a complete assignment) without backtracking, even if conflicts are met during extending the assignment.

译文：其思想是放松回溯过程，通过允许一些有前途的分支扩展到叶(对应于一个完整的赋值)而不进行回溯，即使在扩展赋值期间遇到了冲突。

所依据（猜测的）依据是：以这种方式获得的完整的分配结果是高度一致的，有可能与真正所求解的模型之间有较小的距离(只需要少量翻转即可一致)

（2）实施步骤

首先，找到分支扩展；

其次，交给SLS求解器去 find a model nearby。（a local search solver is called to find a model nearby）

如果在规定翻转次数或时间内找不到最终sat模型，就回到CDCl继续正常求解。