python - 使用 SMTLIB2 查找 z3 中的最大数字
问题描述
我有 7 个杯子,里面有一些水。我需要对这些杯子进行编程以获得不同量的水。完成此操作后,我需要测量水量最多的杯子,然后取出一些量(比如 2 个单位的水)。
c实现:
float c1=2.0, c2= 2.6, c3 = 2.8, c4=4.4 , c5 = 2.4, c6 = 2.1, c7 = 5.8;
if((c1 > c2) && (c1 > c3) && (c1 > c4) && (c1 > c5) && (c1 > c6) && (c1 > c7)); c1=c1-2;
if((c2 > c1) && (c2 > c3) && (c2 > c4) && (c2 > c5) && (c2 > c6) && (c2 > c7)); c2=c2-2;
if((c3 > c2) && (c3 > c1) && (c3 > c4) && (c3 > c5) && (c3 > c6) && (c3 > c7)); c3=c3-2;
if((c4 > c2) && (c4 > c3) && (c4 > c1) && (c4 > c5) && (c4 > c6) && (c4 > c7)); c4=c4-2;
if((c5 > c2) && (c5 > c3) && (c5 > c4) && (c5 > c1) && (c5 > c6) && (c5 > c7)); c5=c5-2;
if((c6 > c2) && (c6 > c3) && (c6 > c4) && (c6 > c5) && (c6 > c1) && (c6 > c7)); c6=c6-2;
if((c7 > c2) && (c7 > c3) && (c7 > c4) && (c7 > c5) && (c7 > c6) && (c7 > c1)); c7=c7-2;
这将给出一个答案c7 = 3.8
我试图在 z3 中实现这一点,并将值分配给 c1....c7
ite( (and((> c1 c2) (> c1 c3) (> c1 c4) (> c1 c5) (> c1 c6) (> c1 c7))) (= c1_1 (- c1 2) (= c1_1 c1))
.
.
.repeated till c7_1
当我得到模型值时,它应该将 c7_1 设为 3.8
是否可以在 z3 中定义它?当我在 if 条件(在 ite 中)中使用不同条件的 and 时,它给了我一个错误。不能这样定义吗?有什么办法吗?
提前致谢
[问题描述][1]
我正在尝试使用 Z3 工具,很容易得到他的第一部分但是对于第二部分来说有点困难。
解决方案
当然。它在 SMTLib 中:
; declare the cups
(declare-const c1 Real)
(declare-const c2 Real)
(declare-const c3 Real)
(declare-const c4 Real)
(declare-const c5 Real)
(declare-const c6 Real)
(declare-const c7 Real)
; each cup has a non-negative units of water
(assert (>= c1 0))
(assert (>= c2 0))
(assert (>= c3 0))
(assert (>= c4 0))
(assert (>= c5 0))
(assert (>= c6 0))
(assert (>= c7 0))
; each amount is different
(assert (distinct c1 c2 c3 c4 c5 c6 c7))
; find maximum, helper function
(define-fun max ((a Real) (b Real)) Real (ite (> a b) a b))
; find the cup with maximum water in it
(define-fun maxC () Real (max c1 (max c2 (max c3 (max c4 (max c5 (max c6 c7)))))))
; make sure there's at least 2 units in the max, per the problem
(assert (>= maxC 2))
; final value
(define-fun finalRes () Real (- maxC 2))
; solve
(check-sat)
(get-value (c1 c2 c3 c4 c5 c6 c7 maxC finalRes))
z3 说:
sat
((c1 2.0)
(c2 (/ 11.0 6.0))
(c3 (/ 19.0 12.0))
(c4 (/ 7.0 4.0))
(c5 (/ 3.0 2.0))
(c6 (/ 23.0 12.0))
(c7 (/ 5.0 3.0))
(maxC 2.0)
(finalRes 0.0))
所以,看起来它把2
单位放在 中c1
,比2
其他所有单位都少,所以你最终得到了一个0
左值。
您的问题在此处可能存在哪些其他限制方面相当模糊,但希望这可以帮助您入门。
推荐阅读
- r - 如何取消缩放滚动缩放的数据
- c# - 为什么字符串在 MessageBox 中有效但在 if 语句中无效
- jsf - 指向位于远程 CDN 上的资源
- windows - FFmpeg 录制可在一台笔记本电脑上工作,但不能在另一台笔记本电脑上工作
- powershell - Azure 远程 VM 脚本
- java - POST JSON 到服务器并接收响应
- .net-core - Blazor Server 项目中无法识别共享命名空间
- python - Python 中的 3D 绘图 - 向散点图添加图例
- react-native - 不变违规:requireNativeComponent:在此 UIManager 中未找到 RNViewOverflow
- html - 试图了解如何使用自定义 Drupal 主题显示图像