Modern SAT solvers are based on a paradigm named conflict driven clause learning (CDCL), while local search is an important alternative. Although there have been attempts combining these two methods, this work proposes deeper cooperation techniques. 译文：尽管有人尝试将这两种方法结合起来，但这项工作提出了更深层次的合作技术。

First, we relax the CDCL framework by extending promising branches to complete assignments and calling a local search solver to search for a model nearby. 译文：首先，我们通过扩展有希望的分支来完成任务，并调用局部搜索求解器来搜索附近的模型来放松CDCL框架。

More importantly, the local search assignments and the conflict frequency of variables in local search are exploited in the phase selection and branching heuristics of CDCL. 译文：更重要的是，在CDCL的相位选择和分支启发式中，利用了局部搜索分配和局部搜索变量的冲突频率。

We use our techniques to improve three typical CDCL solvers (glucose, MapleLCMDistChronoBT and Kissat). Experiments on benchmarks from the Main tracks of SAT Competitions 2017–2020 and a real world benchmark of spectrum allocation show that the techniques bring significant improvements, particularly on satisfiable instances.译文：这些技术带来了显著的改进，特别是在SAT的实例上。

For example, the integration of our techniques allow the three CDCL solvers to solve 62, 67 and 10 more instances in the benchmark of SAT Competition 2020. A resulting solver won the Main Track SAT category in SAT Competition 2020 and also performs very well on the spectrum allocation benchmark.

As far as we know, this is the first work that meets the standard of the challenge “Demonstrate the successful combination of stochastic search and systematic search techniques, by the creation of a new algorithm that outperforms the best previous examples of both approaches.” [35] on standard application benchmarks.

There have been attempts combining CDCL and local search solvers. However, in previous hybrid solvers, CDCL and local search solvers usually see each other as a black box and the hybrid solver invokes the respective solver according to different situations [3, 5, 19, 24, 30].

译文：有人尝试将CDCL和本地搜索解决方案结合起来。然而，在以往的混合求解器中，CDCL和局部搜索求解器通常将对方视为一个黑盒子，混合求解器根据不同的情况调用各自的求解器[3,5,19,24,30]。

This work is devoted to deeper cooperation of CDCL and local search for SAT, where CDCL is the main solver and local search is used as an aiding tool. 译文：本工作致力于CDCL与SAT的本地搜索的深入合作，其中CDCL是主要的解决方案，本地搜索作为辅助工具。

We propose three ideas to use local search to help CDCL in different ways. 译文：我们提出了三种使用本地搜索以不同方式帮助CDCL的想法。

The first idea is a method for plugging a local search solver into a CDCL solver, while the other two ideas concern with using information produced by the local search solver to enhance CDCL. We summarize the three techniques below.

Explore promising branches by local search (Sect. 3)

The first idea is to a novel method to plug a local search solver into a CDCL solver. We relax the backtrack process by allowing some promising branches to be extended to a complete assignment without backtracking, even if conflicts are met during extending the assignment. Then, a local search solver is called to find a model nearby. If the local search cannot find a model within a given time limit, the CDCL search process continues as normal from the node where the algorithm enters the non-backtracking phase.

Phase selection with local search assignments (Sect. 4)

Phase selection refers to pick a truth value (usually called phase) to assign the branching variable. Most modern CDCL solvers implement a phase selection heuristic named phase saving [34], which keeps the branching phase and uses the saved phase when a variable is picked to branch. Recent progress shows that using some other forms of target phase, e.g., the value under the largest conflict-free assignment in the solver, random value and the opposite of the saved phase, to reset the saved phase periodically could be beneficial [10]. We propose a phase resetting technique, which mainly relies on the assignments produced by the integrated local search solver.

Branching with local search conflict information (Sect. 5)

We use the variables’ conflict frequency, i.e., the frequency appearing in unsatisfied clauses during local search, to enhance the branching heuristic in CDCL. Specifically, such information is used to modify the variables’ activity in VSIDS heuristic and the variables’ learning rate in LRB heuristic.

2.1 Preliminary Definitions and Notations

2.2 CDCL Solvers

2.3 Local Search Solvers

2.4 Experiment Preliminaries