Tseitin 인코딩에서 모델 만족

Question

z3 4.0에서 다음 코드를 사용하여 수식을 CNF로 변환했습니다.

(goals 
(goal 

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

    :precision precise :depth 2) 
) 

내가 goal 다음에 표현의 각각 CNF의 한 절입니다 즉, 모든 표현이를 산출하기 위해 conjuncted해야 가정 하였다

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

나는 다음과 같은 무언가를 얻을 실제 공식. 이 연결을 "인코딩 된"수식이라고합니다.

명백히 원래 공식과 인코딩 된 공식은 동일하지 않습니다. 인코딩 된 공식에 Tseitin 인코딩을 수행하는 새로운 변수 k!0, k!1, ...이 포함되어 있기 때문입니다. 그러나, 나는 그들이 동등한, 또는 실제로 그들은 같은 모델 (k!i 변수를 무시)에 의해 만족하고 있다고 기대했다.

즉, 나는 (encoded formula) AND (NOT original formula)이 만족스럽지 않을 것으로 기대하고 있었다. 불행하게도 이것은 사실이 아닌 것 같습니다. 이 수표가 실제로 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))