@conference {416,
	title = {Parallel SMT Solving via Iterative Tree Partitioning},
	booktitle = {TACAS 2026},
	year = {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.},
	author = {Tom{\'a}{\v s} Kol{\'a}rik and Antti E. J. Hyv{\"a}rinen and Seyedmasoud Asadzadeh and Natasha Sharygina}
}
