3

我正在使用 Z3 构建有界模型检查器。在尝试实施完整性测试时，我遇到了一个奇怪的性能问题。完整性测试必须确保所有状态，每条路径最多包含每个状态一次。如果仍有满足此属性的路径，则 Z3 很快就会给出答案，但是在考虑了所有路径的情况下，Z3 似乎呈指数级缓慢。

我已将测试用例简化为以下内容：

; Set the problem size (length of path)
(define-fun sz () Int 5)

; Used to define valid states
(define-fun limit ((s Int)) Bool
  (and (>= s 0)
       (<= s sz)))

; Constructs a path of a given length
(define-fun path-of-len ((path (Array Int Int)) (len Int)) Bool
  (forall ((i Int))
          (=> (and (>= i 0)
                   (< i len))
          (limit (select path i)))))

; Asserts that a given path only contains unique states
(define-fun loop-free ((path (Array Int Int)) (len Int)) Bool
  (forall ((i Int) (j Int))
          (=> (and (>= i 0)
                   (>= j 0)
                   (< i len)
                   (< j len)
                   (not (= i j)))
              (not (= (select path i) (select path j))))))

; Construct a unique path of a given length
(define-fun path ((path (Array Int Int)) (len Int)) Bool
  (and (path-of-len path len)
       (loop-free path len)))

; Declare a concrete path
(declare-const tpath (Array Int Int))

; Assert that the path is loop free
(assert (path tpath (+ sz 2)))

(check-sat)

在我的计算机上，这会导致以下运行时间（取决于路径长度）：

  • 3：0.057s
  • 4：0.561s
  • 5：42.602s
  • 6：>15m（中止）

如果我从 Int 切换到大小为 64 的位向量，性能会稍微好一些，但似乎仍然呈指数级：

  • 3：0.035s
  • 4：0.053s
  • 5：0.061s
  • 6：0.106s
  • 7：0.467s
  • 8：1.809s
  • 9：2m49.074s

奇怪的是，长度为 10 只需要 2m34.197s。如果我切换到更小尺寸的位向量，性能会好一点，但仍然是指数级的。

所以我的问题是：这是可以预料的吗？有没有更好的方法来制定这种“无循环”约束？

4

2 回答 2

1

您的公式本质上是对“鸽子洞”问题的编码。您有sz+1孔（值 0、1、...、sz）和sz+2鸽子（数组单元格(select tpath 0)、...、... (select tpath (+ sz 1))）。你的第一个量词是说每只鸽子都应该放在一个洞里。第二个是说明两只不同的鸽子不应该在同一个洞里。

“鸽子洞”问题没有多项式大小分辨率证明。因此，预计运行时间会呈指数增长。请注意，任何基于分辨率、DPLL 或 CDCL 的 SAT 求解器都将在鸽子洞问题上表现不佳。

使用位向量时可以获得更好的性能，因为 Z3 将它们简化为命题逻辑，并且案例分析在该级别上更加有效。

顺便说一句，您正在使用量词来编码参数问题。这是一个优雅的解决方案，但它不是 Z3 最有效的方法。对于 Z3，一般来说，最好断言“扩展的”无量词问题。但是，对于您的问题中描述的问题，它不会有太大的不同，因为您仍然会经历指数增长。

于 2011-10-27T16:52:46.097 回答
0

就像莱昂纳多所说的那样，由于鸽子洞问题本质上是指数级的，所以性能最终会变差。您可能唯一能做的就是推迟性能变差的时间。由于您已经尝试过位向量，我的建议是尝试按照 Leonardo 的建议将问题转换为无量词问题，因为问题大小是预先定义的，并尝试使用一些策略。

于 2015-08-12T04:29:55.620 回答