How does the SMT solver Z3 handle conditional statements in a constraint?

Question

I have a constraint system which I seek to find solutions for. The constraints consist of lesser/equal inequalities which have a difference of two minimum expressions on their right side, for example:

$x_1 \leq min((x_2),(x_5 + x_6)) - min((x_3),(x_7 + x_8 + x_9))$

$x_2 \leq min((x_3 + x_4), (x_7)) - min((x_5 + x_8), (x_5 + x_9))$

Lacking an in-built minimum function, Z3 forces me to use pairwise comparisons in nested conditional statements. That works well and I either receive solutions or unsatisfiability results which are correct.

In order to formalize my approach, I would like to understand how Z3 deals with the conditional statements inside the inequalities. As there is no upper bound on the variables and as far as I can tell from Z3‘s verbose output, the SAT solver is not involved.

Does Z3 use a linearization method like the „big M“ approach and subsequent application of „cuts and branch“ or another technique?

Answer 1

I can't answer how Z3 works. I can only speculate on some possible ways one could build a solver for this type of constraints, if one wanted.

It appears all of your inequalities have the form

$$A \le \min(B,C) - \min(D,E)$$

where $A,B,C,D,E$ are linear expressions of the variables, i.e., each has the form $a_1x_1 + \dots + a_nx_n + b$, for some constants $a_1,\dots,a_n,b$. This is equivalent to

$$\min(F,G) \le \min(H,I)$$

(take $F=D+A$, $G=E+A$, $H=B+A$, $I=C+A$). This is equivalent to the two inequalities

$$\min(F,G) \le H, \min(F,G) \le I,$$

which in turn is equivalent to the two inequalities

$$\min(F-H,G-H) \le 0, \min(F-I,G-I) \le 0.$$

So, without loss of generality, we can assume you have a system of inequalities of the form

$$\min(U,V) \le 0$$

where each $U,V$ are linear expressions of the variables (with different constants).

I don't know how Z3 solves such a system of inequalities, but one approach is to use integer linear programming (ILP). In particular, for each such inequality, we can introduce a new variable $t$, constrain $t$ to be an integer, and add the following inequalities:

$$\begin{align*} t(U) + (1-t)V &\le 0\\ V &\le U + tM\\ U &\le V + (1-t)M\\ 0 &\le t \le 1 \end{align*}$$

where $M$ is a large constant (larger than the largest possible value of $|U-V|$). This is a big-M method, as you mention in your question, and as you indicate in the question, it's not guaranteed to work correctly if we don't have an upper bound on the value of $|U-V|$.

I don't know whether Z3 uses this technique, or if it does, how it deals with the lack of any known upper bound on $|U-V|$. One possible heuristic would be to guess at a large value of $M$; try to solve the corresponding ILP instance. If there is no feasible solution, then we know there is no feasible solution to the original problem. If there a feasible solution to the ILP instance, we can check whether it solves the original problem. If it solves the original problem, we can output it. If it doesn't, we can double $M$ and try again. I don't know whether there are any guarantees that this will ever terminate, but it is a possible heuristic.

Another possibility is that Z3 might internally use a SMT solver, specifically, SMT with linear inequalities over real variables. It is easy to express your problem as an instance of such a SMT formula, and there are sophisticated SMT solvers for testing satisfiability of such formulas. I suspect this might be the most likely possibility, but I don't have a basis for this suspicion.

Answer 2

A minimum expression $min(x_1, x_2)$ can be transformed by introducing a new variable $m$ replacing the expression and adding the following formula to the set of boolean combinations of (in/dis)equalities:

$(m \leq x_1) \land (m \leq x_2) \land ((m \geq x_1) \vee (m \geq x_2))$

The resulting problem is solved by the algorithm described in the paper https://yices.csl.sri.com/papers/cav06.pdf.