Optimizing a Multiplication and Division

Question

I set up a few boundaries/constraints and wanted to solve them, however when I use the functions multiplication and division the optimisation is not as it should be in my opinion.

Here is my Code:

import com.microsoft.z3.*;
import java.util.*;

System.setProperty( "java.library.path", "/local/Programs/z3-4.6.0-x64-osx-10.11.6/bin/" );

//set sys_paths to null
final Field sysPathsField = ClassLoader.class.getDeclaredField("sys_paths");
        sysPathsField.setAccessible(true);
        sysPathsField.set(null, null);
        //System.loadLibrary("libz3java");
HashMap<String, String> cfg = new HashMap<String, String>();
        cfg.put("model", "true");
        Context ctx = new Context(cfg);
RealExpr P = ctx.mkRealConst("Power");
RealExpr LowerBoundP = ctx.mkReal(0);
RealExpr UpperBoundP = ctx.mkReal(4000);
BoolExpr boundP1 = ctx.mkLe(P, UpperBoundP);
BoolExpr boundP2 = ctx.mkGe(P, LowerBoundP);
BoolExpr bothBoundsP = ctx.mkAnd(boundP1, boundP2);
RealExpr Mass = ctx.mkRealConst("Mass");
RealExpr LowerBoundMass = ctx.mkReal(1000);
RealExpr UpperBoundMass = ctx.mkReal(2000);
BoolExpr boundMass1 = ctx.mkLe(Mass, UpperBoundMass);
BoolExpr boundMass2 = ctx.mkGe(Mass, LowerBoundMass);
BoolExpr bothBoundsMass = ctx.mkAnd(boundMass1, boundMass2);
System.out.println("Optimizing System ...");
Optimize optsys = ctx.mkOptimize();
optsys.Add(
bothBoundsP,
bothBoundsMass,
//Here is the Division that does not work
ctx.mkEq(ctx.mkDiv(P,Mass), Speed)
//Multiplication does not work as well
//ctx.mkEq(ctx.mkMul(P,Mass), Speed)
);
Optimize.Handle optimizeSpeed = optsys.MkMaximize(Speed);
System.out.println(optsys.Check());
System.out.println(optsys.getReasonUnknown());
System.out.println("Optimized Speed: " + optimizeSpeed);

It gets as an output for Division and Multiplication:

Optimizing System ...
UNKNOWN
(incomplete (theory arithmetic))
Optimized Speed: 0

Though it should be 4 and 8000000 respectively. And it should be satisfiable and not unknown. What is the problem here and why can't I optimise for this simple function?

I found this: How does Z3 handle non-linear integer arithmetic?

Does that mean this equation is not solvable? Isn't Multiplication and division linear?

What is `boundMass1` and `boundMass2`? They only appear on the right-hand-side in your program, with no definition. — alias, Mar 07 '18 at 22:45
You're right. Thank you. I included the two missing lines in the code. — Frank Wawrzik, Mar 08 '18 at 13:09
Follow the Java Naming Conventions, variables other than constants always start with lowercase. So `LowerBoundP` should be `lowerBoundP`. The same thing counts for method names. — MC Emperor, Mar 08 '18 at 13:18

score 2 · Answer 1 · answered Mar 08 '18 at 19:25

The issue here is that Z3's optimizer cannot really handle non-linear arithmetic. (In this context, non-linear means you are multiplying/dividing two symbolic quantities. Multiplying/dividing with constants should be OK.)

The trick in these cases is to do an iterative loop. You put your assertions in, then iterate to get a "better" value so long as constraints are satisfied. Of course, this is not guaranteed to converge, so you might have to "cut" the loop at some point.

For your example, here's the equivalent coding in Python:

from z3 import *

s = Solver()

Power = Real ('Power')
s.add (Power >= 0);
s.add (Power <= 4000)

Mass = Real ('Mass')
s.add (Mass >= 1000);
s.add (Mass <= 2000);

Speed = Real ('Speed');

s.add (Speed == Power/Mass);

i = 1
m = None

while s.check() == sat:
  m = s.model ()
  print ("Iteration %d: " % i),
  print m[Speed]
  s.add (Speed > m[Speed])
  i = i+1

print "Final model: "
print m

This prints:

$ python a.py
Iteration 1:  1/1001
Iteration 2:  2/1001
Iteration 3:  3/1001
Iteration 4:  2
Iteration 5:  3
Iteration 6:  4
Final model:
[Power = 4000, Mass = 1000, Speed = 4]

I'm sure you can translate this to Java; though I'd recommend using a better language at least to play around with the ideas.

"Of course, this is not guaranteed to converge, so you might have to "cut" the loop at some point." Please could you clarify this point with more details? — Rehab11, Mar 15 '18 at 17:32
Imagine you're maximizing `x*y` with no other constraints other than both `x` and `y` are positive. Each time around the loop, Z3 would give you a "better" model, but you'd never figure out that the result is actually unbounded. Note that this can happen even if the objective has a bounded minima/maxima: As you find the "next" model, you're not guaranteed to hit it in a finite number of iterations. — alias, Mar 15 '18 at 17:51

Optimizing a Multiplication and Division

1 Answers1

Linked