Solving the Frobenius Problem in Z3: Exploring Quantifier Elimination
P. Anton (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
Quantified formulas over linear integer arithmetic (LIA) are common in formal verification, yet they present significant challenges for satisfiability modulo theories (SMT) solvers such as Z3. In this paper, we explore whether quantifier elimination can improve solver performance on the 2-coin Frobenius Coin Problem, a benchmark involving quantified LIA formulas with structural simplicity. While Z3's default strategy relies on solving satisfiability of a quantified formula directly, we evaluate an alternative tactic-based approach using the \texttt{qe\_rec} tactic to eliminate quantifiers first and produce a quantifier-free formula, which is then solved by the general purpose SMT solver. We conduct benchmarking across 54 satisfiable instances involving pairs of prime coin denominations. Our results indicate that quantifier elimination achieves better performance in both runtime and memory usage, solving more instances and offering consistent speed-ups of up to 10$\times$ compared to the default strategy.