4

我在 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变量时）。

即，我期待这(encoded formula) AND (NOT original formula)是无法满足的。不幸的是，情况似乎并非如此。我有一个反例，该检查实际返回sat。

这是 z3 中的错误，是我使用错误，还是我的任何假设都不成立？

4

1 回答 1

4

这是新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-19T20:04:32.060 回答