Playing with Quantified Satisfaction
Nikolaj Bjørner, Mikoláš Janota · EPiC series in computing · 2018
We develop an algorithm for satisfiability of quantified formulas. The algorithm is based on recent progress in solving Quantified Boolean Formulas, but it generalizes beyond propositional logic to theories, such as linear arithmetic over integers (Presburger arithmetic), linear arithmetic over reals, algebraic data-types and arrays. Compared with previous algorithms for satisfiability of quantified arithmetical formulas our new implementation outperforms previous implementations in Z3 by a significant margin.