z3 - Tseitin 编码下的令人满意的模型

Question

我在 z3 4.0 中使用以下代码片段将公式转换为 CNF。

(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 的一个子句，即所有这些表达式都应该连接起来以产生实际的公式。我将把这个连词称为“编码”公式。

显然，原始公式和编码公式并不等价，因为编码公式包含新变量k!0, k!1, ...，这些变量进行 Tseitin 编码。然而，我期望它们是可等满足的，或者实际上它们满足相同的模型(当忽略 k!i 变量时)。

即，我期望 (编码公式) AND (不是原始公式) 是不可满足的。不幸的是，情况似乎并非如此。我有一个反例，该检查实际上返回 sat。

这是 z3 中的错误吗？我是否使用错误，或者我的任何假设无效？

Answer 1

这是新的 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))