SLS与CDCL结合——文献学习CCAnr: A Configuration Checking Based Local Search Solver for Non-random Satisfiabil

Posted 2020-12-12 yuweng1689

CCAnr: A Configuration Checking Based Local Search Solver for Non-random Satisfiability

Cai S., Luo C., Su K. (2015) CCAnr: A Configuration Checking Based Local Search Solver for Non-random Satisfiability. In: Heule M., Weaver S. (eds) Theory and Applications of Satisfiability Testing -- SAT 2015. SAT 2015. Lecture Notes in Computer Science, vol 9340. Springer, Cham

 

CCAnr  performs unit propagation before local search。

---

 

 

Abstract

This paper presents a stochastic local search (SLS) solver for SAT named CCAnr, which is based on the configuration checking strategy and has good performance on non-random SAT instances. 译文：摘要提出了一种基于配置检查策略的SAT随机局部搜索(SLS)求解器CCAnr，该求解器在非随机SAT实例中具有良好的性能

CCAnr switches between two modes: it flips a variable according to the CCA (configuration checking with aspiration) heuristic if any; otherwise, it flips a variable in a random unsatisfied clause (which we refer to as the focused local search mode). 译文：CCAnr在两种模式之间切换:它根据CCA(依照渴望进行配置检测)启发式(如果有的话)翻转变量;否则，它将翻转一个随机的unsatisfy子句中的变量(我们将其称为焦点本地搜索模式)。 两种翻转变量策略： 根据CCA(依照渴望进行配置检测)启发式翻转变量； 翻转一个随机的unsatisfy子句中的变量——焦点本地搜索模式；

The main novelty of CCAnr lies on the greedy heuristic in the focused local search mode, which contributes significantly to its good performance on structured instances.  译文：CCAnr的主要新颖之处在于集中局部搜索模式中的贪婪启发式，这极大地提高了它在结构化实例上的良好性能

Previous two-mode SLS algorithms usually utilize diversifying heuristics such as age or randomized strategies to pick a variable from the unsatisfied clause. 译文：以前的双模式SLS算法通常利用多样化的启发式方法，如年龄或随机策略，从未满足的子句中选择一个变量。   Our experiments on combinatorial and application benchmarks from SAT Competition 2014 show that CCAnr has better performance than other state-of-the-art SLS solvers on structured instances, and its performance can be further improved by using a preprocessor CP3. 译文：我们在SAT Competition 2014的组合和应用基准测试上的实验表明，CCAnr在结构化实例上比其他最先进的SLS求解器有更好的性能，并且可以通过使用预处理器CP3进一步提高其性能。

Our results suggest that a greedy heuristic in the focused local search mode might be helpful to improve SLS solvers for solving structured SAT instances. 译文：我们的结果表明，在集中局部搜索模式下的贪婪启发式可能有助于改进求解结构化SAT实例的SLS算法。

1 Introduction

The Satisfiability problem (SAT) is a prototypical NP-complete problem of importance in both theory and applications. Two popular approaches for solving SAT are conflict driven clause learning (CDCL) and stochastic local search (SLS). SLS algorithms for SAT perform a local search in the space of truth assignments by starting with a complete assignment, and then repeatedly flipping the truth value of a variable until a satisfying assignment has been found or some limits (usually the time limit) have been reached. The function for choosing the variable to be flipped is usually denoted as pickVar.

译文：可满足性问题是一个典型的np完全问题，具有重要的理论和应用价值。解决SAT的两种常用方法是冲突驱动子句学习(CDCL)和随机局部搜索(SLS)。 SLS算法的基本描述： SAT的SLS算法在真值分配空间中执行局部搜索，从一个完整的分配开始，然后反复翻转变量的真值，直到找到一个令人满意的分配或达到某些限制(通常是时间限制)。选择要翻转的变量的函数通常表示为pickVar。

SLS algorithms for SAT mainly fall into two types: focused local search (FLS) and two-mode SLS. 译文：SAT的SLS算法主要分为两类:聚焦局部搜索(focus local search, FLS)和双模式SLS。   Focused local search (as called in [15,17]) always picks the flip variable from an unsatisfied clause [13,19]; 译文：集中局部搜索(在[15,17]中调用)总是从未满足的子句[13,19]中选择flip变量;   two-mode SLS [1,5,10,16,18] switches between “global local search” (where the flip variable is chosen from a candidate set filtered from the set of all variables) and focused local search, usually depending on whether a local optimum is reached. 译文：双模式SLS[1,5,10,16,18]在“全局局部搜索”(翻转变量是从所有变量的集合中筛选出来的候选集合中选择)和集中局部搜索之间切换，通常取决于是否达到了局部最优。   Also, there is a significant line of research concerns about weighting techniques [8,14,20,21], which are usually utilized in two-mode SLS algorithms. 译文：此外，还有一个重要的研究关注加权技术[8,14,20,21]，它通常用于双模式SLS算法。

SLS is well known as the most effective approach for solving random satisfiable instances, and SLS solvers are often evaluated on random k-SAT benchmarks. 译文：SLS是求解随机可满足实例的最有效方法，SLS求解器通常在随机k-SAT基准上进行评估 For structured instances, SLS solvers have been considered not effective as complete solvers (particularly CDCL ones) for a long time. 译文：对于结构化实例，长期以来，SLS求解器一直被认为不是有效的完整求解器(特别是CDCL)。   Nevertheless, recent progress shows promising results of SLS solvers, particularly two-mode SLS solvers, on crafted satisfiable instances. Modern two-mode SLS solvers are competitive and complementary with complete solvers in solving crafted instances. 译文：然而，最近的进展显示了SLS求解器，特别是双模式SLS求解器在精心设计的可满足实例上的良好结果。现代的双模式SLS求解器在求解精心制作的实例时与完全求解器是竞争和互补的。 For example, in the crafted SAT track of SAT Competition 2009, the SLS solver Sattime solved 109 instances while the best CDCL solved 93 instances [11]; in SAT Competition 2013, CCAnr solved 21 crafted SAT instances that the best complete solver glucose (v2.3) failed to solve, while glucose solved 53 instances that CCAnr failed to solve in the same track (Hard-combinatorial SAT track). Indeed, the top three solvers in the Hard-combinatorial SAT track of SAT Competition 2014, namely Sparrow2riss [2], CCAnr+glucose [3] and SGseq [9] are all hybrid solvers combining an SLS solver and a complete solver。 译文：的确，2014年SAT竞赛硬组合SAT轨道前三名的Sparrow2riss[2]、CCAnr+glucose[3]和SGseq[9]都是一个SLS求解器和一个complete求解器相结合的混合求解器。

【CDCL与SLS结合的求解器】 　　Sparrow2riss 　  CCAnr+glucose　　SGseq

In this paper, we present the CCAnr solver, which is a two-mode SLS solver designed for solving structured instances. 译文：我们提出了CCAnr求解器，这是一个为求解结构化实例而设计的双模式SLS求解器。 Existing two-mode SLS solvers for SAT, including state-of-the-art ones such as Sparrow [1], Sattime [11] and CCASat [5], employ greedy heuristics in the global local search mode with the aim of decreasing the number of unsatisfied clauses, and employ diversifying heuristics in the focused local search mode with the aim of better exploring the search space and avoiding local optima. 译文：现有的用于SAT的双模式SLS求解器，包括最先进的，如Sparrow[1]、Sattime[11]和CCASat [5] 译文：在全局局部搜索模式中采用贪婪启发式，以减少不满足子句的数量;在集中局部搜索模式中采用多样化启发式，以更好地探索搜索空间，避免局部最优。   However, CCAnr employs a greedy heuristic (i.e., picking the one with the greatest score) in the focused local search mode, which significantly contributes to its good performance on structured instances.   Our experiments comparing different versions of CCAnr with various heuristics in the focused local search mode show that, for solving structured instances, it could be helpful to incorporate greedy heuristics in the focused local search mode。 译文：我们的实验比较了不同版本的CCAnr在集中局部搜索模式下的不同启发式算法，结果表明，对于求解结构化实例，在集中局部搜索模式中引入贪心启发式是有帮助的。

The good performance of CCAnr as compared to other SLS solvers is also confirmed by the results in the SAT Competitions 2013 and 2014.译文：2013年和2014年SAT比赛的结果也证实了CCAnr相对于其他SLS求解器的良好性能。 In the Hardcombinatorial SAT track of SAT Competition 2013, CCAnr solves more instances than other SLS solvers except Sparrow+CP3, which solves only 2 more instances than CCAnr.   In SAT Competition 2014, CCAnr+glucose is ranked second in the same track, solving only 1 less instance than Sparrow2riss. However, we note that both Sparrow+CP3 and Sparrow2riss utilize a powerful preprocessor CP3 [12] while CCAnr only performs unit propagation before local search.   【知识点】 　　预处理器：CP3； 　　CCAnr只在局部搜索前执行单位传播。 In this sense, CCAnr can be considered as the best pure SLS solver in this track. In this paper, we also combine CCAnr with the preprocessor CP3, and the resulting solver solves more instances in those benchmarks, yielding further improvement over other SLS solvers.

2 Solver Description

CCAnr is built on top of the Swcca solver [4], and keeps the main technique there, namely the configuration checking (CC) strategy with an aspiration mechanism. In this section, we first introduce the CCA heuristic and the Swcca algorithm, and then describe the CCAnr algorithm by specifying the difference from Swcca. CCAnr is open-source and the code is available for download at http://lcs.ios. ac.cn/∼caisw/SAT.html. Readers interested in the implementation may like to refer to the codes for more details.

译文：CCAnr构建在Swcca求解器[4]之上，并保留了主要技术，即带有期望机制的配置检查(CC)策略。在本节中，我们首先介绍了CCA启发式和Swcca算法，然后通过说明与Swcca的区别来描述CCAnr算法。 译文：CCAnr是开源的，其代码可以在http://lcs.ios下载。ac.cn/∼caisw / SAT.html。对实现感兴趣的读者可以参考代码了解更多细节

 

 

 

 

References

1. Balint, A., Fr¨ohlich, A.: Improving stochastic local search for sat with a new probability distribution. In: Strichman, O., Szeider, S. (eds.) SAT 2010. LNCS, vol. 6175, pp. 10–15. Springer, Heidelberg (2010)

2. Balint, A., Manthey, N.: SparrowToRiss. In: Proc. of SAT Competition 2014: Solver and Benchmark Descriptions, p. 77 (2014)

3. Cai, S., Luo, C., Su, K.: CCAnr+glucose in SAT competition 2014. In: Proc. of SAT Competition 2014: Solver and Benchmark Descriptions, p. 17 (2014)

4. Cai, S., Su, K.: Configuration checking with aspiration in local search for SAT. In: Proceedings of the Twenty-Sixth AAAI Conference on Artificial Intelligence, AAAI 2012, pp. 334–340 (2012)

5. Cai, S., Su, K.: Local search for Boolean Satisfiability with configuration checking and subscore. Artif. Intell. 204, 75–98 (2013)

6. Cai, S., Su, K., Sattar, A.: Local search with edge weighting and configuration checking heuristics for minimum vertex cover. Artif. Intell. 175(9–10), 1672–1696 (2011)

7. Fr¨ohlich, A., Biere, A., Wintersteiger, C.M., Hamadi, Y.: Stochastic local search for satisfiability modulo theories. In: Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence, AAAI 2015, pp. 1136–1143 (2015)

8. Hutter, F., Tompkins, D.A.D., H. Hoos, H.: Scaling and probabilistic smoothing: efficient dynamic local search for SAT. In: Van Hentenryck, P. (ed.) CP 2002. LNCS, vol. 2470, pp. 233–248. Springer, Heidelberg (2002)

9. Li, C.M., Habet, D.: Description of RSeq2014. In: Proc. of SAT Competition 2014: Solver and Benchmark Descriptions, p. 72 (2014)

10. Li, C.-M., Huang, W.Q.: Diversification and determinism in local search for satisfiability. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol. 3569, pp. 158–172. Springer, Heidelberg (2005)

11. Li, C.M., Li, Y.: Satisfying versus falsifying in local search for satisfiability. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 477–478. Springer, Heidelberg (2012)

12. Manthey, N.: Coprocessor 2.0 – a flexible CNF simplifier. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 436–441. Springer, Heidelberg (2012)

13. McAllester, D.A., Selman, B., Kautz, H.A.: Evidence for invariants in local search. In: Proceedings of the 14th National Conference on Artificial Intelligence, AAAI 1997, pp. 321–326 (1997)

14. Morris, P.: The breakout method for escaping from local minima. In: Proceedings of the 11th National Conference on Artificial Intelligence, AAAI 1993, pp. 40–45 (1993)

15. Papadimitriou, C.H.: On selecting a satisfying truth assignment. In: Proceedings of the 32nd Annual Symposium on Foundations of Computer Science, FOCS 1991, pp. 163–169 (1991)

16. Pham, D.N., Gretton, C.: gNovelty+. In: Solver Description of SAT Competition 2007 (2007)