ctx-solver-simplify中的非對稱行爲

我從ctx-solver-simplify看到了相當令人驚訝的行爲，其中使用來自https://git01.codeplex.com/z3（89c1785b）主分支的最新Z3版本的參數順序到z3.And（）似乎很重要）：ctx-solver-simplify中的非對稱行爲

#!/usr/bin/python 
import z3 

a, b = z3.Bools('a b') 
p = z3.Not(a) 
q = z3.Or(a, b) 
for e in z3.And(p, q), z3.And(q, p): 
    print e, '->', z3.Tactic('ctx-solver-simplify')(e)

生產：

And(Not(a), Or(a, b)) -> [[Not(a), Or(a, b)]] 
And(Or(a, b), Not(a)) -> [[b, Not(a)]]

這是在Z3的錯誤嗎？

來源

2012-11-29 user1861926

不，這不是一個錯誤。戰術ctx-solver-simplify是非常昂貴的和固有的不對稱。也就是說，訪問子公式的順序會影響最終結果。這種策略在文件src/smt/tactic/ctx_solver_simplify_tactic.cpp中實現。代碼很可讀。請注意，它使用「SMT」解算器（m_solver），並在遍歷輸入公式時對m_solver.check()進行多次調用。這些電話中的每一個都可能非常昂貴。對於特定的問題領域，我們可以實施一個更加昂貴的策略版本，並避免您的問題中描述的不對稱。

編輯：

您也可以考慮戰術ctx-simplify，它比ctx-solver-simplify便宜，但它是對稱的。戰術ctx-simplify將主要適用規則，如：

A \/ F[A] ==> A \/ F[false] 
x != c \/ F[x] ==> F[c]

哪裏F[A]是可能包含A公式。它比ctx-solver-simplify便宜，因爲它在遍歷公式時不會調用SMT解算器。下面是一個使用這種戰術（也可online）爲例：

a, b = Bools('a b') 
p = Not(a) 
q = Or(a, b) 
c = Bool('c') 
t = Then('simplify', 'propagate-values', 'ctx-simplify') 
for e in Or(c, And(p, q)), Or(c, And(q, p)): 
    print e, '->', t(e)

關於humand可讀性，執行任何戰術的時候，這是從來沒有一個進球。請告訴我們，上述策略是否不足以達到您的目的。

來源

2012-11-29 07:54:51

謝謝！如果我想生成一個公式的簡潔易讀的版本，並且計算時間不那麼重要，那麼我是否可以在Z3中調用API或策略來「更加努力」來簡化表達式？或者我需要修改ctx_solver_simplify_tactic.cpp /寫我自己的戰術？ – user1861926

事實上，'propagate-values'對我有很大幫助 - 再次感謝！ – user1861926

我認爲寫一個自定義策略會更好，因爲當你基本上要求正規性時，還有其他的折衷。 Z3沒有任何將公式轉換爲規範形式的策略。所以，如果你想要的東西總是產生相同的答案公式是地面等值，你將不得不寫一個新的規範，確保這一點。

在簡化公式時，ctx_solver_simplify_tactic還會進行一些折衷：它避免了多次簡化相同的子公式。如果是這樣，它可能會顯着增加結果公式的大小（按指數規律）。

來源

2012-11-29 16:18:24

ctx-solver-simplify中的非對稱行爲

回答

相關問題