1
$\begingroup$

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?

$\endgroup$
4
  • $\begingroup$ I'm not sure whether the internal details of the implementation of Z3 are on-topic here. $\endgroup$
    – D.W.
    Commented Oct 3, 2022 at 21:15
  • 1
    $\begingroup$ I don't think I understand what inequalities can occur. Can you specify this in mathematics? Can you give the general form of an inequality, in mathematics? Are all terms linear expressions, so that every inequality can be expressed as $0 \le \min(E, F) - \min(G, H)$ where each of $E,F,G,H$ is an expression of the form $a_1x_1 + \dots + a_nx_n + c$ (with different constants $a_1,\dots,a_n,c$ for each expression)? $\endgroup$
    – D.W.
    Commented Oct 3, 2022 at 21:15
  • $\begingroup$ Yes, the constraints all contain linear expressions of the form you state with different constants (all being 0 or 1) and c = 0 for all expressions. $\endgroup$
    – MvB
    Commented Oct 4, 2022 at 5:16
  • $\begingroup$ The general form is quite complicated as it depends on the verification behaviour of propositional formulas in logical interpretations, but it boils down to inequalities of the type you describe that I have given two examples for in an edit of the question. $\endgroup$
    – MvB
    Commented Oct 4, 2022 at 5:18

2 Answers 2

1
$\begingroup$

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.

$\endgroup$
5
  • $\begingroup$ Thank you very much, this has clarified the issue for me and points me in the right direction as Z3 does indeed say „smt.searching“. Do you also have an idea about what algorithms an SMT solver would use for the given problem? $\endgroup$
    – MvB
    Commented Oct 4, 2022 at 6:17
  • 1
    $\begingroup$ @MvB, I don't, but you could read the Z3 paper (microsoft.com/en-us/research/project/z3-3/publications), read about the Nelson-Oppen framework, read the paper A fast linear-arithmetic solver for DPLL(T), and use them to do a bit of a literature search. See also en.wikipedia.org/wiki/…. $\endgroup$
    – D.W.
    Commented Oct 4, 2022 at 7:01
  • $\begingroup$ Scanning the papers, I‘ve realized that I had checked them a while ago. I can see how the minimum function and/or conditional statements are handled but still have no idea how Z3 deals with the lack of explicit upper bounds if the problem is indeed transformed into a SAT problem. That was why my original question dealt with Z3 possibly employing cuts-and-branch in some variation. Nevertheless, thanks for your input. $\endgroup$
    – MvB
    Commented Oct 4, 2022 at 7:55
  • 1
    $\begingroup$ @MvB, I believe that for SMT, DPLL(T) (the "lazy" approach) uses SAT without needing explicit upper bounds, because it is not using SAT to reason about the specific values of the real-valued variables, but to reason about which combinations of inequalities are true and which are false. $\endgroup$
    – D.W.
    Commented Oct 4, 2022 at 9:08
  • $\begingroup$ That totally makes sense and lets me formulate the minimum expressions not with conditional statements, but with additional inequalities. Thanks for pointing that out. $\endgroup$
    – MvB
    Commented Oct 4, 2022 at 10:26
1
$\begingroup$

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.

$\endgroup$

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.