Z3最小化-infinity答案
Z3最小化-infinity答案
提问于 2021-06-06 10:38:49
我目前正在使用z3的c++应用程序接口，在最小化整型变量的总和时遇到了问题。
有一些整数变量(rv_i)，根据布尔变量r_i是真还是假，它们中的每一个都会变成某个正数或0。我想最小化rv_i的和，并像下面的代码一样断言表达式。我认为如果所有的rv_is都是假的，那么r_is的和的最小值应该是0，或者如果一些r_is是真的，那么s的和应该是某个正值，但是z3在打印最小化的结果时会给出负无穷大((* (- 1) oo))。为什么z3会将下面代码的最小值设为负无穷大？(检查结果为sat)
(declare-fun rv_10 () Int)
(declare-fun r_10 () Bool)
(declare-fun rv_9 () Int)
(declare-fun r_9 () Bool)
(declare-fun rv_8 () Int)
(declare-fun r_8 () Bool)
(declare-fun rv_7 () Int)
(declare-fun r_7 () Bool)
(declare-fun rv_6 () Int)
(declare-fun r_6 () Bool)
(declare-fun rv_5 () Int)
(declare-fun r_5 () Bool)
(declare-fun rv_4 () Int)
(declare-fun r_4 () Bool)
(declare-fun rv_3 () Int)
(declare-fun r_3 () Bool)
(declare-fun rv_2 () Int)
(declare-fun r_2 () Bool)
(declare-fun rv_1 () Int)
(declare-fun r_1 () Bool)
(declare-fun rv_0 () Int)
(declare-fun r_0 () Bool)
(declare-fun p_1 () Bool)
(declare-fun p_2 () Bool)
(declare-fun p_3 () Bool)
...
(assert (and (=> r_0 (= rv_0 1))
(=> r_1 (= rv_1 3))
(=> r_2 (= rv_2 5))
(=> r_3 (= rv_3 2))
(=> r_4 (= rv_4 2))
(=> r_5 (= rv_5 3))
(=> r_6 (= rv_6 5))
(=> r_7 (= rv_7 5))
(=> r_8 (= rv_8 5))
(=> r_9 (= rv_9 5))
(=> r_10 (= rv_10 5))
(assert (and (=> (not r_0) (= rv_0 0))
(=> (not r_1) (= rv_1 0))
(=> (not r_2) (= rv_2 0))
(=> (not r_3) (= rv_3 0))
(=> (not r_4) (= rv_4 0))
(=> (not r_5) (= rv_5 0))
(=> (not r_6) (= rv_6 0))
(=> (not r_7) (= rv_7 0))
(=> (not r_8) (= rv_8 0))
(=> (not r_9) (= rv_9 0))
(=> (not r_10) (= rv_10 0))
(assert (>= rv_0 0))
(assert (>= rv_1 0))
(assert (>= rv_2 0))
(assert (>= rv_3 0))
(assert (>= rv_4 0))
(assert (>= rv_5 0))
(assert (>= rv_6 0))
(assert (>= rv_7 0))
(assert (>= rv_8 0))
(assert (>= rv_9 0))
(assert (>= rv_10 0))
(assert (=> p_1 (and (or (not r_1) (not r_2)))))
(assert (=> p_2 (and (or r_0) (or r_1 r_2) (or r_3))))
(assert (=> p_3 (or r_6 r_7 r_8 r_9 r_10)))
...
(minimize (+ rv_0
rv_1
rv_2
rv_3
rv_4
rv_5
rv_6
rv_7
rv_8
rv_9
rv_10))
(check-sat)回答 1
Stack Overflow用户
发布于 2021-06-07 14:31:27
我不能复制这个。您的输入中有几个...，如果您删除它们并插入括号以结束相应的表达式，并在最后添加以下行(在check-sat之后)：
(get-objectives)然后z3说：
sat
(objectives
((+ rv_0 rv_1 rv_2 rv_3 rv_4 rv_5 rv_6 rv_7 rv_8 rv_9 rv_10) 0)
)因此，要么你已经...的部分有改变这个行为的代码(不太可能)，要么因为你使用C++应用程序接口进行编程，所以你没有正确地使用C++应用编程接口(更有可能)。
但是，如果看不到导致问题的实际完整输入，就不可能知道出了什么问题。我怀疑z3在这里有问题；你真的应该发布一个MWE (最小可操作示例)；请看这里：https://stackoverflow.com/help/minimal-reproducible-example
页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/67858170
复制相关文章
相似问题
社区富文本编辑器全新改版！诚邀体验～
全新交互，全新视觉，新增快捷键、悬浮工具栏、高亮块等功能并同时优化现有功能，全面提升创作效率和体验
腾讯云开发者
