Z3 最小化-无穷大答案

Question

我目前正在使用 z3 的 c++ API，并且在最小化整数变量的总和时遇到了问题。

有一些整数变量 (rv_i)，它们中的每一个都变成某个正数或 0，这取决于布尔变量 r_i 是真还是假。我想最小化rv_is 的总和并断言如下代码所示的表达式。 我认为如果所有r_is 都为假，则rv_is 之和的最小值应该为0，或者如果r_is 中的一些为真，则应该是某个正值，但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)

Answer 1

我无法复制这个。您的输入中有几个...，如果您删除这些并插入括号以关闭相应的表达式，并在最后添加以下行（在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++ API 进行编程，所以您并没有正确使用 C++ API（更多可能）。

但是如果没有看到导致问题的实际完整输入，就不可能知道发生了什么问题。我怀疑 z3 在这里有错；你真的应该发布一个 MWE（最小可行示例）；看这里：https://stackoverflow.com/help/minimal-reproducible-example