决定Z3求解器优化精度的重要决策因素是什么？

分类：编程问答

如何解决决定Z3求解器优化精度的重要决策因素是什么？

要使用Z3求解器获得优化解决方案，我已经学习了两种优化方法。一种是使用带有“ MkMaximize”或“ MkMinimize”指令的优化求解器。另一种是将优化器方法与通用求解器一起使用，作为[优化超时1]问题的描述。

我发现有时存在不一致，这使我习惯于了解到优化器方法可以得到更准确的答案，而优化求解器的优化方法却是有限的。但是我发现不一致不是永久性的，有时用两种方法生成的解可能是相同的。

我想知道是哪一种方法决定了两种方法之间的不一致，是表述约束还是目标？而且我想获取导致优化求解器不正确的信息。

添加示例：

      Context ctx = new Context();
     Optimize o = ctx.mkOptimize();
     ArithExpr M1A10 = ctx.mkIntConst("M1A10");
     ArithExpr M2A10 = ctx.mkIntConst("M2A10");
     ArithExpr M3A10 = ctx.mkIntConst("M3A10");
     ArithExpr M1A20 = ctx.mkIntConst("M1A20");
     ArithExpr M2A20 = ctx.mkIntConst("M2A20");
     ArithExpr M3A20 = ctx.mkIntConst("M3A20");
     
     ArithExpr M1B10 = ctx.mkIntConst("M1B10");
     ArithExpr M2B10 = ctx.mkIntConst("M2B10");
     ArithExpr M3B10 = ctx.mkIntConst("M3B10");
     ArithExpr M1B20 = ctx.mkIntConst("M1B20");
     ArithExpr M2B20 = ctx.mkIntConst("M2B20");
     ArithExpr M3B20 = ctx.mkIntConst("M3B20");
     ArithExpr M1B30 = ctx.mkIntConst("M1B30");
     ArithExpr M2B30 = ctx.mkIntConst("M2B30");
     ArithExpr M3B30 = ctx.mkIntConst("M3B30");
     
     ArithExpr M1C10 = ctx.mkIntConst("M1C10");
     ArithExpr M2C10 = ctx.mkIntConst("M2C10");
     ArithExpr M3C10 = ctx.mkIntConst("M3C10");
     ArithExpr M1C20 = ctx.mkIntConst("M1C20");
     ArithExpr M2C20 = ctx.mkIntConst("M2C20");
     ArithExpr M3C20 = ctx.mkIntConst("M3C20");
     ArithExpr M1C30 = ctx.mkIntConst("M1C30");
     ArithExpr M2C30 = ctx.mkIntConst("M2C30");
     ArithExpr M3C30 = ctx.mkIntConst("M3C30");
     
     ArithExpr M1A = ctx.mkAdd(M1A10,M1A20);
        ArithExpr M2A = ctx.mkAdd(M2A10,M2A20);
        ArithExpr M3A = ctx.mkAdd(M3A10,M3A20);
        ArithExpr M1B = ctx.mkAdd(M1B10,M1B20,M1B30);
        ArithExpr M2B = ctx.mkAdd(M2B10,M2B20,M2B30);
        ArithExpr M3B = ctx.mkAdd(M3B10,M3B20,M3B30);   
        ArithExpr M1C = ctx.mkAdd(M1C10,M1C20,M1C30);
        ArithExpr M2C = ctx.mkAdd(M2C10,M2C20,M2C30);
        ArithExpr M3C = ctx.mkAdd(M3C10,M3C20,M3C30);

        ArithExpr M1z10= ctx.mkAdd(M1A10,M1B10,M1C10);
        ArithExpr M2z10= ctx.mkAdd(M2A10,M2B10,M2C10);
        ArithExpr M3z10= ctx.mkAdd(M3A10,M3B10,M3C10);

        ArithExpr M1z20= ctx.mkAdd(M1A20,M1C20);
        ArithExpr M2z20= ctx.mkAdd(M2A20,M2C20);
        ArithExpr M3z20= ctx.mkAdd(M3A20,M3C20);

        ArithExpr M1z30= ctx.mkAdd(M1B30,M1C30);
        ArithExpr M2z30= ctx.mkAdd(M2B30,M2C30);
        ArithExpr M3z30= ctx.mkAdd(M3B30,M3C30);
        
        o.Add(ctx.mkGe(M1A10,ctx.mkInt(0)));
        o.Add(ctx.mkGe(M1A20,ctx.mkInt(0)));
        o.Add(ctx.mkGe(M2A10,ctx.mkInt(0)));
        o.Add(ctx.mkGe(M2A20,ctx.mkInt(0)));
        o.Add(ctx.mkGe(M3A10,ctx.mkInt(0)));
        o.Add(ctx.mkGe(M3A20,ctx.mkInt(0)));
        
        o.Add(ctx.mkGe(M1B10,ctx.mkInt(0)));
        o.Add(ctx.mkGe(M1B20,ctx.mkInt(0)));
        o.Add(ctx.mkGe(M1B30,ctx.mkInt(0)));
        o.Add(ctx.mkGe(M2B10,ctx.mkInt(0)));
        o.Add(ctx.mkGe(M2B20,ctx.mkInt(0)));
        o.Add(ctx.mkGe(M3B30,ctx.mkInt(0)));
        o.Add(ctx.mkGe(M3B10,ctx.mkInt(0)));
        o.Add(ctx.mkGe(M3B20,ctx.mkInt(0)));
        
        o.Add(ctx.mkGe(M1C10,ctx.mkInt(0)));
        o.Add(ctx.mkGe(M1C20,ctx.mkInt(0)));
        o.Add(ctx.mkGe(M1C30,ctx.mkInt(0)));
        o.Add(ctx.mkGe(M2C10,ctx.mkInt(0)));
        o.Add(ctx.mkGe(M2C20,ctx.mkInt(0)));
        o.Add(ctx.mkGe(M2C30,ctx.mkInt(0)));
        o.Add(ctx.mkGe(M3C30,ctx.mkInt(0)));
        o.Add(ctx.mkGe(M3C10,ctx.mkInt(0)));
        o.Add(ctx.mkGe(M3C20,ctx.mkInt(0)));


        o.Add(ctx.mkLt(M1z10,ctx.mkInt(80)));
        o.Add(ctx.mkLt(M1z20,ctx.mkInt(80)));
        o.Add(ctx.mkLt(M1z30,ctx.mkInt(80)));

        o.Add(ctx.mkLt(M2z10,ctx.mkInt(80)));
        o.Add(ctx.mkLt(M2z20,ctx.mkInt(80)));
        o.Add(ctx.mkLt(M2z30,ctx.mkInt(80)));

        o.Add(ctx.mkLt(M3z10,ctx.mkInt(80)));
        o.Add(ctx.mkLt(M3z20,ctx.mkInt(80)));
        o.Add(ctx.mkLt(M3z30,ctx.mkInt(80)));
        
        o.Add(ctx.mkGe(ctx.mkAdd(ctx.mkMul(M1A10,ctx.mkInt(100)),ctx.mkMul(ctx.mkInt(200),M2A10),ctx.mkMul(ctx.mkInt(150),M3A10)),ctx.mkInt(20000)));
        o.Add(ctx.mkGe(ctx.mkAdd(ctx.mkMul(M1A,M2A),M3A)),ctx.mkInt(40000)));
        o.Add(ctx.mkGe(ctx.mkAdd(ctx.mkMul(ctx.mkAdd(M1B10,M1B20),ctx.mkInt(150)),ctx.mkMul(ctx.mkInt(300),ctx.mkAdd(M2B10,M2B20)),ctx.mkAdd(M3B10,M3B20))),ctx.mkInt(25000)));
        o.Add(ctx.mkGe(ctx.mkAdd(ctx.mkMul(M1B,M2B),M3B)),ctx.mkInt(45000)));
        o.Add(ctx.mkGe(ctx.mkAdd(ctx.mkMul(M1C,ctx.mkInt(200)),ctx.mkMul(ctx.mkInt(250),M2C),M3C)),ctx.mkInt(30000)));

        ArithExpr time = ctx.mkAdd( M1A,M2A,M3A,M1B,M2B,M3B,M1C,M2C,M3C);
o.MkMinimize(time);
        //  o.Add(ctx.mkLt(time,ctx.mkInt(550)));
        o.Check();
        if(o.Check() == Status.SATISFIABLE)
        {
            
            M1A10=(ArithExpr) o.getModel().getConstInterp(M1A10).simplify();
            M1A20=(ArithExpr) o.getModel().getConstInterp(M1A20).simplify();
            M2A10=(ArithExpr) o.getModel().getConstInterp(M2A10).simplify();
            M2A20=(ArithExpr) o.getModel().getConstInterp(M2A20).simplify();
            M3A10=(ArithExpr) o.getModel().getConstInterp(M3A10).simplify();
            M3A20=(ArithExpr) o.getModel().getConstInterp(M3A20).simplify();
            
            M1B10=(ArithExpr) o.getModel().getConstInterp(M1B10).simplify();
            M1B20=(ArithExpr) o.getModel().getConstInterp(M1B20).simplify();
            M1B30=(ArithExpr) o.getModel().getConstInterp(M1B30).simplify();
            M2B10=(ArithExpr) o.getModel().getConstInterp(M2B10).simplify();
            M2B20=(ArithExpr) o.getModel().getConstInterp(M2B20).simplify();
            M2B30=(ArithExpr) o.getModel().getConstInterp(M2B30).simplify();
            M3B10=(ArithExpr) o.getModel().getConstInterp(M3B10).simplify();
            M3B20=(ArithExpr) o.getModel().getConstInterp(M3B20).simplify();
            M3B30=(ArithExpr) o.getModel().getConstInterp(M3B30).simplify();
            
            M1C10=(ArithExpr) o.getModel().getConstInterp(M1C10).simplify();
            M1C20=(ArithExpr) o.getModel().getConstInterp(M1C20).simplify();
            M1C30=(ArithExpr) o.getModel().getConstInterp(M1C30).simplify();
            M2C10=(ArithExpr) o.getModel().getConstInterp(M2C10).simplify();
            M2C20=(ArithExpr) o.getModel().getConstInterp(M2C20).simplify();
            M2C30=(ArithExpr) o.getModel().getConstInterp(M2C30).simplify();
            M3C10=(ArithExpr) o.getModel().getConstInterp(M3C10).simplify();
            M3C20=(ArithExpr) o.getModel().getConstInterp(M3C20).simplify();
            M3C30=(ArithExpr) o.getModel().getConstInterp(M3C30).simplify();
            
            ArithExpr timeA = ctx.mkAdd(M1A10,M1A20,M2A10,M2A20,M3A10,M3A20,M1B30,M2B30,M3B30,M1C10,M1C30,M2C10,M2C30,M3C10,M3C30);
            
            System.out.println(timeA.simplify());
        }
        
        System.out.println(o.Check());
 }

这个例子很长。 指令'mkMinimize'的结果为557，但是当我使用'o.Add（ctx.mkLt（time，ctx.mkInt（550）））;'的约束时。它仍在工作并生成549的结果。

解决方法

不幸的是，很难准确地理解您要问的问题。但是基于这些评论，我正在收集到您是在说以下情况：

  1. 您使用z3的优化程序，它为您提供了最小值
  2. 您在求解器周围循环，要求小于此最小值的值仍能满足您的所有约束。规划求解说sat，可以为您带来更好的价值。

如果是这种情况，那么应该报告z3中的错误。如果优化程序为您返回了一个值，那么它实际上就是最佳选择：不应存在满足约束条件的“更好”（即，取决于正在执行的优化类型，是“较小”还是“较大”）。

但是从您的描述中无法确定是否是这种情况。如果您实际上将Stackoverflow减少到一个最小的例子来显示问题，那么Stackoverflow效果最好，以便人们可以复制该问题。您也可能会遇到一些与编码有关的问题，这些问题会使您误入歧途。但是，如果您确定上面是发生了什么，那么那不是z3上的错误，因此应在其错误跟踪器中报告该错误，并提供尽可能少的示例。 （https://github.com/Z3Prover/z3/issues）

版权声明：本文内容由互联网用户自发贡献，该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务，不拥有所有权，不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容， 请发送邮件至 dio@foxmail.com 举报，一经查实，本站将立刻删除。

相关推荐

matplotlib报错：AttributeError: module 'backend_interagg' has no attribute 'FigureCanvas'. Did you mean: 'FigureCanvasAgg'?
使用本地python环境可以成功执行 import pandas as pd import matplotlib.pyplot as plt # 设置字体 plt.rcParams['font.sans-serif'] = ['SimHei'] # 能正确显示负号 p
gitlab登录失败，报错：This challenge page was accidentally cached by an intermediary and is no longer available.
设置时间 控制面板
后端开发常见错误
错误1：Request method ‘DELETE‘ not supported 错误还原：controller层有一个接口，访问该接口时报错：Request method ‘DELETE‘ not supported 错误原因：没有接收到前端传入的参数，修改为如下 参考 错误2：cannot r
docker常见错误
错误1：启动docker镜像时报错：Error response from daemon: driver failed programming external connectivity on endpoint quirky_allen 解决方法：重启docker -> systemctl r
idea常见错误
错误1：private field ‘xxx‘ is never assigned 按Altʾnter快捷键，选择第2项 参考：https://blog.csdn.net/shi_hong_fei_hei/article/details/88814070 错误2：启动时报错，不能找到主启动类 #
pip安装依赖失败
报错如下，通过源不能下载，最后警告pip需升级版本 Requirement already satisfied: pip in c:\users\ychen\appdata\local\programs\python\python310\lib\site-packages (22.0.4) Coll
maven常见错误
错误1：maven打包报错 错误还原：使用maven打包项目时报错如下 [ERROR] Failed to execute goal org.apache.maven.plugins:maven-resources-plugin:3.2.0:resources (default-resources)
cloud项目中常见错误
错误1：服务调用时报错 服务消费者模块assess通过openFeign调用服务提供者模块hires 如下为服务提供者模块hires的控制层接口 @RestController @RequestMapping("/hires") public class FeignControl
springboot常见错误
错误1：运行项目后报如下错误 解决方案 报错2：Failed to execute goal org.apache.maven.plugins:maven-compiler-plugin:3.8.1:compile (default-compile) on project sb 解决方案：在pom.
springmvc拦截器中使用redisTemplate报空指针异常
参考 错误原因 过滤器或拦截器在生效时，redisTemplate还没有注入 解决方案：在注入容器时就生效 @Component //项目运行时就注入Spring容器 public class RedisBean { @Resource private RedisTemplate<String
vite报错：npm ERR! command C:WINDOWSsystem32cmd.exe /d /s /c C:UsersychenAppDataLocalTempnpx-dde1c848.cmd
使用vite构建项目报错 C:\Users\ychen\work>npm init @vitejs/app @vitejs/create-app is deprecated, use npm init vite instead C:\Users\ychen\AppData\Local\npm-
VM VirtualBox中安装centos时报错：设置基础软件仓库时出错
参考1 参考2 解决方案 # 点击安装源 协议选择 http:// 路径填写 mirrors.aliyun.com/centos/8.3.2011/BaseOS/x86_64/os URL类型 软件库URL 其他路径 # 版本 7 mirrors.aliyun.com/centos/7/os/x86
kafka常见问题
报错1 [root@slave1 data_mocker]# kafka-console-consumer.sh --bootstrap-server slave1:9092 --topic topic_db [2023-12-19 18:31:12,770] WARN [Consumer clie
hive常见问题
错误1 # 重写数据 hive (edu)> insert overwrite table dwd_trade_cart_add_inc > select data.id, > data.user_id, > data.course_id, > date_format(
装载数据时报错：Failed to execute spark task, with exception 'org.apache.hadoop.hive.ql.metadata.HiveException(Failed to create spark client.)'
错误1 hive (edu)> insert into huanhuan values(1,'haoge'); Query ID = root_20240110071417_fe1517ad-3607-41f4-bdcf-d00b98ac443e Total jobs = 1
flume常见问题
报错1：执行到如下就不执行了，没有显示Successfully registered new MBean. [root@slave1 bin]# /usr/local/software/flume-1.9.0/bin/flume-ng agent -n a1 -c /usr/local/softwa
hadoop集群常见错误
虚拟及没有启动任何服务器查看jps会显示jps，如果没有显示任何东西 [root@slave2 ~]# jps 9647 Jps 解决方案 # 进入/tmp查看 [root@slave1 dfs]# cd /tmp [root@slave1 tmp]# ll 总用量 48 drwxr-xr-x. 2
hive常见错误
报错1 hive> show databases; OK Failed with exception java.io.IOException:java.lang.RuntimeException: Error in configuring object Time taken: 0.474 se
Linux常见错误
报错1 [root@localhost ~]# vim -bash: vim: 未找到命令 安装vim yum -y install vim* # 查看是否安装成功 [root@hadoop01 hadoop]# rpm -qa |grep vim vim-X11-7.4.629-8.el7_9.x
使用sqoop一直卡在：mapreduce.Job: Running job: job_1703173956074_0001
修改hadoop配置 vi /usr/local/software/hadoop-2.9.2/etc/hadoop/yarn-site.xml # 添加如下 <configuration> <property> <name>yarn.nodemanager.res
pythonJavaScriptjavaHTMLPHPreactjsC#AndroidCSSNode.jssqlrpython-3.xMysqLjQueryc++pandasFlutterangularIOSdjangolinuxswifttypescript路由器JSON路由器设置无线路由器h3c华三华三路由器设置华三路由器电脑软件教程arraysdocker软件图文教程Cvue.jslaravelspring-boot