1
$\begingroup$

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.

example from paper

Φ′ 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):

matrix A

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.

$\endgroup$
1
  • $\begingroup$ By the equalities, there is a linear dependency between $x,y,z,s_1$ and $s_2$. You can indeed express $y$ and $z$ as functions of $x, s_1$ and $s_2$ by elimination. $y=s_1-x, z=2s_1-s_2-x$. $\endgroup$
    – user16034
    Commented Aug 21, 2023 at 11:53

1 Answer 1

0
$\begingroup$

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] $$

$\endgroup$
5
  • 1
    $\begingroup$ More precisely, you can eliminate (some of) the variables that do not appear in the inequalities, using the equalities. $\endgroup$
    – user16034
    Commented Aug 21, 2023 at 13:37
  • $\begingroup$ If you use the equations you get for y and z and try to eliminate them from the matrix you end up getting rid of the other variables. For example, if you substitute $z = -x -2s_1 - s_2$ into $s_2 = x + 2y - z$ you get an equation with $s_2$ on both sides which removes $s_2$ and $s_2$ shouldn't be removed. $\endgroup$
    – Tilo RC
    Commented Aug 23, 2023 at 18:25
  • $\begingroup$ @TiloRC The idea behind this step is that $y$ and $z$ do not participate in the inequality constraints. To solve those inequality constraints (e.g. using the simplex method), you don't need to eliminate those variables, you can just ignore them. Once you have the possible values for $x$, $s_1$, and $s_2$, you then need to compute $y$ and $z$, and that's where this set of equations comes in. $\endgroup$
    – Pseudonym
    Commented Aug 24, 2023 at 0:11
  • $\begingroup$ @Pseudonym Perhaps that is what the paper meant by gaussian elimination. I'm still not sure when you're allowed to remove variables though. Suppose you want to check if the following is satisfiable: $x\ge0 \land x+y\le2 \land x+2*y-z\ge6$. In this situation you definitely can't get rid of z because if you do the problem goes from sat to unsat. This desmos graph demonstrates that because you can adjust the slide for z so that the problem because satisfiable: desmos.com/calculator/mphisnkfx5. $\endgroup$
    – Tilo RC
    Commented Aug 24, 2023 at 1:00
  • $\begingroup$ @TiloRC leodemoura.github.io/files/cav06.pdf $\endgroup$
    – Pseudonym
    Commented Aug 24, 2023 at 2:02

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.