z3「超過」完全有序的關係

我想創建一個SMT序列，以便我有一個完整的排序順序。z3「超過」完全有序的關係

例1： a < b和b < c應滿足的

例2： a < b和c < d應該是不可滿足。通過添加b < c我們會得到滿足。

有沒有人有任何想法，如果這一般甚至可能？到目前爲止，我嘗試了以下內容：

(declare-fun my_rel (Int Int) (Bool)) 
(assert (forall ((i Int)(j Int)) (implies (my_rel i j) (> i j)))) 
(declare-const a Int) 
(declare-const b Int) 
(declare-const c Int) 
(declare-const d Int) 
(assert (my_rel a b)) 
(assert (my_rel c d)) 
(check-sat)

這應返回UNSAT。通過增加(assert (my_rel b c))它應該滿足。

來源

2014-09-23 paubo147

我相信你想要的是一種方法來檢查一個有限的元素集合x_1 ... x_n上的傳遞順序是否必須是或需要完成並且是全部的，因爲一組用戶斷言P關於訂購。

<關係似乎在您的示例中是隱式傳遞的。將隱式傳遞的二元關係一起破解的簡單方法是使用未解釋的函數將任意任意域嵌入到完全排序的解釋域中。確保爲此目的添加的未解釋函數僅出現在「嵌入到訂單中」的含義中。

(declare-fun foo (U) (Int)) 
(define-fun my_rel_strict ((i U) (j U)) (Bool) (> (foo i) (foo j))) 
(define-fun my_rel_nonstrict ((i U) (j U)) (Bool) 
    (or (= (foo i) (foo j)) (my_rel_strict i j))

兩者my_rel關係將傳遞性和my_rel_strict具有的全部條件（或者（my_real_nonstrict I J）或（my_rel_nonstrictĴi）持有）。（請參見http://en.wikipedia.org/wiki/Total_order）因爲my_rel不具有反對稱性，所以它們也不是總的順序。爲了避免潛在的問題，域的基數應該至少是共域（或兩者都是無限的）。（my_rel_nonstrict的編碼不是很好，我會嘗試< =在實際中。）

接下來我相信你想要的是一個包含檢查。給定一組斷言P，用戶是否定義了傳遞順序（我現在寫爲<）必須是總數？我們發明一個公式：總（X_1 ... x_n）爲一組有限的元素：

total(x_1 ... x_n) = (and_{for all i,j} (or (< x_i x_j) (= x_i x_j) (> x_i x_j)))

（不是總的非常愉快的編碼，但編碼都是一樣的。）要檢查將P需要總（ ...），我們用下面的查詢smt求解器：

(assert P) (assert (not total(...))) 
; You may also need (assert (distinct x_1 ... x_n))

如果不可滿足，則包含成立。如果它是可以滿足的，那麼蘊含有一個反例，並不成立。

訂單可能會很難編碼，所以我的建議可能不適用於您的應用程序。（同樣用上一粒鹽，我不是百分之百的。）

來源

2014-09-24 13:18:59 Tim

z3「超過」完全有序的關係

回答

相關問題