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)

下面的输出显示所有 e1、e2、e3、e4 和 e5 为真，尽管输入中的 xor 语句明确禁止这样做：

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,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
于 2012-02-02T10:59:12.027 回答