Lightweight Online Learning for Sets of Related Problems in Automated Reasoning
This work addresses efficiency improvements for automated reasoning in hardware model checking, though it is incremental as it builds on existing solvers like Kissat.
The paper tackles the challenge of solving sets of related automated reasoning problems by introducing Self-Driven Strategy Learning (sdsl), a lightweight online learning method that constructs a dataset during problem-solving and uses it to adjust strategies, resulting in certifying larger bounds and finding more counter-examples than state-of-the-art approaches on hardware model checking benchmarks.
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.