Quantified Formulas¶
So far we have concentrated on quantifier-free satisfiability. But how about quantifiers? They can be used to express, e.g., verification conditions such as \A{x_1}{\ElemSort}{\A{x_2}{\ElemSort}{\A{x_3}{\ElemSort}{\SubType(x_1,x_2)\land\SubType(x_2,x_3)\Implies\SubType(x_1,x_3)}}} Handling quantifiers in SMT is a long-standing challenge and an ongoing research topic. Some SMT solvers have (possibly incomplete) algorithms for handling quantifiers.
Quantifier elimination¶
Some theories allow us to get rid of the quantifiers, meaning that we can get an equivalent formula that has no quantifiers. Formally, a \Sig -theory \Th admits quantifier elimination if there is an algorithm that, given a \Sig -formula F , returns a quantifier-free \Sig -formula G that is \Th -equivalent to F (meaning that each interpretation \Interp is a \Th -model of F iff it is a \Th -model of G ).
Example
The theory of linear arithmetic over reals, \TLRA , admits quantifier elimination.
Eliminating y from \begin{array}{rl}\A{x}{\RealsSort}{\E{y}{\RealsSort}{}}&({x-y \ge 1}\land{-x-2y \le -1}\land{-2x-y\ge-8}) \lor\\\\& ({x-y \le 2}\land{-x-2y \ge 1})\end{array} we get \A{x}{\RealsSort}{({1 \le x}\land{x \le 5}) \lor (x \le 1)} and then \False after eliminating x .
The figure below shows the inequalities as lines and the areas described by the first conjunction in blue and the second one in green. Elimination of y results on the projection of these areas on the x-axis.

Some theories do not admit quantifier elimination but small extensions do:
Example
The theory of linear arithmetic over integers \TLIA does not admit quantifier elimination. For instance, the formula \E{x}{\IntsSort}{2x=y} does not have a \TLIA -equivalent quantifier-free formula.
If we augment the theory \TLIA with the divisibility predicate \Div{d}{n} evaluating to true whenever n is divisible by d , the resulting theory admits quantifier elimination. As an example, a quantifier-free version of \E{x}{\IntsSort}{2x=y} is \Div{2}{y} .
For further discussion, see Section 7.1 in Aaron Bradley and Zohar Manna: The Calculus of Computation, Springer, 2007
Fourier-Motzkin elimination¶
The Fourier–Motzkin elimination method is a quantifier elimination method for linear arithmetic over reals. It is conceptually rather simple but may require lots of memory in practise. The idea is to eliminate quantifiers one-by-one, starting from the innermost quantifier. It only works for conjunctions of atoms and, therefore, the formula must be translated into DNF. Furthermore, it can only eliminate existential quantifiers but universal quantifiers can be handled by using the equivalence {\forall x: \phi} \Equiv {\neg \exists x: \neg \phi} to eliminate \forall x: \phi as follows:
negate the formula \phi and translate the result to DNF,
apply the Fourier-Motzkin method to each disjunct, and
negate the disjunction of the results.
Eliminating an existentially quantified variable can be done as follows. For simplicity, we only consider inequalities \le and \ge . Assume a conjunction \FM of linear inequalities over n variables x_1,…,x_n and a variable to be eliminated, say x_1 . The inequalities in \FM can be rewritten into \FMup \land \FMlo \land \FMindep, where
\FMlo contains the \Nlo inequalities of the form b_l + \sum_{j=2}^{n} a_{j,l} x_j \le x_1 in \FM . For each 1 \le l \le \Nlo , let \Rlo{l}(x_2,…,x_n) = b_l + \sum_{j=2}^{n} a_{j,l} x_j .
\FMup contains the \Nup inequalities of the form x_1 \le b_k + \sum_{j=2}^{n} a_{j,k} x_j in \FM . For each 1 \le k \le \Nup , let with \Rup{k}(x_2,…,x_n) = b_k + \sum_{j=2}^{n} a_{j,k} x_j .
\FMindep is the conjunction of the inequalities in \FM that do not involve x_1 .
The conjunction \FMup \land \FMlo \land \FMindep is satisfiable if and only if there exists a real-valued assignment on \Set{x_2,…,x_n} that
evaluates \FMindep to true and
there is a value on x_1 so that \Rlo{l}(x_2,…,x_n) \le x \le \Rup{k}(x_2,…,x_n) holds each 1 \le l \le \Nlo and 1 \le k \le \Nup
Thus \FMup \land \FMlo \land \FMindep over the variables x_1,…,x_n is satisfiable if and only if \FMindep \land \bigwedge_{1 \le l \le \Nlo, 1 \le k \le \Nup}{\Rlo{l}(x_2,…,x_n) \le \Rup{k}(x_2,…,x_n)} over the variables x_2,…,x_n is satisfiable. The method above is easy to generalize for strict inequalities as well. The elimination method has double-exponential worst-case complexity when eliminating all the variables in a formula.
Example
Consider the formula (x-y \ge 1)\land(-x-2y \le -1)\land(-2x-y\ge-8) and eliminate y . Now
\FMlo \Def (-0.5x+0.5 \le y) ,
\FMup \Def (y \le x-1) \land (y \le -2x+8) and
\FMindep \Def \True
Thus the resulting formula is (-0.5x+0.5 \le x-1) \land (-0.5x+0.5 \le -2x+8) \land \True that, when simplified, is equivalent to (x \ge 1) \land (x \le 5)
Example
Consider the quantified linear arithmetic over reals formula \begin{array}{rl}\A{x}{\RealsSort}{\E{y}{\RealsSort}{}}&({x-y \ge 1}\land{-x-2y \le -1}\land{-2x-y\ge-8}) \lor\\\\& ({x-y \le 2}\land{-x-2y \ge 1})\end{array} The formula is already in DNF. Eliminating y from the formula, we get \A{x}{\RealsSort}{({1 \le x}\land{x \le 5}) \lor (x \le 1)}
Negating, we get {({1 > x}\lor{x > 5}) \land (x > 1)} , which is ({1 > x} \land {x > 1}) \lor ({x > 5} \land {x > 1}) in DNF.
Simplifying, we get {x > 5} .
Eliminating x we get \E{x}{\RealsSort}{x > 5} = \True and thus \A{x}{\RealsSort}{({1 \le x}\land{x \le 5}) \lor (x \le 1)} = \neg\True = \False .
Other approaches¶
Solving quantified formulas in the SMT context is an ongoing research topic. One approach used in some current solvers is “quantifier instantiation”
Yeting Ge and Leonardo de Moura: Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories, Proc. CAV 2009, pp 306–320
Yeting Ge, Clark Barrett, and Cesare Tinelli: Solving quantified verification conditions using satisfiability modulo theories, Ann. Math. Artif. Intel. 55:101–122, 2009
and also search-based methods start to appear
Nikolaj Bjørner and Mikolas Janota: Playing with Quantified Satisfaction, Proc. LPAR 2015, pp 15–27