Integer Range - gsdlab/chocosolver GitHub Wiki

A -> int

How many solutions will the solver find for this model? This depends on the integer range set in the scope.


A scope of this setting will find 5 solutions where A = -2, A = -1, A = 0, A = 1, and A = 2. So the integer belonging to A is constrained by the integer range.

The solver does several optimizations to remove the integer range constraint if possible.

  1. Expressions are not constrained by the range. For example.
A -> int
B -> int
<< max (A.ref + B.ref) >>

In this example, suppose 2 is the upper limit of the integer range. It possible for A.ref + B.ref = 4 which exceeds the upper limit but this is okay because expressions are not constrained by the range. This will find the solution where goal is 4.

A -> int
B -> int
C -> int
[ C = A.ref + B.ref ]

There is a problem with this example. C = 2 is the largest we can set C. So the solver will never find the solution where A = 2 and B = 2 unless we increase the integer range.

  1. Partially known integers are not constrained by the range. Here are some examples where the integer is partially known.
A -> int
    [this.ref = 4]
B : Feature
    [this.footprint.ref = 4]

In this example, we know that A.ref = 4. Even though 4 is outside the integer range, the solver will just set it to 4 and ignore the range. Likewise, we know that footprint.ref = 4.

This works well for feature models as long as all the attributes are known.

A : Feature
    [this.footprint.ref = 3]
B : Feature
    [this.footprint.ref = 4]
C : Feature
    [this.footprint.ref = 5]

This is fine. We know that every footprint is either 3, 4, or 5, so the solver create integers that are large enough to handle this even if the upper limit on the integer range is only 2.

Future work

Improve the analysis for partially known integers to work in more cases.

As of right now, it does not recognize inequalites.

[ total_footprint <= 60 ]
[ total_footprint >= 10 ]

The solver is not smart enough right now to determine that total_footprint is between 10 and 60.