“Per-Instance Subproblem Generation for Strategy Selection in SMT” by Amalee Wilson, Nina Narodytska, Clark Barrett, and Haoze Wu. In Proceedings of the 25^th International Conference on Formal Methods In Computer-Aided Design (FMCAD '25), (Ahmed Irfan and Daniela Kaufmann, eds.), Oct. 2025, pp. 94-103. Menlo Park, CA, USA.
In this paper, we investigate customizing the solving strategy for an individual SMT problem, based solely on the problem itself, without relying on any offline strategy tuning. Our key insight is to generate a set of subproblems derived from the original formula, analyze the behavior of candidate solving strategies on these smaller, representative subproblems, and predict which strategy will perform best on the original formula. We demonstrate that performance on the subproblems is frequently indicative of performance on the original formula. Additionally, we introduce a novel subproblem generation procedure that outperforms existing SMT formula partitioning techniques for the proposed workflow. Finally, we show that on a selection of SMT-LIB benchmarks, when our approach can make a prediction, it can reduce the total compute time substantially.
BibTeX entry:
@inproceedings{WNB+25,
author = {Amalee Wilson and Nina Narodytska and Clark Barrett and Haoze Wu},
editor = {Ahmed Irfan and Daniela Kaufmann},
title = {Per-Instance Subproblem Generation for Strategy Selection in SMT},
booktitle = {Proceedings of the {\it 25^{th}} International Conference
on Formal Methods In Computer-Aided Design (FMCAD '25)},
pages = {94--103},
publisher = {TU Wien Academic Press},
month = oct,
year = {2025},
doi = {10.34727/2025/isbn.978-3-85448-084-6_15},
note = {Menlo Park, CA, USA},
url = {https://repositum.tuwien.at/handle/20.500.12708/219543}
}
(This webpage was created with bibtex2web.)