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)
)

私は、それに続く式のそれぞれがgoalCNF の 1 つの節であると想定していました。つまり、これらすべての式を結合して、実際の式を生成する必要があります。この結合を「エンコードされた」式と呼びます。

明らかに、元の式とエンコードされた式は同等ではありません。エンコードされた式に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 に答える