# Lightweight Online Learning for Sets of Related Problems in Automated Reasoning

arXiv: https://arxiv.org/abs/2305.11087 · HTML: https://mlsanity.com/paper/2305.11087/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- Builds on 12 of its 62 references that are in the map.
- First posted on arXiv 18 May 2023.

## Builds on (most cited first, 12 of 12)

- [Solving Mixed Integer Programs Using Neural Networks](https://mlsanity.com/paper/2012.13349/) (2020)
- [Neuro-Symbolic Program Synthesis](https://mlsanity.com/paper/1611.01855/) (2016)
- [Guiding High-Performance SAT Solvers with Unsat-Core Predictions](https://mlsanity.com/paper/1903.04671/) (2019)
- [Understanding Random Forests: From Theory to Practice](https://mlsanity.com/paper/1407.7502/) (2014)
- [Teaching Temporal Logics to Neural Networks](https://mlsanity.com/paper/2003.04218/) (2020)
- [The Voice of Optimization](https://mlsanity.com/paper/1812.09991/) (2018)
- [G2SAT: Learning to Generate SAT Formulas](https://mlsanity.com/paper/1910.13445/) (2019)
- [Manthan: A Data Driven Approach for Boolean Function Synthesis](https://mlsanity.com/paper/2005.06922/) (2020)
- [A Novel Automated Curriculum Strategy to Solve Hard Sokoban Planning Instances](https://mlsanity.com/paper/2110.00898/) (2021)
- [Improve SAT-solving with Machine Learning](https://mlsanity.com/paper/1710.11204/) (2017)
- [Engineering an Efficient Boolean Functional Synthesis Engine](https://mlsanity.com/paper/2108.05717/) (2021)
- [Understanding VSIDS Branching Heuristics in Conflict-Driven Clause-Learning SAT Solvers](https://mlsanity.com/paper/1506.08905/) (2015)

## Built on by (most cited first, 2 of 2)

- [Mini-Batch Robustness Verification of Deep Neural Networks](https://mlsanity.com/paper/2508.15454/) (2025)
- [The Luna Bound Propagator for Formal Analysis of Neural Networks](https://mlsanity.com/paper/2603.23878/) (2026)

## Abstract (arXiv)

We present Self-Driven Strategy Learning (textitsdsl), a lightweight online learning methodology for automated reasoning tasks that involve solving a set of related problems. textitsdsl 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+textitsdsl 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.