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.