how to port a minizinc model into Z3 using C# API via PowerShell

[eosfor]

Hello colleagues,

I have a minizinc model, which is supposed to solve an "assignment" problem. Basically, having a list of Virtual Machine objects with their attributes, I'm trying to map them to their counterparts in Azure, in such a way that the counterpart has enough vCPUs and RAM. Additionally, I'm trying to minimize the target cost and maximize the performance attributes.

To make it a bit more interactive, easier to use from the command line I'm want to use .NET interface through PowerShell. It allows to combine all necessary tools under the same umbrella, so one does not need to install anything except PowerShell, basically

The minizinc model is here.
The PowerShell script is here
The data files and z3 binaries to make it work are also there.

So what I'm trying to do is literally map it to z3.

First, I'm preparing necessary data by reading a few CSV files and indexing that data to hashtables, just to speed up access

# import raw VM data and convert strings to ints
$sourceVMs = Import-Csv .\vmdata.csv
$sourceVMs  | % { $_.cpu = [int]$_.cpu; $_.ram = [int]$_.ram; $_.datadisk = [int]$_.datadisk; }

$targetSizes = import-csv ".\vmCostACUData.csv"

## hash tables with data to simplify search
$sourceVmHt = @{}
$targetVmHt = @{}

$sourceVMs | % {
    $sourceVmHt[$_.vmID] = $_
}

$targetSizes | % {
    $targetVmHt[$_.Name] = $_
}
##

Next, I basically create the necessary enums, as I did in the minizinc model. They are supposed to limit possible values of the decision variables and serve as indexes in some cases.

# enum existingVMs;
# enum vmSizes;

$existingVMs = $ctx.MkEnumSort("existingVMs", $sourceVMs.vmid)
$vmSizes = $ctx.MkEnumSort("vmSizes", $targetSizes.Name)

Create a bunch of decision variables, each of which is supposed to contain a name of that target VM size, calculated by the model, and store them in the array

$selectedSize = 
    $sourceVMs | % {
        $ctx.MkConst($_.vmid, $vmSizes)
    }

and add two main constraints

# constraint forall(vm in existingVMs)(
#    vmSizeCPU[selectedSize[vm]] >=  vmCPU[vm]
# );


## assuming $_.ToString() returns the name of the variable
## and $_ it's value
$selectedSize | % {
    $a = $ctx.MkNumeral($sourceVmHt[$_.ToString()].cpu, $ctx.MkIntSort())
    $b = $ctx.MkNumeral($targetVmHt[$_].vCPUs, $ctx.MkIntSort())
    $s.Add( $ctx.MkGt($a, $b))
}

# constraint forall(vm in existingVMs)(
#     vmSizeRAM[selectedSize[vm]] >= vmRAM[vm]
# );

$selectedSize | % {
    $a = $ctx.MkNumeral($sourceVmHt[$_.ToString()].ram, $ctx.MkIntSort())
    $b = $ctx.MkNumeral($targetVmHt[$_].MemoryGB, $ctx.MkIntSort())
    $s.Add( $ctx.MkGt($a, $b))
}

At this point I expect the model to return at least something, but it returns an empty model

PS C:\Work\z3tests> c:\Work\z3tests\z3.ps1
SATISFIABLE
PS C:\Work\z3tests> $m

NumConsts  : 0
ConstDecls : {}
Consts     : {}
NumFuncs   : 0
FuncDecls  : {}
Decls      : {}
NumSorts   : 0
Sorts      : {}

At least this is what I think I'm doing :)

The question here is - what I'm doing wrong, and what should I do to make it right?
And then how to make the model to try optimize the objective functions?

[NikolajBjorner]

ctx.MkNumeral tries to parse your string as a numeric constant not as a variable. Use MkConst

[eosfor]

Thanks, @NikolajBjorner

Let me probably put it a bit differently. To show where I am, I've put together a small project in C#. I hope this way it will be easier to explain. The project is here, the actual piece of code is here.

To my understanding, the main points are these. First I should create a set of "decision variables", the model should then decide their values. I assume that in Z3 they are called "constants", but I may be wrong :)/ So I create a set of such variables, and for simplicity store them in the dictionary.

The domain of each variable is limited by the enum, I derive from the source data

            var vmSizes = ctx.MkEnumSort("vmSizes", TargetVMIndex.Keys.ToArray());

            var selectedSize = new Dictionary<string, Expr>();


            for (int i = 0; i < SourceVM.Length; i++)
            {
                var name = SourceVM[i].Properties["vmid"].ToString();
                selectedSize.Add(name, ctx.MkConst(name, vmSizes));
            }

So here I assume, that the model should decide the value for each variable, based on constraints I want to supply. Constraints go as follows. Here I'm using the enum values as indexes into the source data and into the dictionary of variables. But for them, I need to use the value of the variable as an index in another data dictionary. And that is what I don't know how to do. The code below obviously does not work, and the question here is how to make it work?

            //constraint forall(vm in existingVMs)(
            //    vmSizeRAM[selectedSize[vm]] >= vmRAM[vm]
            //);
            foreach (var el in existingVMs.Consts)
            {
                var sourceObject = SourceVMIndex[el.ToString()];
                var targetObject = selectedSize[el.ToString()];
                s.Add(ctx.MkGt(TargetVMIndex[targetObject].vCPUs, sourceObject.cpu));
            }

            //constraint forall(vm in existingVMs)(
            //    vmSizeCPU[selectedSize[vm]] >= vmCPU[vm] * 0.8
            //);
            foreach (var el in existingVMs.Consts)
            {
                var sourceObject = SourceVMIndex[el.ToString()];
                var targetObject = selectedSize[el.ToString()];
                s.Add(ctx.MkGt(TargetVMIndex[targetObject].MemoryGB, sourceObject.ram));
            }

Perhaps I don't understand some concepts, as I'm trying to reflect my knowledge of minizinc into this and it may be not relevant. Would be really appreciated for any explanations or clues.

Thanks

[eosfor]

I spent some more time experimenting. Unfortunately, there are not that many "digestible" tutorials on C# APIs, so from time to time I'm just blindly trying this or that. But anyway, What I've done so far is this. In general, it is a PowerShell command implemented in C#. It takes two pieces of data, the list of "source" VMs and the lit of "target" sizes. And it tries to match one into another by a few parameters, like CPU and RAM + tries to optimize two objective functions. The "source list" has 87 rows in it, and the "target" on has 240 rows. So when I run this with the whole input it never ends. The sample usage is here

The question here is, do I do something wrong and where?

As a side note, minizing+gecode solves the same problem in less than a second. and minizinc + or-tools does it in around 5 seconds. So I assume that Z3 should do this somewhere around those numbers. So I assume I do smth wrong here, but I'm stuck and have no idea where to look :(

[NikolajBjorner]

I don't expect z3 to do well on problem domains it is not tuned for. It is not built specifically for OR domains.
These domains where z3 is not a suitable tool include LP problems, especially problems where constants are provided with a large decimal expansion and IP problems with bounded numbers. The sweet spot in some cases is discrete domains where you can leverage SMT features. See http://theory.stanford.edu/~nikolaj/supercharging.html for a case study.

[eosfor]

I'm trying to do it too. I also want to study how to extract the results from the model, similar to what I do with or-tools. Maybe you can paste the relevant pieces here :D?

Actually, I planned to convert all this C# code into pure PowerShell and try it in .NET interactive notebooks. The aim here was to open the modeling capability for those, who are not familiar with C# and are more oriented at scripting. It makes it available right in the command line. However the complexity of the C# interface itself, kind of, still makes it hard to use.

Does it make sense to "train" the solver to be able to deal with it?

BTW, separate question, does it make sense to interface Z3 to minizinc, as or-tools does, for example? Minizinc seems to provide a pretty convenient language for modeling. I know there is smt-lib, but it does not look as simple. Plus minizinc has a set of pretty good courses on Coursera, and that will give another push for Z3, perhaps. Just my IMHO.

Thanks again, @NikolajBjorner! All this is really cool and I still have much to learn. I wish there was a course on the topic, covering the concepts, C# API with examples, like here,

[eosfor]

I did it!

I did not have a chance to verify all the stuff yet, but as far as I can see the optimization objective values look the same as or-tools return. Now the question is, can Z3 do it faster. I wish it could

costs minimum

OR-TOOLS
CpSolverResponse summary:
status: OPTIMAL
objective: 20010
best_bound: 20010
booleans: 0
conflicts: 0
branches: 0
propagations: 0
integer_propagations: 1
restarts: 0
lp_iterations: 0
walltime: 0.636374
usertime: 0.636374
deterministic_time: 0.00416944
gap_integral: 0

Z3
Lower : 20010
Upper : 20010
Value : 20010
LowerAsVector : {0, 20010, 0}
UpperAsVector : {0, 20010, 0}

performance maximum

OR-TOOLS
CpSolverResponse summary:
status: OPTIMAL
objective: 584240
best_bound: 584240
booleans: 260
conflicts: 1095
branches: 2340
propagations: 88449
integer_propagations: 18152
restarts: 507
lp_iterations: 0
walltime: 6.82701
usertime: 6.82701
deterministic_time: 0.422987
gap_integral: 0.00604726

Z3
Lower : 584240
Upper : 584240
Value : 584240
LowerAsVector : {0, 584240, 0}
UpperAsVector : {0, 584240, 0}

Thank you SO MUCH, @NikolajBjorner!

🥳 🎉

[NikolajBjorner]

It solves in about 389 seconds, which is some orders of magnitude slower than what should be possible.
Small point fixes will not help and algorithmic changes are required to solve this kind of problems.
I learn from all examples; and learned a few minor issues that led to minor improvements, lurking under the covers.

I am not familiar with minizink to smtlib conversion efforts. There is https://link.springer.com/chapter/10.1007/978-3-030-58942-4_10, which targets the OMT solver. It is maybe good to expose z3 to the OR problem domains, which it will not be tuned for, but likely a time zink, I mean sink, given that the main backends to minizink are tuned for the problem sets already formulated for it while z3 is not at all.

[NikolajBjorner]

information like this:

booleans: 0
conflicts: 0
branches: 0
propagations: 0
integer_propagations: 1
restarts: 0
lp_iterations: 0

suggests the first objective is solved by pre-processing.
I guess the optimistic bound is feasible and therefore detected at once.

[eosfor]

In the end, I came up with this:

the PowerShell module to try Z3 and OR-TOOLS for this task: https://github.com/eosfor/AzureVmCalc. Z3 is hidden so far, due to the slowness. @NikolajBjorner doe it makes sense to register this as an, say, improvement request or something?

The .NET interactive notebook with the or-tools example. The Z3 one should look the same.

Thanks, @NikolajBjorner for all your help!