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.

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