QF_LRA

Problem formulation

A formula in Quantifier-Free Linear Real Arithmetic (QF_LRA) is a boolean combination of atoms in the form

$$\sum_{i=1}^n a_i x_i \bowtie b$$

where $a_i, b \in \R$, $x_i$ are variables, and $\bowtie \in \{<, \leq, =, \neq, >, \geq\}$ is a comparison operator.

When dealing with a conjunction of such atoms, we can represent the problem as a system of linear inequalities:

$$\begin{bmatrix} a_{11} & a_{12} & \cdots & a_{1n} \\ a_{21} & a_{22} & \cdots & a_{2n} \\ \vdots & \vdots & \ddots & \vdots \\ a_{m1} & a_{m2} & \cdots & a_{mn} \\ \end{bmatrix} \begin{bmatrix} x_1 \\ x_2 \\ \vdots \\ x_n \\ \end{bmatrix} \bowtie \begin{bmatrix}b_1 \\ b_2 \\ \vdots \\ b_m \\ \end{bmatrix}$$

Moreover, there are usually bounds on the variables, which can be represented as

$$\begin{bmatrix} l_1 \\ l_2 \\ \vdots \\ l_n \\ \end{bmatrix} \leq \begin{bmatrix} x_1 \\ x_2 \\ \vdots \\ x_n \\ \end{bmatrix} \leq \begin{bmatrix} u_1 \\ u_2 \\ \vdots \\ u_n \\ \end{bmatrix}$$

Tableau formulation

We introduce a new vector of variables $s$, where each entry $s_i$ corresponds to the slack variable for the $i$-th inequality, i.e., $s_i = \sum_{j=1}^n a_{ij} x_j$.

$$\begin{bmatrix} a_{11} & a_{12} & \cdots & a_{1n} & -1 & 0 & \cdots & 0 \\ a_{21} & a_{22} & \cdots & a_{2n} & 0 & -1 & \cdots & 0 \\ \vdots & \vdots & \ddots & \vdots & \vdots & \vdots & \ddots & \vdots \\ a_{m1} & a_{m2} & \cdots & a_{mn} & 0 & 0 & \cdots & -1 \\ \end{bmatrix} \begin{bmatrix} x_1 \\ x_2 \\ \vdots \\ x_n \\ s_1 \\ s_2 \\ \vdots \\ s_m \\ \end{bmatrix} = \begin{bmatrix} 0 \\ 0 \\ \vdots \\ 0 \\ \end{bmatrix}$$

to which we have to add the bounds on the variables:

$$\begin{bmatrix} l_1 \\ l_2 \\ \vdots \\ l_n \\ b_1^l \\ b_2^l \\ \vdots \\ b_m^l \\ \end{bmatrix} \leq \begin{bmatrix} x_1 \\ x_2 \\ \vdots \\ x_n \\ s_1 \\ s_2 \\ \vdots \\ s_m \\ \end{bmatrix} \leq \begin{bmatrix} u_1 \\ u_2 \\ \vdots \\ u_n \\ b_1^u \\ b_2^u \\ \vdots \\ b_m^u \\ \end{bmatrix}$$

where the new bounds for the slack variables are defined as

$$b_i^l = \begin{cases} b_i & \text{if $\bowtie_i \in \{=, \geq, >\}$} \\ -\infty & \text{otherwise} \ \end{cases} \quad b_i^u = \begin{cases} b_i & \text{if $\bowtie_i \in \{=, \leq, <\}$} \\ +\infty & \text{otherwise} \end{cases} \quad$$

which simply ensures that the original inequalities are satisfied by the slack variables. Given $\bar{x} = \begin{bmatrix} x & s \end{bmatrix}^T$, we can rewrite the problem as

$$\begin{bmatrix}A & -I \\ \end{bmatrix}\bar{x} = \begin{bmatrix}0 \\ \end{bmatrix} \quad \text{with} \quad \begin{bmatrix}l \\ b^l \\ \end{bmatrix} \leq \bar{x} \leq \begin{bmatrix}u \\ b^u \\ \end{bmatrix}$$

Pivoting and updating

We can divide the variables into two sets: basic variables and non-basic variables. We will always enforce the following rules:

• basic variables are expressed in terms of non-basic variables
• the value of non-basic variables is always set to one of their bounds

Based on these rules, every time the value of a non-basic variable changes, which happens every time we enforce a stricter bound on the variable that forces us to update the latest assignment, we need update the values of the basic variables accordingly.

If we notice that a basic variable, has been assigned a value that violates its bounds, we may also want to switch its status with a non-basic variable. This operation is called pivoting. For it to be useful in the first place, we need to find a non-basic variable that, when its value is changed, allows us to satisfy the violated bound of the basic variable.

If we find such a variable, we can perform a pivoting operation to switch the status of $\bar{x}_i$ and $\bar{x}_j$, making $\bar{x}_j$ a basic variable and $\bar{x}_i$ a non-basic variable. If this violates some other bounds, we can repeat the process until we find an assignment that satisfies all bounds, or we end up in a situation where no pivoting operation is possible. If the latter happens, it means that the original problem is unsatisfiable, and we must return an explanation to the SAT solver.

Solving QF_LRA

Tableau pivoting

We start by assigning the value of $0$ to all variables and construct the tableau as described in the previous section, but ignoring the bounds for the moment.

$$\begin{bmatrix} a_{11} & a_{12} & \cdots & a_{1n} & -1 & 0 & \cdots & 0 \\ a_{21} & a_{22} & \cdots & a_{2n} & 0 & -1 & \cdots & 0 \\ \vdots & \vdots & \ddots & \vdots & \vdots & \vdots & \ddots & \vdots \\ a_{m1} & a_{m2} & \cdots & a_{mn} & 0 & 0 & \cdots & -1 \\ \end{bmatrix} \quad \bar{x} = \begin{bmatrix} 0 \\ 0 \\ \vdots \\ 0 \\ \end{bmatrix}$$

At the beginning, all variable in the original $x$ are non-basic, while all slack variables are basic. Then, we start enforcing the bounds one by one. Each time the current assignment is stricter than the current assignment of a non-basic variable, we update the value of the basic variables accordingly. Otherwise, we simply update the current bound of the basic variable, and check if the current assignment violates it. If it does, we try to pivot the basic variable with a non-basic variable that allows us to satisfy the violated bound. If we find such a variable, we perform the pivoting operation and update the values of the basic variables accordingly. If we cannot find such a variable, it means that the original problem is unsatisfiable, and we must return an explanation to the SAT solver.