Z3中如何优化一段代码？ （PI_NON_NESTED_ARITH_WEIGHT 相关）

Question

我在z3 中有一个代码，旨在解决an optimization problem for a boolean formula

(set-option :PI_NON_NESTED_ARITH_WEIGHT 1000000000)

(declare-const a0 Int) (assert (= a0 2))
(declare-const b0 Int) (assert (= b0 2))
(declare-const c0 Int) (assert (= c0 (- 99999)))
(declare-const d0 Int) (assert (= d0 99999))
(declare-const e0 Int) (assert (= e0 49))
(declare-const f0 Int) (assert (= f0 49))

(declare-const a1 Int) (assert (= a1 3))
(declare-const b1 Int) (assert (= b1 3))
(declare-const c1 Int) (assert (= c1 (- 99999)))
(declare-const d1 Int) (assert (= d1 99999))
(declare-const e1 Int) (assert (= e1 48))
(declare-const f1 Int) (assert (= f1 49))

(declare-const c Int)
(declare-const d Int)
(declare-const e Int)
(declare-const f Int)

(define-fun max ((x Int) (y Int)) Int
  (ite (>= x y) x y))

(define-fun min ((x Int) (y Int)) Int
  (ite (< x y) x y))

(define-fun goal ((c Int) (d Int) (e Int) (f Int)) Int
  (* (- d c) (- f e)))

(define-fun sat ((c Int) (d Int) (e Int) (f Int)) Bool
   (and (and  (>= d c) (>= f e))
        (forall ((x Int)) (=> (and (<= a0 x) (<= x b0))
                              (> (max c (+ x e)) (min d (+ x f)))))))

(assert (and (sat c d e f)
             (forall ((cp Int) (dp Int) (ep Int) (fp Int)) (=> (sat cp dp ep fp)
                                                               (>= (goal c d e f) (goal cp dp ep fp))))))

(check-sat)

我猜是因为量词和含义，这段代码成本很高。在线测试的时候给了我2个warning，最终结果是unknown：

failed to find a pattern for quantifier (quantifier id: k!33)
using non nested arith. pattern (quantifier id: k!48), the weight was increased to 1000000000 (this value can be modified using PI_NON_NESTED_ARITH_WEIGHT=<val>). timeout`. 

谁能告诉我这两个警告是否会避免获得好的结果？有什么办法可以优化这段代码让它运行吗？

Answer 1

我已经通过以下迭代方式解决了 Z3 中的优化问题，本质上是一个循环，通过多次调用 Z3 来搜索解决方案。

1. 找到一个解决方案（在您的情况下，是(sat c d e f)的解决方案

2. 计算该解决方案的值（如果您的解决方案是c0、d0、e0、f0、评估(goal c0 d0 e0 f0)。调用该值v0。

3. 找到新问题的解决方案(and (sat c1 d1 e1 f1) (> (goal c1 d1 e1 f1) v0))。

4. 如果第 3 点返回 UNSAT，v0 是您的最大值。如果不是，请使用新解决方案 v0 并返回第 3 点。

您有时可以通过先猜测一个上限（即值 cu、du、eu、fu 以使 (and (sat c d e f) (<= (goal cu du eu fu)) 是 UNSAT）然后通过二分法继续进行来加快该过程。

根据我的经验，迭代方式比使用量词解决优化问题要快得多。

Answer 2

SoftTimur：由于您的问题涉及整数的非线性算术（在目标函数中），即使您可以解决遇到的其他问题，Z3 也可能会对您的问题做出“未知”响应。非线性整数算术是不可判定的，Z3 中的当前求解器不太可能在存在量词的情况下有效地处理您的问题。 （当然，了不起的 Z3 人员可以“正确”地调整他们的求解器来解决这个特定问题，但不确定性问题仍然普遍存在。）即使你没有任何非线性构造，量词也是你的软肋SMT 求解器，您不太可能使用量化方法走多远。

因此，您基本上只剩下 Philippe 使用迭代的想法。然而，我想强调的是，这两种方法（迭代与量化）是不等价的！从理论上讲，量化的方法更强大。例如，如果您要求 Z3 给您最大的整数值（一个简单的最大化问题，其中成本是整数本身的值），它会正确地告诉您不存在这样的整数。但是，如果您遵循迭代方法，您将永远循环。通常，在优化问题没有全局最大值/最小值的情况下，迭代方法将失败。理想情况下，基于量词的方法可以处理此类情况，但它会受到您自己观察到的其他限制。

与 Z3（以及一般的 SMT 求解器）一样出色，使用 SMT-Lib 对其进行编程有点痛苦。这就是为什么许多人正在构建更易于使用的界面。例如，如果您愿意使用 Haskell，您可以尝试使用 SBV 绑定，它可以让您从 Haskell 编写 Z3 脚本。事实上，我已经在 Haskell 中编写了你的​​问题：http://gist.github.com/1485092。 （请记住，我可能误解了您的 SMTLib 代码，或者可能犯了编码错误，所以请仔细检查。）

Haskell 的 SBV 库支持量化和迭代优化方法。当我尝试使用量词 z3 时，Z3 确实返回“未知”，这意味着问题无法确定。 （参见程序中的函数“test1”。）当我尝试迭代版本时（参见函数“test2”），它不断寻找更好的解决方案，大约10分钟后我将其杀死，找到了以下解决方案：

*** Round 3128 ****************************
*** Solution: [4,42399,-1,0]
*** Value   : 42395 :: SInteger

您是否碰巧知道您的问题的这个特定实例是否真的有最佳解决方案？如果是这样，你可以让程序运行更长的时间，它最终会找到它，否则它会永远运行。

如果您选择探索 Haskell 路径以及遇到任何问题，请告诉我。