A Fast Linear-Arithmetic Solver: How can Gaussian elimination be used to simplify matrix A?

Question

I am working on an LRA Theory solver for SymPy, an open source python library for symbolic computations. You can find my work here. Currently I'm trying to optimize it to run faster.

My implementation is based off of Bruno Dutertre's and Leonardo de Moura's paper "A Fast Linear-Arithmetic Solver for DPLL(T)". My question regards a particular paragraph from the paper about a way to speed things up:

Since the elementary atoms of Φ′ are known in advance, we can immediately simplify the constraints Ax = 0 by removing any variable xi that does not occur in any elementary atom of Φ′. This is done by Gaussian elimination. In practice, this presimplification can reduce the matrix size significantly.

Φ′ is the second part of the boolean formula above—that is the bottom formula which includes only inequalities. The top formula which is a conjunction of equalities is represented by the matrix A. The matrix for this particular example would look something like this (or at least this is how it's represented in my implementation):

The first row with variables is just to show which column corresponds to which variable. It's not actually part of the matrix.

I'm confused about how to reduce the size of this matrix. In this particular example, it seems like the column with z can be removed while maintaining equisatisfiability. I think you can also get rid of y. However, I can come up with examples where variables can't be removed despite not appearing in Φ′, so you can't simply just always get rid of such variables. Presumably Gaussian elimination has to be involved somehow.

Answer 1

The idea here is that if you have a solution for $x$, $s_1$, and $s_2$, then from this you can find $y$ and $z$.

The way you can solve this is to solve the linear system:

$$\begin{eqnarray*} y + 0z & = & s_1 - x\\ 2y - z & = & s_2 - x\end{eqnarray*}$$

Which has the solution:

$$\begin{eqnarray*} y & = & s_1 - x \\ z & = & 2s_1 - s_2 - x\end{eqnarray*}$$

What I think the paper is getting at is that you can use Gaussian elimination directly on the tableau that you have constructed. Consider this form of the linear system, with the variables to be eliminated moved to the left:

$$\left[\begin{matrix}1 & 0 & 1 & -1 & 0 \\ 2 & -1 & 1 & 0 & -1\end{matrix}\right] \left[\begin{matrix}y \\ z \\ x \\ s_1 \\ s_2\end{matrix}\right] = \left[ \begin{matrix}0 \\ 0\end{matrix} \right] $$

Turn this into an equivalent system where the leftmost 2 by 2 submatrix is the identity:

$$\left[\begin{matrix}1 & 0 & 1 & -1 & 0 \\ 0 & 1 & 1 & -2 & 1\end{matrix}\right] \left[\begin{matrix}y \\ z \\ x \\ s_1 \\ s_2\end{matrix}\right] = \left[ \begin{matrix}0 \\ 0\end{matrix} \right] $$

And that gives you equations for $y$ and $z$:

$$\left[\begin{matrix}1 & 0 \\ 0 & 1 \end{matrix}\right] \left[\begin{matrix}y \\ z\end{matrix}\right] = - \left[\begin{matrix}1 & -1 & 0 \\ 1 & -2 & 1\end{matrix}\right] \left[\begin{matrix}x \\ s_1 \\ s_2\end{matrix}\right] $$