We report on work in progress to generalize an algorithm recently introduced in  for checking satisfiability 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 eliminating or partially eliminating quantifiers. We also apply the algorithm for Presburger Arithmetic formulas and evaluate it on formulas from a model checker for Duration Calculus . We report on experiments on different variants of the auxiliary procedures. So far, there is an edge to applying SMT-TEST proposed in , while we found that a simpler approach which just eliminates quantified variables per round is almost as good. Both approaches offer drastic improvements to applying default quantifier elimination.
Main Research Area:
10th International Workshop on Satisfiability Modulo Theories (SMT 2012)