Evaluating Z3's Performance on Real Number Constraints
Empirical Strategies for Tactic Selection and Parallelization
D.G. Delov (TU Delft - Electrical Engineering, Mathematics and Computer Science)
D.G. Sprokholt – Mentor (TU Delft - Programming Languages)
S.S. Chakraborty – Mentor (TU Delft - Programming Languages)
A.E. Zaidman – Graduation committee member (TU Delft - Software Technology)
More Info
expand_more
Other than for strictly personal use, it is not permitted to download, forward or distribute the text or part of it, without the consent of the author(s) and/or copyright holder(s), unless the work is under an open content license such as Creative Commons.
Abstract
Z3 is a widely used SMT solver with support for linear and non-linear arithmetic. While powerful, its performance is dependent on tactics -- user-defined strategies that guide the solving process. This paper systematically analyzes the performance of Z3 across various tactic sequences, including ones with parallelization, on benchmarks from SMT-LIB. The results reveal that certain problems can get a speed-up of up to 5 times with the appropriate strategy, however different approaches come with certain limitations. We explore a pattern in linear problems where parallelization and heavy preprocessing make a big difference to performance. Additionally, we discuss two non-linear benchmarks for which it is very evident that the right approach to tactic selection matters and there is no single optimal strategy in SMT solving. These are all important observations since SMT solvers are a key part of many industrial processes where speed and accuracy are crucial.