We report on work in progress to generalize an algorithm recently introduced in [10] for checkingsatisfiability of formulas with quantifier alternation. The algorithm uses two auxiliary procedures:a procedure for producing a candidate formula for quantifier elimination and a procedure for eliminatingor partially eliminating quantifiers. We also apply the algorithm for Presburger Arithmeticformulas and evaluate it on formulas from a model checker for Duration Calculus [8]. We report onexperiments on different variants of the auxiliary procedures. So far, there is an edge to applyingSMT-TEST proposed in [10], while we found that a simpler approach which just eliminates quantifiedvariables per round is almost as good. Both approaches offer drastic improvements to applyingdefault quantifier elimination.
The complexity of presburger arithmetic with bounded quantifier alternation depth