Parallel SMT Solving via Iterative Tree Partitioning

TitleParallel SMT Solving via Iterative Tree Partitioning
Publication TypeConference Paper
Year of Publication2026
AuthorsKolárik, Tomáš, Hyvärinen Antti E. J., Asadzadeh Seyedmasoud, and Sharygina Natasha
Conference NameTACAS 2026
Abstract

We present a novel algorithm for parallel solving of SMT
problems based on a partitioning process that divides the original problem into a tree structure in an iterative way. By enabling node revisiting, the new method addresses the problem of partitioning divergence found in prior approaches that frequently leads to longer runtimes compared to sequential results. The resulting algorithm is highly flexible, offers a combination of partitioning, portfolio solving, and clause sharing, allows the use of various partitioning functions, and scales gracefully with the available resources. We implemented the new approach in the tool SMTS on top of the efficient sequential SMT solver OpenSMT. Our experimental results demonstrate a substantial improvement over OpenSMT in logics QF LRA and QF LIA even when the partitioning approach utilizes just a single solver. Notably, SMTS has consistently dominated several divisions of the annual competition of parallel SMT solvers.