不能令人滿意的模型的性能問題

Question

我正在使用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：>15米（中止）

如果我從int轉換到大小64 bitvectors，表現得更好一點，但似乎仍然指數：

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

奇怪的是，長度爲10的只需要2m34.197s。 如果我切換到較小尺寸的位向量，性能會稍微好一些，但仍然是指數級的。

所以我的問題是：這是預期？有沒有更好的方式來制定這種「無環」限制？

Answer 1

你的公式本質上是編碼的「鴿子洞」問題。 您有sz+1孔（值爲0,1，...，sz）和sz+2鴿子（陣列單元格(select tpath 0)，...，(select tpath (+ sz 1))）。 你第一個量詞是說每隻鴿子都應該放在其中一個洞裏。 第二個是說兩隻不同的鴿子不應該在同一個洞裏。

「鴿子洞」問題沒有多項式尺寸分辨率證明。因此，預計運行時間呈指數級增長。 請注意，任何基於分辨率，DPLL或CDCL的SAT解算器都會在鴿子洞問題上表現不佳。

使用位向量時性能會更好，因爲Z3會將它們降低爲命題邏輯，並且案例分析很多在這個級別更有效率。

順便說一句，你使用量詞來編碼參數問題。 這是一個優雅的解決方案，但它不是Z3最有效的方法。 對於Z3，一般來說，最好斷言「擴展的」量詞免費問題。 但是，對於您的問題中描述的問題，它不會有很大的區別，因爲您仍然會經歷指數增長。

Answer 2

就像萊昂納多所說的那樣，由於鴿子洞問題本質上是指數級的，因此最終的表現將會變壞。你可能做的唯一事情就是推遲性能下降的時間。既然你已經嘗試了位向量，我的建議是嘗試將問題轉換爲Leonardo建議的無量詞問題，因爲問題的大小是預定義的，並嘗試使用一些策略。