Branching Heuristic Combining in SAT

学习文献来源：

1. Combining VSIDS and CHB Using Restarts in SAT。

引用：

@inproceedings{DBLP:conf/cp/CherifHT21,author = {Mohamed Sami Cherif andDjamal Habet andCyril Terrioux},editor = {Laurent D. Michel},title = {Combining {VSIDS} and {CHB} Using Restarts in {SAT}},booktitle = {27th International Conference on Principles and Practice of ConstraintProgramming, {CP} 2021, Montpellier, France (Virtual Conference),October 25-29, 2021},series = {LIPIcs},volume = {210},pages = {20:1--20:19},publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},year = {2021},url = {https://doi.org/10.4230/LIPIcs.CP.2021.20},doi = {10.4230/LIPICS.CP.2021.20},timestamp = {Wed, 21 Aug 2024 22:46:00 +0200},biburl = {https://dblp.org/rec/conf/cp/CherifHT21.bib},bibsource = {dblp computer science bibliography, https://dblp.org} }

 

	Abstract Conflict Driven Clause Learning (CDCL) solvers are known to be efficient on structured instances and manage to solve ones with a large number of variables and clauses. An important component in such solvers is the branching heuristic which picks the next variable to branch on. In this paper, we evaluate different strategies which combine two state-of-the-art heuristics, namely the Variable State Independent Decaying Sum (VSIDS) and the Conflict History-Based (CHB) branching heuristic.   These strategies take advantage of the restart mechanism, which helps to deal with the heavy-tailed phenomena in SAT, to switch between these heuristics thus ensuring a better and more diverse exploration of the search space. 这些策略利用SAT中的重启机制，该机制有助于处理SAT中的重尾现象，从而在这些启发式方法之间进行切换，确保对搜索空间进行更全面且更多样化的探索。 Our experimental evaluation shows that combining VSIDS and CHB using restarts achieves competitive results and even significantly outperforms both heuristics for some chosen strategies. 我们的实验评估表明，结合VSIDS和CHB并使用重启机制能够取得具有竞争力的结果，甚至在某些选定策略中显著优于这两种启发式方法。
	备注：两类启发式最早来源文献： VSIDS --------------------------------------------------------------------------------- @inproceedings{DBLP:conf/dac/MoskewiczMZZM01,author = {Matthew W. Moskewicz andConor F. Madigan andYing Zhao andLintao Zhang andSharad Malik},title = {Chaff: Engineering an Efficient {SAT} Solver},booktitle = {Proceedings of the 38th Design Automation Conference, {DAC} 2001,Las Vegas, NV, USA, June 18-22, 2001},pages = {530--535},publisher = {{ACM}},year = {2001},url = {https://doi.org/10.1145/378239.379017},doi = {10.1145/378239.379017},timestamp = {Sat, 30 Sep 2023 09:38:31 +0200},biburl = {https://dblp.org/rec/conf/dac/MoskewiczMZZM01.bib},bibsource = {dblp computer science bibliography, https://dblp.org} }     CHB ------------------------------------------------------------------------------ @inproceedings{DBLP:conf/aaai/LiangGPC16,author = {Jia Hui Liang andVijay Ganesh andPascal Poupart andKrzysztof Czarnecki},editor = {Dale Schuurmans andMichael P. Wellman},title = {Exponential Recency Weighted Average Branching Heuristic for {SAT}Solvers},booktitle = {Proceedings of the Thirtieth {AAAI} Conference on Artificial Intelligence,February 12-17, 2016, Phoenix, Arizona, {USA}},pages = {3434--3440},publisher = {{AAAI} Press},year = {2016},url = {https://doi.org/10.1609/aaai.v30i1.10439},doi = {10.1609/AAAI.V30I1.10439},timestamp = {Mon, 01 Jul 2024 10:37:52 +0200},biburl = {https://dblp.org/rec/conf/aaai/LiangGPC16.bib},bibsource = {dblp computer science bibliography, https://dblp.org} }
	1 Introduction In recent years, combining VSIDS and CHB has shown promising results. For instance, the MapleCOMSPS solver, which won several medals in the 2016 and 2017 SAT competitions, switches from VSIDS to CHB after a set amount of time, or alternates between both heuristics by allocating the same duration of restarts to each one. 近年来，将VSIDS与CHB相结合已显示出良好的效果。例如，在2016年和2017年SAT竞赛中获得多项奖牌的MapleCOMSPS求解器，在经过一定时间后会从VSIDS切换到CHB，或者通过为每种启发式分配相同长度的重启时间来在两者之间交替使用。   备注1：此处介绍了最初较为简单的切换启发式的时机。   Yet, we still lack a thorough analysis on such strategies in the state of art as well as a comparison with new promising methods based on machine learning in the context of SAT solving. Indeed, recent research has also shown the relevance of machine learning in designing efficient search heuristics for SAT as well as for other decision problems. 然而，我们仍然缺乏对这类策略的彻底分析，以及在SAT求解背景下与基于机器学习的新有前景方法的比较。事实上，最近的研究也表明，机器学习在设计高效的SAT搜索启发式方法以及其他决策问题中具有相关性。   One of the main challenges is defining a heuristic which can have high performance on any considered instance.  主要挑战之一是定义一个启发式方法，使其在任何考虑的实例上都能表现出高性能。众所周知，一种启发式方法在一个实例族上可能表现非常出色，而在另一个实例族上却可能严重失效。   To this end, several reinforcement learning techniques can be used, specifically under the Multi-Armed Bandit (MAB) framework, to pick an adequate heuristic among CHB and VSIDS for each instance. 为此，可以使用几种强化学习技术，在多臂机（MAB）框架下，为每个实例在CHB和VSIDS之间选择一个合适的启发式方法。 These strategies also take advantage of the restart mechanism in modern CDCL algorithms to evaluate each heuristic and choose the best one accordingly. The evaluation is usually achieved by a reward function, which has to estimate the efficiency of a heuristic by relying on information acquired during the runs between restarts. In this paper, we want to compare these different strategies and, in particular, we want to know whether incorporating strategies which switch between VSIDS and CHB can achieve a better result than both heuristics and bring further gains to practical SAT solving. 这些策略还利用现代CDCL算法中的重启机制来评估每种启发式方法，并据此选择最佳的一种。评估通常通过奖励函数实现，该函数需要依靠重启之间运行过程中获取的信息来估计启发式方法的效率。在本文中，我们希望比较这些不同的策略，特别是想了解：采用在VSIDS和CHB之间切换的策略，是否能比这两种启发式方法都取得更好的效果，并为实际的SAT求解带来进一步的提升。   备注2：         此处介绍了本文核心MAB机制：利用重启之间运行过程中获取的信息，构建并使用奖励函数，来评估多种启发式策略的效率，在比较之后确定下一步的策略选择。         附带的也可以评估为什么早期简单粗暴的多策略切换会显现出一定的优势。