How to represent variance in a performant way?

[adarah]

Hi there, I discovered this wonderful tool today and it's working nicely, but I ran into a problem.
I need to add a soft-constraint that makes each variable's value as close to each other as possible.

To do this, I came up with the idea of using the variance to represent the overall distance of all points, which can be seem below:

vars = IntVector('my_prefix', len(valid_days))
scheme_mean = Sum(*vars)/len(valid_days)
square_diffs = [(v - scheme_mean)**2 for v in vars]
variance = Sum(*square_diffs)/(len(valid_days)-1)

The problem is that the time to solve the model shot up drastically (it is a pretty complicated expression after all). Usually I will have 30, 60 or 90 variables. Is there any better way to tackle this?

Here's the full code for reference: https://gist.github.com/Adarah/eb88a8b18f12ea501330838729e12ae5

[NikolajBjorner]

z3 doesn't have any support for such objectives. Note that convex, quadratic, objectives are handled by reasonable MIP tools, but not z3.
One way to deal with the limitation is to introduce piecewise linear approximations. z3 is happy to take functions that are defined in intervals.