Which techniques are used to handle Non-linear Integer Real problems in z3?

StackOverflow https://stackoverflow.com/questions/21247410

  •  30-09-2022
  •  | 
  •  

Question

Here are z3 statistics for a problem in the Non-Linear Integer Real Fragment (and many of my problems are similar to this): 

 (:add-rows            11062574
  :added-eqs           34
  :arith-conflicts     37293
  :assert-lower        837747
  :assert-upper        1909779
  :binary-propagations 13807730
  :bound-prop          32666
  :conflicts           47631
  :decisions           157457
  :del-clause          32828
  :final-checks        39307
  :gcd-tests           329820
  :gomory-cuts         927
  :ineq-splits         19490
  :memory              39.52
  :minimized-lits      93912
  :mk-clause           73468
  :pivots              768193
  :propagations        15992318
  :pseudo-nonlinear    254856
  :restarts            41
  :time                151.65
  :total-time          151.68)

Since the problem is non-linear, I believe the Simplex technique is not directly being used to solve this (although I see some Simplex-like statistics in the output). Based on an earlier response, I understand the non-linear Real technique in the presence of Integers is based on Grobner bases, and that the relevant functions are in theory_arith*. Is there a paper/some documentation where I could find specific information about the techniques that are implemented in z3 for this fragment?

Also, although the problem is non-linear as such, the only occurrence of non-linearity involve multiplication of two variables (and there are a few such expressions), and one of the variables can only taken on values that are powers of two and bound/defined by some simple constraints:

(const1 <=  |a| < const2) => (var-a = const1)

where const1 and const2 are consecutive positive powers of two. Thus, var-a represents the largest power of two lesser than or equal to |a|. These variables were declared to be of type Real. Especially curious since I see a term pseudo-nonlinear in the stats output. Are the constraints being linearized internally, in some way? Also, is there a better way to encode these constraints so that z3 does better on such problems?

Licensed under: CC-BY-SA with attribution
Not affiliated with StackOverflow
scroll top