Efficient determination of feasible ranges for integer variables

[ptr1120]

Hello,

I am having the following kind of CSP problems where all variables are either of kind boolean or integer. The relations between variables can be either of kind boolean logic {∧, ∨, ->, !} or there can be equality and order relations {==,!=,<,>,>=,<=} between integer variables. The integer variables also have an initial domain of feasible values e.g. [-1000..1000].

Example:

Variables: { bool1, bool2, bool3, int1, int2, int3 }
Domains: { bool1, bool2, bool3 ∈ [0..1]; int1, int2, int3 ∈ [-1000..1000] }
Constraints: { bool1 -> int1 <= -50 ∨ int1 > 100; 
               bool2 -> int2 < 20; 
               int3 > int2;}

My question is now how can I efficiently propagate which ranges of the integer domain for each variable are feasible?
Obviously in the given Example and under the assumption that bool1 and bool2 are booth true the feasible ranges for the integer variables would be int1 ∈ [-1000..-50],[101..1000]; int2 ∈ [-1000..19]; int3 ∈ [-1000..18].

My simple approach would be to extract all relations with integer variables {e.g. {int1 <= -50; int1 > 100; int1 > 100; int2 < 20; int3 > int2}) and than check for each variable whether there is a possible solution for one representative value of the related relations.
My question: is there any more algorithmic way or any interface inside Z3 that would help me solve this kind of problem?
I already researched and found several algorithms in the field of "Interval Constraint Satisfaction Problem (ICSP)", but they are mainly about real typed variables and I think for integer variables there may be a simpler way to do this.

Thank you

[NikolajBjorner]

One approach is to apply nested maximization calls to widen feasible intervals from sample points.
A custom algorithm for bit-vectors that is used to represent all models is described here: https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/secguru.pdf
When you just extract intervals per variable, you don't need cubes/hyper cubes. It reduces to a single variable case.
There are cases where bit-vectors will be more efficient in the finite domain case. You can find min-max boundaries also from integer starting points by sampling satisfiable solutions, then invoke a different copy of the constraints using the optimization features.

[ptr1120]

Thank you so much for this information.