1

我有一个代码z3，旨在解决布尔公式的优化问题

(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个警告，最终结果是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`.

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

4

2 回答 2

3

我已经通过以下迭代方式解决了 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是您的最大值。如果不是，请使用新解决方案 asv0并返回第 3 点。

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

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

于 2011-12-15T18:53:10.240 回答
3

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 路径以及您有任何问题，请告诉我。

于 2011-12-16T08:47:19.193 回答