1

無向グラフでハミルトン閉路を見つける問題をハッキングしています。しかし、最近の実験では、不可能なモデルになるはずだったものが作成されました。入力は次のとおりです。

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

入力の xor ステートメントが明確にこれを禁止しているにもかかわらず、e1、e2、e3、e4、および e5 のすべてが true であることを示す出力を次に示します。

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

ここで何がうまくいかないかについて誰か意見がありますか？

よろしく。

4

1 に答える 1

2

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

(simplify (xor true true true true true))を返すためtrue、エンコーディングは現在のモデルを禁止していません。

一般に、を保証するa1には、次のようにします。a2a3

(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
于 2012-02-02T10:59:12.027 に答える