CODEWITHSUNDEEP
z3
Schemer
Schemer

Reputation: 1665

Z3 Model Incorrect

I am hacking away at the problem of finding a Hamiltonian cycle in an undirected graph. But a recent experiment produced what should have been an impossible model. Here is the input:

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

Here is the output showing all of e1, e2, e3, e4, and e5 to be true despite the xor statement in the input that specifically prohibits this:

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

Does anyone have any opinions on what's going wrong here?

Regards.

Upvotes: 1

Views: 241

Answers (1)

pad
pad

Reputation: 41290

I don't know what you're trying to do, but it seems that you misused xor.

Since (simplify (xor true true true true true)) returns true, your encoding doesn't prohibit the current model.

In general, to guarantee a1, a2 and a3 has exactly one true, you could do as follows:

(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

Upvotes: 2

Related Questions