Z3 最小化-无穷大答案

编程问答 2022-04-28

问题描述

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

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

解决方法

我无法复制这个。您的输入中有一些 ...，如果您删除它们并插入括号以关闭相应的表达式，并在最后（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

c++infinityminimizeoptimizationoptimizationz3