Z3モデルが正しくない

Question

私は、無向グラフでハミルトニアンサイクルを見つける問題をハッキングしています。しかし、最近の実験では、不可能なモデルでなければならないものが作られました。

sat 
(model 
    (define-fun e2() Bool 
    true) 
    (define-fun e5() Bool 
    true) 
    (define-fun e3() Bool 
    true) 
    (define-fun e4() Bool 
    true) 
    (define-fun e1() Bool 
    true) 
    (define-fun v3() Bool 
    true) 
    (define-fun v2() Bool 
    true) 
    (define-fun v1() Bool 
    true) 
    (define-fun v0() Bool 
    true) 
) 

：ここ

;number of vertices = 4 
;5 edges: 
;e1 = 0 1 
;e2 = 1 2 
;e3 = 2 3 
;e4 = 3 0 
;e5 = 1 3 

(declare-const v0 Bool) 
(declare-const v1 Bool) 
(declare-const v2 Bool) 
(declare-const v3 Bool) 

(declare-const e1 Bool) 
(declare-const e2 Bool) 
(declare-const e3 Bool) 
(declare-const e4 Bool) 
(declare-const e5 Bool) 

(assert (xor (and e2 e3 e4 e5) (and e1 e3 e4 e5) (and e1 e2 e4 e5) (and e1 e2 e3 e5) (and e1 e2 e3 e4))) 

(assert (and v0 v1 v2 v3)) 

;(assert (=> (and e2 e3 e4 e5) (and v0 v1 v2 v3))) 
;(assert (=> (and e1 e3 e4 e5) (and v0 v1 v2 v3))) 
;(assert (=> (and e1 e2 e4 e5) (and v0 v1 v2 v3))) 
;(assert (=> (and e1 e2 e3 e5) (and v0 v1 v2 v3))) 
;(assert (=> (and e1 e2 e3 e4) (and v0 v1 v2 v3))) 

(assert (=> e1 (or e2 e4 e5))) 
(assert (=> e2 (or e1 e3 e5))) 
(assert (=> e3 (or e2 e4 e5))) 
(assert (=> e4 (or e1 e3 e5))) 
(assert (=> e5 (or e1 e2 e4))) 

(assert (and (=> e1 e2) (=> e2 e3) (=> e3 e4) (=> e4 e1))) 

(check-sat) 
(get-model) 

E1、E2、E3、E4、およびE5のすべてを示す出力は、これを具体的に禁止入力でXOR声明にもかかわらず、真であるとされています。ここで入力されています

ここで何がうまくいかないのか誰にも意見はありますか？

よろしくお願いいたします。

Answer 1

あなたは何をしようとしているのかわかりませんが、あなたはxorを誤用したようです。

(simplify (xor true true true true true))がtrueを返すので、あなたのエンコーディングは現在のモデルを禁止していません。一般的に

、次のようにa1、a2とa3が、あなたは正確に一つの真行うことができました保証する：

(assert (or a1 a2 a3)) ; at least one true 
(assert (and (=> a1 (and (not a2) (not a3))) 
      (=> a2 (and (not a1) (not a3))) 
      (=> a3 (and (not a1) (not a2))))); at most one true