We present Self-Driven Strategy Learning ($\textit{sdsl}$), a lightweight online learning methodology for automated reasoning tasks that involve solving a set of related problems. $\textit{sdsl}$ does not require offline training, but instead automatically constructs a dataset while solving earlier problems. It fits a machine learning model to this data which is then used to adjust the solving strategy for later problems. We formally define the approach as a set of abstract transition rules. We describe a concrete instance of the sdsl calculus which uses conditional sampling for generating data and random forests as the underlying machine learning model. We implement the approach on top of the Kissat solver and show that the combination of Kissat+$\textit{sdsl}$ certifies larger bounds and finds more counter-examples than other state-of-the-art bounded model checking approaches on benchmarks obtained from the latest Hardware Model Checking Competition.

翻译：我们提出了一种自我驱动的策略学习（Self-Driven Strategy Learning，简称sdsl）方法，这是一种针对涉及解决一组相关问题的自动推理任务的轻量级在线学习技术。sdsl无需离线训练，而是在解决早期问题时自动构建数据集，并利用该数据拟合机器学习模型，从而调整后续问题的求解策略。我们以一组抽象转换规则的形式正式定义了该方法。我们描述了sdsl演算的一个具体实例，该实例采用条件采样生成数据，并使用随机森林作为底层机器学习模型。我们将该方法实现于Kissat求解器之上，并证明在来自最新硬件模型检验竞赛的基准测试中，相比于其他最先进的界限模型检验方法，Kissat+sdsl能够认证更大的边界并发现更多的反例。