A Survey of Satisfiability Modulo Theory <s> Quantifier Elimination by Projection <s> We propose a new quantifier elimination algorithm for the theory of linear real arithmetic. This algorithm uses as subroutine satisfiability modulo this theory, a problem for which there are several implementations available. The quantifier elimination algorithm presented in the paper is compared, on examples arising from program analysis problems, to several other implementations, all of which cannot solve some of the examples that our algorithm solves easily. <s> BIB001 </s> A Survey of Satisfiability Modulo Theory <s> Quantifier Elimination by Projection <s> We report on work in progress to generalize an algorithm recently introduced in [Monniaux, CAV 2010] 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 [Monniaux, CAV 2010], 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. <s> BIB002
In case a quantifier elimination, or projection, algorithm, is available for conjunctions of constraints, as happens with linear real arithmetic,  one can, given a formula ∃ y F ( x, y), find a conjunction C 1 ⇒ F , project C 1 over x as π(C 1 ), conjoin ¬π(C 1 ) to F and repeat the process (generating C 2 etc.) until the F becomes unsatisfiable BIB001 . i C i is then equivalent to ∃ y F . Again, this process may be made lazier, for nested quantification in particular  BIB002 .