模型无法满足的性能问题
我正在使用 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。 如果我切换到较小尺寸的位向量，性能会变得更好一些，但仍然是指数级的。
所以我的问题是：这是可以预料的吗？有没有更好的方法来制定这种“无循环”约束？
I'm using Z3 to construct a bounded model-checker. I'm running into a strange performance problem when trying to implement a completeness test. The completeness test has to make sure that all states that every path contains each state at most once. If there are still paths which fulfill this property, Z3 is quick with an answer, however in the case where all paths have been considered, Z3 seems to be exponentially slow.
I've reduced my test-case to the following:
; 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)
On my computer this results in the following running times (depending on path length):
- 3: 0.057s
- 4: 0.561s
- 5: 42.602s
- 6: >15m (aborted)
If I switch from Int to bitvectors of size 64, the performance gets a little better, but still seems exponential:
- 3: 0.035s
- 4: 0.053s
- 5: 0.061s
- 6: 0.106s
- 7: 0.467s
- 8: 1.809s
- 9: 2m49.074s
Strangely enough, for a length of 10 it only takes 2m34.197s.
If I switch to bitvectors of smaller size, the performance gets a little better, but is still exponential.
So my question is: Is this to be expected? Is there a better way to formulate this "loop-free" constraint?
如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
发布评论
评论（2）
你的公式本质上是在编码“鸽子洞”问题。
您有
sz+1个洞（值 0、1、...、sz）和sz+2鸽子（数组单元格（选择 tpath 0），...，<代码>（选择tpath（+ sz 1）））。第一个量词指出每只鸽子都应该放入其中一个洞中。
第二条规定两只不同的鸽子不应该在同一个洞里。
对于“鸽子洞”问题，没有多项式大小分辨率的证明。
因此，预计运行时间呈指数增长。
请注意，任何基于分辨率、DPLL 或 CDCL 的 SAT 求解器在处理鸽子洞问题时都会表现不佳。
使用位向量时可以获得更好的性能，因为 Z3 将它们简化为命题逻辑，并且案例分析在该级别上效率更高。
顺便说一句，您正在使用量词来编码参数问题。
这是一个优雅的解决方案，但对于 Z3 来说并不是最有效的方法。
对于 Z3，一般来说，最好断言“扩展”量词自由问题。
但是，对于您问题中描述的问题，这不会产生太大的影响，因为您仍然会经历指数增长。
Your formula is essentially encoding the “pigeon-hole” problem.
You have
sz+1holes (the values 0, 1, …, sz) andsz+2pigeons (the array cells(select tpath 0), …,(select tpath (+ sz 1))).You first quantifier is stating that each pigeon should be put in one of the holes.
The second is stating that two different pigeons should not be in the same hole.
There is no polynomial size resolution proof for the “pigeon-hole” problem.
So, the exponential growth in run time is expected.
Note that any SAT solver based on resolution, DPLL, or CDCL will perform badly on the pigeon-hole problem..
You get better performance when using bit-vectors because Z3 reduces them to propositional logic and case analysis is much more efficient at that level.
BTW, you are using quantifiers for encoding parametric problems.
That is an elegant solution, but it is not the most efficient approach for Z3.
For Z3, in general, it is better to assert the 'expanded' quantifier free problem.
However, for the problem described in your question, it will not make a big difference, since you will still experience the exponential growth.
正如莱昂纳多所说，由于鸽笼问题本质上是指数级的，所以性能最终会变差。您可能唯一能做的就是推迟性能变差的时间。既然您已经尝试过位向量，我的建议是尝试将问题转换为莱昂纳多建议的无量词问题，假设问题大小是预先定义的，并尝试使用一些策略。
Just like what Leonardo said, since the pigeon-hole problem is exponential in nature, the performance will go bad eventually whatsoever. The only thing you could probably do is to postpone the time the performance goes bad. Since you have tried bit-vector, my suggestions are try converting the problem into quantifier-free problem as suggested by Leonardo, given that the problem size is pre-defined, and try using some tactics.