Efficient subformula orders for real quantifier elimination of non-prenex formulas

Abstract

In this paper we study speeding up real quantifier elimination (QE) methods for non-prenex formulas. Our basic strategy is to solve non-prenex first-order formulas by performing QE for subformulas constituting the input non-prenex formula. We propose two types of methods (heuristic methods/machine learning based methods) to determine an appropriate ordering of QE computation for the subformulas. Then we empirically examine their effectiveness through experimental results over more than 2,000 non-trivial example problems. Our experiment results suggest machine learning can save much effort spent to design effective heuristics by trials and errors without losing efficiency of QE computation.