Z3行爲改變要求對造成不滿意的核心

我有幾個SMTLIB2實例Z3通常認爲不飽和度在幾十毫秒內自動，然而，當我在請求添加爲它產生不飽和度核心，退房SAT保持持續幾分鐘無返回。這是行爲嗎？請求不飽和內核做的不僅僅是開啓儀器記錄依賴關係，還要更改z3運行的過程和選項？是否有可能設置更多的選項，以便我在使用未核心代時看到相同的行爲，因爲我在不使用它時會看到這種情況？Z3行爲改變要求對造成不滿意的核心

我對科學的Linux 6.3採用Z3 4.3.1（穩定分支）。

的例子在AUFNIRA，雖然一些不涉及實數，可能不是非線性的。

謝謝，

保羅。

來源

2013-02-21 Paul Jackson

的不飽和度核使用的「答案文字」（又名假設）跟蹤。當我們使不飽和度核心的提取和使用斷言，如

(assert (! (= x 10) :named a1))

Z3將在內部創建的名稱a1新鮮布爾變量，並斷言

(assert (=> a1 (= x 10)))

時，check-sat被調用時，它假定所有這些輔助變量是真實的。也就是說，Z3試圖表明這個問題不符合這些假設。對於可滿足的情況，它將像往常一樣終止模型。對於不可滿足的實例，只要它生成只包含這些假定的布爾變量的引理就會終止。外稃是形式(or (not a_i1) ... (not a_in))的其中a_i的是假設的布爾變量的子集。據我所知，這種技術已被MiniSAT求解器引入。它被描述爲here（第3節）。我非常喜歡它，因爲它很容易實現，我們基本上沒有免費的核心代。

然而，這種方法也有一些缺點。首先，一些預處理步驟不再適用。如果我們只是斷言

(assert (= x 10))

Z3將取代x與10無處不在。我們說Z3正在進行「價值傳播」。如果斷言是這僅僅是一個例子，許多其它預處理步驟受影響的形式

(assert (=> a1 (= x 10)))

的不施加此預處理步驟。在解決時間過程中，某些簡化步驟也被禁用。如果我們檢查Z3源文件smt_context.cpp我們會發現這樣的代碼：當「答案文字」 /使用的假設

void context::simplify_clauses() { 
     // Remark: when assumptions are used m_scope_lvl >= m_search_lvl > m_base_lvl. Therefore, no simplification is performed. 
     if (m_scope_lvl > m_base_lvl) 
      return; 
     ... 
    }

條件m_scope_lvl > m_base_lvl)始終爲真。因此，當我們啓用不可靠的核心代時，我們可能真的會影響性能。看來沒有什麼是免費的:)

來源

2013-02-21 19:36:56

Z3行爲改變要求對造成不滿意的核心

回答

相關問題