滿足Tseitin編碼模型

我在z3 4.0中使用以下代碼片段將公式轉換爲CNF。滿足Tseitin編碼模型

(set-logic QF_UF) 
(
    set-option 
    :produce-models 
    true 
) 

; ------ snip ------- 
; 
; declarations, 
; and assert statement 
; of "original" formula 
; here. 
; 
; ------ snap ------- 

(
    apply 
    (
    then 
    (
     ! 
     simplify 
     :elim-and 
     true 
    ) 
    tseitin-cnf 
) 
)

我得到類似如下：

(goals 
(goal 

    ; ------ snip ------- 
    ; 
    ; Lot's of lines here 
    ; 
    ; ------ snap ------- 

    :precision precise :depth 2) 
)

我假定每個跟隨goal表達的是CNF的一個條款，即所有這些表述應聯體，產生實際公式。我將這個連接詞稱爲「編碼」公式。

顯然，原始公式和編碼公式並不相同，因爲編碼公式包含進行Tseitin編碼的新變量k!0, k!1, ...。但是，我期待他們是可以等價的，或者實際上他們是通過相同的模型滿足的（當忽視變量k!i時）。

也就是說，我期待(encoded formula) AND (NOT original formula)是不可滿足的。不幸的是，這似乎並非如此;我有一個反例，其中檢查實際上返回sat。

這是一個在z3中的錯誤，我使用它是錯誤的，還是我的任何假設無效？

來源

2012-06-18 Georg

這可能是一個錯誤。你能否在某個地方發佈這個例子？沒有看到整個例子，很難看到發生了什麼。 –

這是新的tseitin-cnf策略中的一個錯誤。我修復了這個錯誤，並在下一個版本（Z3 4.1）中提供修復。同時，您可以通過使用簡化操作來解決錯誤。也就是說，使用

(apply 
    (then (! simplify :elim-and true) 
      (! simplify :elim-and true) 
      tseitin-cnf))

，而不是

(apply 
    (then (! simplify :elim-and true) 
      tseitin-cnf))

來源

2012-06-19 20:04:32

滿足Tseitin編碼模型

回答

相關問題