New Branching Heuristics for Incremental Bounded Model Checking
Satyam Shubham, Sutirtha Bhattacharyya, Ansuman Banerjee, Raj Kumar Gajavelly · 2025
Recent SAT solvers have shown a gigantic leap in the problem sizes they can handle, thereby benefiting Bounded Model Checking (BMC) at scale. Among the arsenal of branching heuristics that power modern day SAT solvers, one popular state-of-the-art heuristic is Variable State Independent Decaying Sum (VSIDS), which has significantly expedited the performance of SAT solvers on some problem instances. In this work, we develop two new modifications on VSIDS to expedite the performance of BMC. Our motivation stems from the fact that the CNF formulae arising from BMC unfolding are incremental in nature, and thereby, can benefit from variable activity and branching decisions of previous iterations. We propose a Reinforcement Learning (RL) based strategy to learn and selectively pass on variable activities across BMC iterations. Experiments on the HWMCC24 benchmarks show comparable or improved performance for around 65% of both SAT and UNDET instances.