A Survey of Satisfiability Modulo Theory <s> 11 <s> This paper develops abstract quantifier elimination procedures for linear arithmetic over the reals and integers. They are formulated as theory solvers in the context of an abstract DPLL-based search. The resulting procedures allow the solvers to maintain integral control of the search process. We also evaluate this procedure and compare it with several alternatives. So far, the evaluation indicates that the proposed approach has some compelling advantages. <s> BIB001 </s> A Survey of Satisfiability Modulo Theory <s> 11 <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 these eager approaches, the size of the substitution set may grow quickly (especially for linear integer arithmetic, which may involve enumerating all cases up to the least common multiple of the divisibility constants). For this reason, lazy approaches were proposed where the substitutions are generated from counterexamples, in much the same way that learned lemmas are generated in DPLL(T) BIB001 BIB002 . For a formula A( x) ∧ ∀y B( x, y), the system first solves A( x) for a solution x 0 , then checks whether there exists y such that ¬B( x 0 , y); if so, such an y 0 is generalized into one of the possible substitutions S 1 ( x) and the system restarts by solving A( x) ∧ B( x, S 1 ( x). The process iterates until a solution is found or the substitutions accumulated block all solutions for x; termination is ensured because the set of possible symbolic substitutions is finite. Note that a full quantifier elimination is not necessary to produce a solution.