决策变元选择_决策分支策略——文献学习Exploiting Glue Clauses to Design Effective CDCL Branching Heuristics

2024-02-19 21:48:40

Exploiting Glue Clauses to Design Effective CDCL Branching Heuristics

Chowdhury M.S., Müller M., You JH. (2019) Exploiting Glue Clauses to Design Effective CDCL Branching Heuristics. In: Schiex T., de Givry S. (eds) Principles and Practice of Constraint Programming. CP 2019. Lecture Notes in Computer Science, vol 11802. Springer, Cham

决策变量选择策略——选在那些出现在粘合子句中的文字做为决策变量更有利于冲突的生成。

Abstract

In conflict-directed clause learning (CDCL) SAT solving, a state-of-the-art criterion to measure the importance of a learned clause is called literal block distance (LBD), which is the number of distinct decision levels in the clause. The lower the LBD score of a learned clause, the better is its quality. The learned clauses with LBD score of 2, called glue clauses, are known to possess high pruning power. In this work, we relate glue clauses to decision variables. First, we show experimentally that branching decisions with variables appearing in glue clauses, called glue variables, are more conflict efficient than with nonglue variables. This observation motivated the development of a structure-aware CDCL variable bumping scheme, which increases the heuristic score of a glue variable based on its appearance count in the glue clauses that are learned so far by the search. Empirical evaluation shows the effectiveness of the new method on the main track instances from SAT Competitions 2017 and 2018 with four state-of-the-art CDCL SAT solvers. Finally, we show that the frequency of learned clauses that are glue clauses can be used as a reliable indicator of solving efficiency for some instances, for which the standard performance metrics fail to provide a consistent explanation.

译文：衡量已学习子句重要性的最先进标准称为文字块距离(LBD)，它是子句中不同决策级别的数量. 译文：学习语句的LBD分数越低，其质量越好. 译文：已知LBD得分为2的学习子句称为glue子句，具有较高的剪枝能力。

 

译文：在本文中，我们将glue子句与决策变量联系起来。首先，我们通过实验证明，带有出现在粘合子句中的变量的分支决策(称为粘合变量)，比带有非粘合变量的分支决策更具有冲突效率。

 

译文：这一观察结果促使开发了具有结构感知的CDCL变量碰撞方案，该方案基于glue变量在搜索到目前为止学到的glue子句中的外观计数增加了它的启发式分数。经验评价表明，新方法在2017年和2018年SAT比赛的主要赛道实例上的有效性，4个最先进的CDCL SAT求解器。

 

译文：最后，我们表明，对于某些情况，在标准性能指标无法提供一致解释的情况下，作为粘合子句的学习频率可以作为求解效率的可靠指标。

Keywords

CDCL    SAT Branching heuristics    Glue clauses 

 

1 Introduction

Given a formula FF of boolean variables, the task of SAT solving is to determine a variable assignment that satisfies FF or to report the unsatisfiability of FF in case no such assignment exists. SAT is known to be NP-complete [5]. Despite the hardness, modern CDCL SAT solvers can solve large real-world problems from important domains, such as hardware design verification [8], software debugging [4], planning [21], and encryption [18, 23], sometimes with surprising efficiency. This is the result of a careful combination of its key components, such as preprocessing [6, 10] and inprocessing [11, 17], robust branching heuristics [13, 14, 19], efficient restart policies [2, 20], intelligent conflict analysis [22], and effective clause learning [19].
 
Clause learning prunes search space. As conflict discovery is the only way to learn clauses, the rate of discovery is critical for CDCL SAT solvers. As a large amount of learned clauses reduces the overall performance, the management of the learned clause database also becomes a key component of a modern CDCL SAT solver [19, 22].
 
In earlier CDCL SAT solvers, the size and recent activities of learned clauses were the dominant criteria for determining the relevance of learned clauses [7]. The CDCL SAT solver Glucose [1] was the first to apply a new measure called literal block distance (LBD), which indicates the number of distinct decision levels in a learned clause. The learned clauses with LBD score of 2, called glue clauses, are of particular interest [1, 20] because a glue clause connects a block of closely related variables, and thus a relatively small number of decisions are needed to make it a unit clause (i.e., a clause that has all but one literals assigned under the current partial assignment). A glue clause therefore may cause a faster generation of conflicts within fewer numbers of decisions, which leads to pruning of the search space. Simply put, glue clauses have higher potential to reduce search space more quickly than other learned clauses. For this reason, all modern CDCL SAT solvers permanently store glue clauses.
 
nspired by the intuitive characteristics of glue clauses, we ask the following question: Can glue clauses be used to help re-rank decision variables to improve search efficiency? We call the decision variables that have appeared in at least one glue clause up to the current search state glue variables, and others nonglue variables.
 

The main contributions of this paper are:

    • We conduct an experiment using the 750 instances from the main track of SAT Competition 2017 and 2018 (abbreviated as SAT-2017 and SAT-2018, respectively) with four state-of-the-art CDCL SAT solvers: glucose 4.11 (just called Glucose), MAPLECOMSPS_PURE_LRB2 (abbreviated as MapleLRB), Maple_LCM_Dist3 (abbreviated as MLD, winner of SAT-2017) and MapleLCMDistChronoBT4 (abbreviated as MLD_CBT, winner of SAT-2018). Our experiment shows that decisions with glue variables are more conflict efficient than those with nonglue variables. Furthermore, glue variables are picked up by CDCL branching heuristics disproportionately more often.

    • We design a structure-aware variable score bumping method called Glue Bumping (GB), which dynamically bumps activity score of a glue variable based on its current activity score and (normalized) glue level, which is a measure of the count of glue clauses in which the variable appears. The method is simple to implement.

    • We implemented the GB method on top of the same four SAT solvers mentioned above. For the 750 instances from SAT-2017 and SAT-2018, all GB extensions solve more instances than the baselines and achieve lower PAR-2 scores5. One of our extended solver solves 9 additional instances over the instances from SAT-2017. According to [2], this level of performance gain closely resembles to the introduction of a critical feature, which is remarkable, given the simplicity of the new method.

    • We provide evidence that the frequency of glue clauses in learned clauses may serve as a reliable indicator of solving efficiency. In [16], the authors reported correlations between solving efficiency of branching heuristics and standard metrics based on the global learning rate (GLR) and average LBD (aLBD) scores - higher solving efficiency is indicated by higher average GLR and lower average aLBD. We show that these two measures do not provide a consistent explanation of solving efficiency for some subsets of SAT-2017 and SAT-2018, for which the correlations are highly expected to hold. However, using a new measure based on the frequency of learned clauses that are glue, we are able to provide a consistent explanation.
 
The next section provides preliminaries. Section 3 reports an experiment on the role of glue variables in CDCL SAT solving, which motivates the design of a bumping scheme in Sect. 4. Section 5 reports an experimental analysis. In Sect. 7 we explain why our standard bumping scheme does not work very well for Glucose and how to fix the issue. Section 8 reports some additional experimental results with the GB method. Section 9 is about related work and future directions can be found in Sect. 10.
 

2 Preliminaries

2.1 Inner Working of a CDCL Solver

A CDCL SAT solver works by extending an initially empty partial assignment using two operations in an interleaving fashion: a branching decision and unit propagation (UP). A branching decision selects an unassigned variable by using a branching heuristic and assigns a boolean value to it. Following a branching decision, UP simplifies F by deducing a new set of implied variable assignments. UP may lead to a conflict due to a falsified or conflicting clause. Conflict analysis determines the root cause of a conflict and generates a learned clause that is added to F to prevent the conflict from reappearing in the future, thereby pruning the search. Search continues from a backjumping level computed from the learned clause. We refer the reader to [3] for more details on CDCL SAT solving.

译文：CDCL SAT求解器通过使用交叉方式的两个操作扩展最初的空部分分配来工作:分支决策和单元传播。

译文：分支决策使用分支启发式选择一个未分配的变量，并给它赋一个布尔值。译文：在进行分支决策之后，UP通过推导一组新的隐含变量赋值来简化F。UP可能会由于失败或有冲突的条款而导致冲突。译文：冲突分析确定冲突的根本原因，并生成一个学习子句，添加到F中以防止冲突在未来再次出现，从而实现对搜索空间的剪枝。

译文：从learned子句计算的回跳级别继续搜索。有关CDCL SAT解决方案的更多细节，请读者参阅[3]。
 
 
 
 
 
 

 

 

 

 

References

  1. 1. Audemard, G., Simon, L.: Predicting learnt clauses quality in modern SAT solvers. In: Proceedings of IJCAI 2009, pp. 399–404 (2009)Google Scholar
  2. 2. Audemard, G., Simon, L.: Refining restarts strategies for SAT and UNSAT. In: Milano, M. (ed.) CP 2012. LNCS, pp. 118–126. Springer, Heidelberg (2012).  https://doi.org/10.1007/978-3-642-33558-7_11CrossRefGoogle Scholar
  3. 3. Biere, A., Heule, M., Maaren, H.V., Walsh, T.: Handbook of Satisfiability: Volume 185 Frontiers in Artificial Intelligence and Applications. IOS Press, Amsterdam (2009)Google Scholar
  4. 4. Cadar, C., Ganesh, V., Pawlowski, P.M., Dill, D.L., Engler, D.R.: EXE: automatically generating inputs of death. In: Proceedings of CCS 2006, pp. 322–335 (2006)Google Scholar
  5. 5. Cook, S.A.: The complexity of theorem-proving procedures. In: Proceedings of the 3rd Annual ACM Symposium on Theory of Computing 1971, pp. 151–158 (1971)Google Scholar
  6. 6. Eén, N., Biere, A.: Effective preprocessing in SAT through variable and clause elimination. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol. 3569, pp. 61–75. Springer, Heidelberg (2005).  https://doi.org/10.1007/11499107_5CrossRefzbMATHGoogle Scholar
  7. 7. Eén, N., Sörensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2004).  https://doi.org/10.1007/978-3-540-24605-3_37CrossRefGoogle Scholar
  8. 8. Gupta, A., Ganai, M.K., Wang, C.: SAT-based verification methods and applications in hardware verification. In: Bernardo, M., Cimatti, A. (eds.) SFM 2006. LNCS, vol. 3965, pp. 108–143. Springer, Heidelberg (2006).  https://doi.org/10.1007/11757283_5CrossRefzbMATHGoogle Scholar
  9. 9. Jamali, S., Mitchell, D.: Centrality-based improvements to CDCL heuristics. In: Beyersdorff, O., Wintersteiger, C.M. (eds.) SAT 2018. LNCS, vol. 10929, pp. 122–131. Springer, Cham (2018).  https://doi.org/10.1007/978-3-319-94144-8_8CrossRefGoogle Scholar
  10. 10. Järvisalo, M., Biere, A., Heule, M.: Blocked clause elimination. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 129–144. Springer, Heidelberg (2010).  https://doi.org/10.1007/978-3-642-12002-2_10CrossRefzbMATHGoogle Scholar
  11. 11. Järvisalo, M., Heule, M.J.H., Biere, A.: Inprocessing rules. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS (LNAI), vol. 7364, pp. 355–370. Springer, Heidelberg (2012).  https://doi.org/10.1007/978-3-642-31365-3_28CrossRefGoogle Scholar
  12. 12. Katsirelos, G., Simon, L.: Eigenvector centrality in industrial SAT instances. In: Milano, M. (ed.) CP 2012. LNCS, pp. 348–356. Springer, Heidelberg (2012).  https://doi.org/10.1007/978-3-642-33558-7_27CrossRefGoogle Scholar
  13. 13. Liang, J.H., Ganesh, V., Poupart, P., Czarnecki, K.: Exponential recency weighted average branching heuristic for SAT solvers. In: Proceedings of AAAI 2016, pp. 3434–3440 (2016)Google Scholar
  14. 14. Liang, J.H., Ganesh, V., Poupart, P., Czarnecki, K.: Learning rate based branching heuristic for SAT solvers. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 123–140. Springer, Cham (2016).  https://doi.org/10.1007/978-3-319-40970-2_9CrossRefzbMATHGoogle Scholar
  15. 15. Liang, J.H., Ganesh, V., Zulkoski, E., Zaman, A., Czarnecki, K.: Understanding VSIDS branching heuristics in conflict-driven clause-learning SAT solvers. In: Proceedings of Haifa Verification Conference, HVC 2015, pp. 225–241 (2015)Google Scholar
  16. 16. Liang, J.H., Hari Govind, V.K., Poupart, P., Czarnecki, K., Ganesh, V.: An empirical study of branching heuristics through the lens of global learning rate. In: Gaspers, S., Walsh, T. (eds.) SAT 2017. LNCS, vol. 10491, pp. 119–135. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-66263-3_8CrossRefzbMATHGoogle Scholar
  17. 17. Luo, M., Li, C.-M., Xiao, F., Manyà, F., Lü, Z.: An effective learnt clause minimization approach for CDCL SAT solvers. In: Proceedings of IJCAI 2017, pp. 703–711 (2017)Google Scholar
  18. 18. Massacci, F., Marraro, L.: Logical cryptanalysis as a SAT problem. J. Autom. Reasoning 24(1/2), 165–203 (2000)MathSciNetCrossRefGoogle Scholar
  19. 19. Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient SAT solver. In: Proceedings of Design Automation Conference, DAC 2001, pp. 530–535 (2001)Google Scholar
  20. 20. Oh, C.: Between SAT and UNSAT: the fundamental difference in CDCL SAT. In: Heule, M., Weaver, S. (eds.) SAT 2015. LNCS, vol. 9340, pp. 307–323. Springer, Cham (2015).  https://doi.org/10.1007/978-3-319-24318-4_23CrossRefGoogle Scholar
  21. 21. Rintanen, J.: Engineering efficient planners with SAT. In: Proceedings of ECAI 2012, pp. 684–689 (2012)Google Scholar
  22. 22. Marques Silva, J.P., Sakallah, K.A.: GRASP: a search algorithm for propositional satisfiability. IEEE Trans. Comput. 48(5), 506–521 (1999)MathSciNetCrossRefGoogle Scholar
  23. 23. Soos, M., Nohl, K., Castelluccia, C.: Extending SAT solvers to cryptographic problems. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 244–257. Springer, Heidelberg (2009).  https://doi.org/10.1007/978-3-642-02777-2_24CrossRefGoogle Scholar
  24. 24. Xiao, F., Luo, M., Li, C.-M., Manya, F., Lu, Z.: MapleLRB__LCM, Maple__LCM, Maple__LCM__Dist, MapleLRB__LCMoccRestart and Glucose3.0+width in sat competition 2017. In: Proceedings of SAT Competition 2017, pp. 22–23 (2017)Google Scholar
上一篇：【2019年8月】OCP 071认证考试最新版本的考试原题-第18题


下一篇：[学习笔记]2-SAT