摘 要：冲突驱动子句学习（conflict-driven clause learning，CDCL）是现代SAT求解器的主流框架，而基于变量活性的分支算法是其高效求解的关键因素之一。将全局学习率（global learning rate，GLR）和变量决策层结合（试读）...