决策变元选择_决策分支策略——文献学习An Empirical Study of Branching Heuristics Through the Lens of Global Learning Ra

2023-10-26 09:42:46

An Empirical Study of Branching Heuristics Through the Lens of Global Learning Rate

Liang J.H., V.K. H.G., Poupart P., Czarnecki K., Ganesh V. (2017) An Empirical Study of Branching Heuristics Through the Lens of Global Learning Rate. In: Gaspers S., Walsh T. (eds) Theory and Applications of Satisfiability Testing – SAT 2017. SAT 2017. Lecture Notes in Computer Science, vol 10491. Springer, Cham

 

Abstract

In this paper, we analyze a suite of 7 well-known branching heuristics proposed by the SAT community and show that the better heuristics tend to generate more learnt clauses per decision, a metric we define as the global learning rate (GLR).（定义为全局学习率的度量标准）

Like our previous work on the LRB branching heuristic, we once again view these heuristics as techniques to solve the learning rate optimization problem. First, we show that there is a strong positive correlation between GLR and solver efficiency for a variety of branching heuristics. Second, we test our hypothesis further by developing a new branching heuristic that maximizes GLR greedily(贪婪分支启发式).

 

首先揭示GLR与各种决策策略是正相关；

其次提出了maximizes GLR greedily.

第三提出机器学习算法是一个很好的廉价逼近贪婪GLR最大化启发式的方法——SGDB决策分支算法

We show empirically that this heuristic achieves very high GLR and interestingly very low literal block distance (LBD) over the learnt clauses. 译文：我们的经验表明，这种启发式获得非常高的GLR和非常有趣的非常低的文字块距离(LBD)学习子句。

 

In our experiments this greedy branching heuristic enables the solver to solve instances faster than VSIDS, when the branching time is taken out of the equation.译文：在我们的实验中，当分支时间从方程中去掉时，这种贪婪分支启发式使求解者比VSIDS更快地解决实例。

 

This experiment is a good proof of concept that a branching heuristic maximizing GLR will lead to good solver performance modulo the computational overhead.译文：该实验很好地证明了最大化GLR的分支启发式算法在计算开销的基础上可以获得较好的求解性能。

 

Third, we propose that machine learning algorithms are a good way to cheaply approximate the greedy GLR maximization heuristic as already witnessed by LRB. 译文：第三，我们提出机器学习算法是一个很好的廉价逼近贪婪GLR最大化启发式的方法，LRB已经证明。

 

In addition, we design a new branching heuristic, called SGDB, that uses a stochastic gradient descent online learning method to dynamically order branching variables in order to maximize GLR. We show experimentally that SGDB performs on par with the VSIDS branching heuristic.

译文：此外，我们还设计了一种新的分支启发式算法，称为SGDB，它使用随机梯度下降在线学习方法对分支变量进行动态排序，以使GLR最大化。我们通过实验证明，SGDB的性能与VSIDS的分支启发式相当。
 

1 Introduction

Searching through a large, potentially exponential, search space is a reoccurring problem in many fields of computer science. Rather than reinventing the wheel and implementing complicated search algorithms from scratch, many researchers in fields as diverse as software engineering [7], hardware verification [9], and AI [16] have come to rely on SAT solvers as a general purpose tool to efficiently search through large spaces. By reducing the problem of interest down to a Boolean formula, engineers and scientists can leverage off-the-shelf SAT solvers to solve their problems without needing expertise in SAT or developing special-purpose algorithms.
译文：在计算机科学的许多领域中，搜索一个巨大的潜在指数搜索空间是一个反复出现的问题。译文：在软件工程[7]、硬件验证[9]和AI[16]等不同领域的许多研究人员并没有重新发明*并从头开始实现复杂的搜索算法，而是开始依赖于SAT求解器作为通用工具来在大空间中高效搜索。译文：通过将感兴趣的问题简化为一个布尔公式，工程师和科学家可以利用现成的SAT解决方案来解决他们的问题，而不需要SAT方面的专业知识或开发特殊用途的算法。
Modern conflict-driven clause-learning (CDCL) SAT solvers can solve a wide-range of practical problems with surprising efficiency, thanks to decades of ongoing research by the SAT community. Two notable milestones that are key to the success of SAT solvers are the Variable State Independent Decaying Sum (VSIDS) branching heuristic (and its variants) [23] and conflict analysis techniques [22]. The VSIDS branching heuristic has been the dominant branching heuristic since 2001, evidenced by its presence in most competitive solvers such as Glucose [4], Lingeling [5], and CryptoMiniSat [26].

译文：现代冲突驱动的clause-learning (CDCL) SAT解决器能够以惊人的效率解决广泛的实际问题，这要归功于SAT社区进行了几十年的持续研究。

译文：两个值得注意的里程碑是SAT求解成功的关键是变量状态独立衰减和(VSIDS)分支启发式(及其变体)[23]和冲突分析技术[22]。

译文：自2001年以来，VSIDS分支启发式一直是占主导地位的分支启发式，其存在于大多数竞争性求解程序中，如葡萄糖[4]、Lingeling[5]和CryptoMiniSat[26]。
 
One of the challenges in designing branching heuristics is that it is not clear what constitutes a good decision variable. We proposed one solution to this issue in our LRB branching heuristic paper [19], which is to frame branching as an optimization problem. We defined a computable metric called learning rate and defined the objective as maximizing the learning rate. Good decision variables are ones with high learning rate. Since learning rate is expensive to compute a priori, we used a multi-armed bandit learning algorithm to estimate the learning rate on-the-fly as the basis for the LRB branching heuristic [19].

译文：在我们的LRB分支启发式论文[19]中，我们提出了一个解决方案，即将框架分支作为一个优化问题。译文：设计分支启发式的挑战之一是不清楚什么构成了一个好的决策变量。

译文：我们定义了一个可计算的度量称为学习率，并将目标定义为最大化学习率。译文：好的决策变量是学习率高的决策变量。由于先验计算学习率代价高昂，因此我们使用多武装匪徒学习算法来实时估计学习率，作为LRB分支启发式[19]的基础。
 
In this paper, we deepen our previous work and our starting point remains the same, namely, branching heuristics should be designed to solve the optimization problem of maximizing learning rate. In LRB, the learning rate metric is defined per variable. In this paper, we define a new metric, called the global learning rate (GLR) to measure the solver’s overall propensity to generate conflicts, rather than the variable-specific metric we defined in the case of LRB. Our experiments demonstrate that GLR is an excellent objective to maximize.
译文：在本文中，我们深化了之前的工作，但我们的出发点是相同的，即设计分支启发式来解决学习率最大化的优化问题。译文：在LRB中，每个变量定义了学习速率度量。译文：在本文中，我们定义了一个新的度量，称为全局学习率(GLR)来度量求解者产生冲突的总体倾向，而不是我们在LRB情况下定义的变量特定度量。译文：我们的实验证明，GLR是一个极好的目标最大化。

Contributions
  • A new objective for branching heuristic optimization: In our previous work with LRB, we defined a metric that measures learning rate per variable. In this paper, we define a metric called the global learning rate (GLR), that measures the number of learnt clauses generated by the solver per decision, which intuitively is a better metric to optimize since it measures the solver as a whole. We show that the objective of maximizing GLR is consistent with our knowledge of existing branching heuristics, that is, the faster branching heuristics tend to achieve higher GLR. We perform extensive experiments over 7 well-known branching heuristics to establish the correlation between high GLR and better solver performance (Sect. 3).

译文：一种新的分支启发式优化目标:我们定义了一个称为全局学习率(GLR)的度量指标，它度量求解器每次决策生成的学习子句的数量，直观上，它是一个更好的度量指标，因为它度量的是求解器作为一个整体。

译文：我们表明，最大化GLR的目标与我们对现有分支启发式的认识是一致的，即越快的分支启发式越容易获得更高的GLR。我们对7个众所周知的分支启发式进行了广泛的实验，以建立高GLR和更好的求解器性能之间的相关性(第3节)。
  • A new branching heuristic to greedily maximize GLR: To further scientifically test the conjecture that GLR maximization is a good objective, we design a new branching heuristic that greedily maximizes GLR by always selecting decision variables that cause immediate conflicts. It is greedy in the sense that it optimizes for causing immediate conflicts, and it does not consider future conflicts as part of its scope. Although the computational overhead of this heuristic is very high, the variables it selects are “better” than VSIDS. More precisely, if we ignore the computation time to compute the branching variables, the greedy branching heuristic generally solves more instances faster than VSIDS. Another positive side-effect of the greedy branching heuristic is that relative to VSIDS, it has lower learnt clause literal block distance (LBD) [3], a sign that it is learning higher quality clauses. The combination of learning faster (due to higher GLR) and learning better (due to lower LBD) clauses explains the power of the greedy branching heuristic. Globally optimizing the GLR considering all possible future scenarios a solver can take is simply too prohibitive. Hence, we limited our experiments to the greedy approach. Although this greedy branching heuristic takes too long to select variables in practice, it gives us a gold standard of what we should aim for. We try to approximate it as closely as possible in our third contribution (Sect. 4).

译文：贪婪地最大化GLR的新分支启发式:译文：我们设计了一种新的分支启发式，通过总是选择导致直接冲突的决策变量来贪婪地最大化GLR。

译文：它是贪婪的，因为它优化了眼前的冲突，而不考虑未来的冲突。尽管这种启发式的计算开销非常大，但它选择的变量“更好”于VSIDS。

译文：更准确地说，如果我们忽略计算分支变量的计算时间，贪婪分支启发式算法通常比VSIDS更快地解决更多的实例。

译文：贪婪分支启发式的另一个积极的副作用是，相对于VSIDS，它学习的子句文字块距离(LBD)[3]更低，表明它学习的子句质量更高。

译文：学习更快(由于较高的GLR)和学习更好(由于较低的LBD)子句的结合解释了贪婪分支启发式的威力。

译文：全局优化GLR，考虑所有可能的未来场景，求解者可以采取简直是太禁止。因此，我们的实验限于贪心方法。尽管在实践中，这种贪婪的分支启发式在选择变量方面花费了太长的时间，但它为我们应该追求的目标提供了一个黄金标准。在我们的第三篇文章(第4节)中，我们试图尽可能地接近它。
  • A new machine learning branching heuristic to maximize GLR: We design a second heuristic, called stochastic gradient descent branching (SGDB), using machine learning to approximate our gold standard, the greedy branching heuristic. SGDB trains an online logistic regression model by observing the conflict analysis procedure as the CDCL algorithm solves an instance. As conflicts are generated, SGDB will update the model to better fit its observations. Concurrently, SGDB also uses this model to rank variables based on their likelihood to generate conflicts if branched on. We show that in practice, SGDB is on par with the VSIDS branching heuristic over a large and diverse benchmark but still shy of LRB. However, more work is required to improve the learning in SGDB (Sect. 5).

译文：一种新的最大化GLR的机器学习分支启发式算法：译文：我们设计了第二个启发式，称为随机梯度下降分支(SGDB)，使用机器学习来近似我们的黄金标准，贪婪分支启发式。译文：SGDB通过观察CDCL算法解决实例时的冲突分析过程，训练一个在线逻辑回归模型。

译文：当冲突产生时，SGDB将更新模型以更好地适应其观察结果。同时，SGDB也使用这个模型根据变量在分支时产生冲突的可能性来对变量进行排序。译文：同时，SGDB也使用这个模型根据变量在分支时产生冲突的可能性来对变量进行排序。
 

 

 

References

  1. 1. https://sites.google.com/a/gsd.uwaterloo.ca/maplesat/
  2. 2. https://sites.google.com/a/gsd.uwaterloo.ca/maplesat/sgd
  3. 3. Audemard, G., Simon, L.: Predicting learnt clauses quality in modern SAT solvers. In: Proceedings of the 21st International Joint Conference on Artificial Intelligence, IJCAI 2009, pp. 399–404. Morgan Kaufmann Publishers Inc., San Francisco (2009)
  4. 4. Audemard, G., Simon, L.: Glucose 2.3 in the SAT 2013 Competition. In: Proceedings of SAT Competition 2013, pp. 42–43 (2013)
  5. 5. Biere, A.: Lingeling, Plingeling, PicoSAT and PrecoSAT at SAT Race 2010. FMV Report Series Technical Report 10(1) (2010)
  6. 6. Bottou, L.: On-line Learning in Neural Networks. On-line Learning and Stochastic Approximations, pp. 9–42. Cambridge University Press, New York (1998)
  7. 7. Cadar, C., Ganesh, V., Pawlowski, P.M., Dill, D.L., Engler, D.R.: EXE: automatically generating inputs of death. In: Proceedings of the 13th ACM Conference on Computer and Communications Security, CCS 2006, pp. 322–335. ACM, New York (2006)
  8. 8. Carvalho, E., Silva, J.P.M.: Using rewarding mechanisms for improving branching heuristics. In: Online Proceedings of The Seventh International Conference on Theory and Applications of Satisfiability Testing, SAT 2004, 10–13 May 2004, Vancouver, BC, Canada, (2004)
  9. 9. Clarke, E., Biere, A., Raimi, R., Zhu, Y.: Bounded model checking using satisfiability solving. Formal Meth. Syst. Des. 19(1), 7–34 (2001)
  10. 10. Cox, D.R.: The regression analysis of binary sequences. J. Roy. Stat. Soc.: Ser. B (Methodol.) 20(2), 215–242 (1958)
  11. 11. 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). doi: 10.1007/978-3-540-24605-3_37
  12. 12. Fisher, R.A.: Frequency distribution of the values of the correlation coefficient in samples from an indefinitely large population. Biometrika 10(4), 507–521 (1915
  13. 13. Goldberg, E., Novikov, Y.: BerkMin: a fast and robust SAT-solver. Discrete Appl. Math. 155(12), 1549–1561 (2007)
  14. 14. Jeroslow, R.G., Wang, J.: Solving propositional satisfiability problems. Ann. Math. Artif. Intell. 1(1–4), 167–187 (1990)
  15. 15. Katebi, H., Sakallah, K.A., Marques-Silva, J.P.: Empirical study of the anatomy of modern SAT solvers. In: Sakallah, K.A., Simon, L. (eds.) SAT 2011. LNCS, vol. 6695, pp. 343–356. Springer, Heidelberg (2011). doi: 10.1007/978-3-642-21581-0_27
  16. 16. Kautz, H., Selman, B.: Planning as satisfiability. In: Proceedings of the 10th European Conference on Artificial Intelligence, ECAI 1992, pp. 359–363. Wiley Inc., New York (1992)
  17. 17. Lagoudakis, M.G., Littman, M.L.: Learning to select branching rules in the DPLL procedure for satisfiability. Electron. Notes Discrete Math. 9, 344–359 (2001)
  18. 18. Liang, J.H., Ganesh, V., Poupart, P., Czarnecki, K.: Exponential recency weighted average branching heuristic for SAT solvers. In: Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence, AAAI 2016, pp. 3434–3440. AAAI Press (2016)
  19. 19. Liang, J.H., Ganesh, V., Poupart, P., Czarnecki, K.: Learning rate based branching heuristic for SAT solvers. In: Proceedings of the 19th International Conference on Theory and Applications of Satisfiability Testing, SAT 2016, Bordeaux, France, 5–8 July 2016, pp. 123–140 (2016)r
  20. 20. Luby, M., Sinclair, A., Zuckerman, D.: Optimal speedup of Las Vegas algorithms. Inf. Process. Lett. 47(4), 173–180 (1993)
  21. 21. Marques-Silva, J.P.: The impact of branching heuristics in propositional satisfiability algorithms. In: Barahona, P., Alferes, J.J. (eds.) EPIA 1999. LNCS, vol. 1695, pp. 62–74. Springer, Heidelberg (1999). doi: 10.1007/3-540-48159-1_5
  22. 22. Marques-Silva, J.P., Sakallah, K.A.: GRASP-a new search algorithm for satisfiability. In: Proceedings of the 1996 IEEE/ACM International Conference on Computer-aided Design, ICCAD 1996, pp. 220–227. IEEE Computer Society, Washington, D.C. (1996)
  23. 23. Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient SAT solver. In: Proceedings of the 38th Annual Design Automation Conference, DAC 2001, pp. 530–535. ACM, New York (2001)
  24. 24. Murphy, K.P.: Machine Learning: A Probabilistic Perspective. The MIT Press, Cambridge (2012)
  25. 25. Pipatsrisawat, K., Darwiche, A.: A lightweight component caching scheme for satisfiability solvers. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol. 4501, pp. 294–299. Springer, Heidelberg (2007). doi: 10.1007/978-3-540-72788-0_28
  26. 26. Soos, M.: CryptoMiniSat v4. SAT Competition, p. 23 (2014)
  27. 27. Spearman, C.: The proof and measurement of association between two things. Am. J. Psychol. 15(1), 72–101 (1904)
  28. 28. Stump, A., Sutcliffe, G., Tinelli, C.: StarExec: a cross-community infrastructure for logic solving. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS, vol. 8562, pp. 367–373. Springer, Cham (2014). doi: 10.1007/978-3-319-08587-6_28

 

上一篇：linux shell命令中调试的set -n


下一篇：Zookeeper--概述、安装