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