Quantifier elimination for linear real arithmetic (LRA) is the problem of taking in a formula with quantifiers and producing a logically equivalent formula without quantifiers.

# Linear Real Arithmetic (LRA)

LRA includes all first order formulas whose atomic formulas consist of a linear expression and comparator. For example:

is a formula in linear real arithmetic, as is:

A formula like:

is not in LRA because the term is raised to the power of 2.

# Example

Lets eliminate the quantifier from:

Readers who are good at algebra can probably solve this problem in their heads, but to get a sense of what an algorithm for quantifier elimination over LRE would look like lets go through it in detail.

There are two linear expressions of interest:

A plot of these looks like so:

The function is negative at every point from to , is zero at and is positive at every point after .

The function is positive from to , is zero at and is negative at every point after that.

We can express this compactly in a table (called a sign table) like so:

To satisfy our original formula we need a value of where is zero and is positive. We can check if such a value exists by scanning each row of the table and checking if the column for is and the column for is . Row two, corresponding to the point satisfies this condition, so the formula is the quantifier free equivalent of the original formula.

Notice that because we know that both functions involved are lines, and because we know each line's slope the structure of the sign table is completely determined by the *ordering *of the roots of each line.

This example had only one variable, so it was possible to solve each linear equation explicitly for its root, and then use the values of the roots to determine the layout of the sign table, but nothing in our analysis changes if we replace the numerical values of the roots with symbols like and , compute the order in which the roots occur, and then use the ordering of the roots to compute the sign table.

The catch for more complex formulas is that when a problem contains more than one variable there isn't any one correct ordering of the equation's roots since the ordering of the roots depends on the values of the variables.

The solution to this problem is to compute every possible ordering of the roots and compute a sign table for each ordering. We will see how this works in the next example.

# Example with Multiple Variables

Lets eliminate the quantifier from:

This formula contains 2 linear expressions:

Since we are eliminating the quantified variable from our formula lets think of these as linear expressions in :

The first of these expressions is zero when:

And the second has a root when:

For brevity lets write:

Depending on the value of there are 3 possible orderings for these roots:

For each of these three possibilities we can construct a sign table that will break up the axis into intervals along which both of our expressions have constant signs.

For the sign table looks like:

The sign table has 5 intervals. is linear in x, has a slope of 3 in and has a root at , so it is zero at , negative at all points before and positive after . For the table is similar.

For the sign table looks like:

Notice that because we do not need separate intervals for each of them like we did in the case where .

Finally the sign table for is:

Note that given one of our 3 root order constraints we can decide if the original formula is true by table lookup. The problem is solvable if and only if and so it has a solution only if the sign table has a row where the sign of is negative and the sign of is positive or zero.

By inspection we can see that this is only true when , so the only way there is an such that our formula is satisified is if:

which can be simplified to the condition:

simplifying further:

Notice that this last expression is an expression in LRA! In fact all three of our possible root orderings can be written as formulas in linear real arithmetic.

The other crucial point is that since the real numbers are a totally ordered field one of the three orderings must be true, so we can write:

is equivalent to:

Which is equivalent to:

Now for brevity lets write:

So we have:

Now we can distribute F over the disjunction to get:

Then we can distribute the existential quantifier over each formula:

And since does not appear in any of the root order conditions this is just:

But since each of the expressions for and are just logical encodings of the possible root orders, and each root order implies a sign table that we can use to decide whether there is any such that is we can just solve F in each clause of the disjunction via the sign table.

As we already saw in the discussion of sign tables the only root ordering where there is an that makes is the condition , so our formula becomes:

Which simplifies to:

And we have eliminated the quantifier and all occurences of !

**Outline of the Algorithm**

Suppose we have a quantifier free formula (QFF) in linear real arithmetic with variables .

The idea of the algorithm is to distribute over a disjunction of every possible root ordering. Then find the truth value of under that ordering. For brevity we will write as

Since the real line is totally ordered one of the possible orders of roots must be true. Suppose is the set of all possible orders, then we can write the formula as:

Distributing F we get:

Distributing the existential quantifier we get:

Now in each conjunction the root ordering holds, so we can evaluate to True or False using the root ordering:

Now the only formulas that appear are the root orderings, , which depend only on and the terms each of which is either or , so we are done.

To shorten the formula we can drop any of the formulas in the disjunction where .

# Evaluating a Formula Given a Root Ordering

One detail we glossed over is how to use the sign table to evaluate . In both of our examples we could just look at the sign tables and check, but for a computer to do this task we need a more precise procedure.

The idea is to use a recursive algorithm to walk down the formula collecting all intervals in the sign table that satisfy the conditions of the formula. If there is at least one satisfying interval then the formula evaluates to true given the root ordering.

The recursive procedure is as follows:

Where returns the set of all rows of the sign table where linear polynomial has one of the signs in the list .

# Complexity and Better Alternatives

The complexity of this algorithm is horrifyingly bad. We have to enumerate all possible orderings of roots to eliminate one quantifier so for a formula containing expressions it is approximately for a single quantifier.

Much faster algorithms exist. An early algorithm called the Ferrante-Rakoff method can eliminate all quantifiers from a formula with quantifiers in where is a positive constant.

Later Loos and Weispfenning invented an improved method with a smaller constant . That method is implemented in the computer algebra package redlog.