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 回答