SAT问题是一个经典的NP完全问题。许多其他领域的问题都可以转化为SAT问题，并利用SAT求解器进行求解。分支启发是现代SAT求解器的关键部分之一。一个优秀的分支启发算法可以加速学习子句的生成，提高现代SAT求解器的效率。分支启发关注的问题是搜索过程中如何选择下一个进行赋值的变量。作者将该问题类比于强化学习领域的多臂赌博机问题，将变量赋值期间对生成学习子句的贡献率类比于多臂赌博机的收益。作者使用指数移动平均计算期望收益，同时结合步长和权重衰减技巧提高搜索的局部性，加入原因侧补偿项提高收益的完整性，最终提出学习率分支(LRB)启发算法。该算法相较于被广泛应用的经典分支启发算法VSIDS，具有显著的性能提升，而且计算开销较小，可以应用于后续的SAT求解器。
截至2023年SAT竞赛中优秀求解器的简图（不完整）。并行以Painless框架为代表，介绍了PRS求解器的改进，分布式以Mallob框架为代表，介绍了改进。
SAT问题是一个经典的NP完全问题。许多其他领域的问题都可以转化为SAT问题，并利用SAT求解器进行求解。搜索重启是现代SAT求解器的关键部分之一。一个优秀的重启策略可以提高现代SAT求解器的效率。作者将现代SAT求解器看作“子句生成器”，并使用文字块距离(LBD)对子句质量进行衡量。作者使用全局平均和局部平均的LBD作为动态评估子句质量的方法，并根据两者之间的差距，判断是否进行重启。针对该重启策略的实验表明：该重启策略能显著提高SAT问题中不可满足实例的判定效率，但对可满足实例没有显著的效率提升。作者又提出，当本次搜索中已赋值的变量数量显著多于之前搜索的平均数量时，对重启操作进行阻塞，可以帮助可满足实例的判定。我认为本文提出的重启策略和阻塞策略想法简明、实现有效，有助于后续SAT求解器的设计。