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.
|Number of pages||10|
|Publication status||Published - 2012|
|Event||10th International Workshop on Satisfiability Modulo Theories (SMT 2012) - Manchester, United Kingdom|
Duration: 30 Jun 2012 → 1 Jul 2012
|Workshop||10th International Workshop on Satisfiability Modulo Theories (SMT 2012)|
|Period||30/06/2012 → 01/07/2012|