优化乘法和除法 [英] Optimizing a Multiplication and Division

问题描述

我设置了一些边界/约束并想解决它们，但是当我使用乘法和除法函数时，优化并不像我认为的那样.

这是我的代码:

import com.microsoft.z3.*;导入 java.util.*;System.setProperty( "java.library.path", "/local/Programs/z3-4.6.0-x64-osx-10.11.6/bin/" );//设置sys_paths为空final Field sysPathsField = ClassLoader.class.getDeclaredField("sys_paths");sysPathsField.setAccessible(true);sysPathsField.set(null, null);//System.loadLibrary("libz3java");HashMap<字符串，字符串>cfg = new HashMap();cfg.put("model", "true");上下文 ctx = 新上下文(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("优化系统...");优化 optsys = ctx.mkOptimize();optsys.Add(两个边界P，两个边界质量，//这里是不工作的分区ctx.mkEq(ctx.mkDiv(P,Mass), 速度)//乘法也不行//ctx.mkEq(ctx.mkMul(P,Mass), 速度));Optimize.Handle optimizeSpeed = optsys.MkMaximize(Speed);System.out.println(optsys.Check());System.out.println(optsys.getReasonUnknown());System.out.println("优化速度:" + optimizeSpeed);

它作为除法和乘法的输出:

优化系统...未知(不完整(理论算术))优化速度:0

虽然应该分别是 4 和 8000000.它应该是可满足的，而不是未知的.这里有什么问题，为什么我不能针对这个简单的功能进行优化?

我发现了这个:Z3 如何处理非线性整数算法?>

这是否意味着这个方程不可解?乘法和除法不是线性的吗?

解决方案

这里的问题是 Z3 的优化器无法真正处理非线性算术.(在这种情况下，非线性意味着您将两个符号量相乘/相除.与常量相乘/相除应该没问题.)

在这些情况下的技巧是进行迭代循环.您放入断言，然后迭代以获得更好"的值，只要满足约束即可.当然，这不能保证收敛，因此您可能必须在某个时候切断"循环.

对于您的示例，以下是 Python 中的等效代码:

from z3 import *s = 求解器()功率 = 真实('功率')s.add (Power >= 0);s.add (Power <= 4000)质量 = 真实('质量')s.add(质量 >= 1000)；s.add (质量 <= 2000);速度 = 真实 ('速度');s.add (速度 == 功率/质量);我 = 1m = 无而 s.check() == 坐:m = s.model()打印 ("迭代 %d:" % i),打印 m[速度]s.add(速度> m[速度])我=我+1打印最终模型:"打印米

打印:

$ python a.py迭代 1:1/1001迭代 2:2/1001迭代 3:3/1001迭代 4:2迭代 5:3迭代 6:4最终模型:[功率 = 4000，质量 = 1000，速度 = 4]

我相信你可以把它翻译成 Java；尽管我建议至少使用更好的语言来处理这些想法.

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?

解决方案

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.

这篇关于优化乘法和除法的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！