文献学习--Deep Cooperation of CDCL and Local Search for SAT
作者：互联网
Deep Cooperation of CDCL and Local Search for SAT
Cai S., Zhang X. (2021) Deep Cooperation of CDCL and Local Search for SAT. In: Li CM., Manyà F. (eds) Theory and Applications of Satisfiability Testing – SAT 2021. SAT 2021. Lecture Notes in Computer Science, vol 12831. Springer, Cham. https://doi-org-s.era.lib.swjtu.edu.cn/10.1007/978-3-030-80223-3_6
Abstract
|
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. |
|
1 Introduction
| SAT solvers are often used as a core component of more complex tools such as solvers for Satisfiability Module Theory (SMT), which are indispensable for program analysis and software verification. 译文：SAT求解器通常作为更复杂工具的核心组件，如满足性模块理论(SMT)求解器，在程序分析和软件验证中是必不可少的。 | |
| CDCL is evolved from the DPLL backtracking procedure [14], and usually involves a number of key techniques, mainly including 1) clause learning from conflicts [36], 2) exploiting the structure of conflicts during clause learning [36], 3) learnt clause management scheme [4], 4) lazy data structures for the representation of formulas [31], 5) effective branching heuristics, e.g., VSIDS [31], and 6) periodically restarting [18]. Additional techniques used in recent CDCL solvers include phase saving [34], switching between “stabilizing” mode (seldom-restart) and frequent-restart mode [33], clause veriification [29], among others. | |
|
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. |
|
| We apply our techniques to three state-of-the-art CDCL solvers, including the latest version of glucose [4], and the winner of the Main track of SAT Competition 2019 and 2020 namely MapleLCMDistChronoBT-DL [22] and Kissat_sat [10]. The experimental results show that our techniques allow them to solve a remarkable number of additional instances in the main track benchmark of SAT Competition 2017–2020. 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. Besides, the improved version of the three CDCL solvers also shows better results on a real world benchmark arising from a spectrum repacking problem in the context of bandwidth auction. | |
| Seen from experiments, the promising branches exploration technique and the local search based phase resetting techniques are very helpful to solve satisfiable instances, with a price of slight degradation on unsatisfiable instances (usually solving 2 or 3 fewer unsatisfiable instances). The local search conflict frequency enhanced branching strategy can be positive to satisfiable and also saves back a few unsatisfiable instances. Overall, these techniques significantly improves the performance of the CDCL solvers, leading to a remarkable increase on the number of total solved instances. | |
2 Preliminaries
2.1 Preliminary Definitions and Notations |
|
| 。。。 | |
2.2 CDCL Solvers |
|
2.3 Local Search Solvers |
|
| For local search algorithms, we need to define the search space and a neighborhood relation. In the context of SAT, the search space is the set of complete assignments which can be characterized as the set of strings {0,1}n{0,1}n, where n is the number of variables in the formula. For SAT, the seemingly most natural neighborhood N maps candidate solutions to their set of Hamming neighbors, i.e., candidate solutions that differ in exactly one variable. A local search algorithm starts from a position of search space and then moves to one neighbor of the current position in each step, trying to find a position which represents a satisfying assignment. | |
2.4 Experiment Preliminaries |
|
标签：Search,CDCL,solver,--,search,solvers,local,SAT 来源： https://www.cnblogs.com/yuweng1689/p/15517766.html