0
解決策は存在しますが、z3はUNSATです。z3はUNSATを間違って言っています
(set-logic QF_UFNRA)
(declare-fun a() Real)
(declare-fun b() Real)
(declare-fun c() Real)
(declare-fun d() Real)
(declare-fun e() Real)
(declare-fun f() Real)
(declare-fun g() Real)
(declare-fun h() Real)
(assert (and (<= a 1.0) (> a 0.0)))
(assert (and (<= b 1.0) (> b 0.0)))
(assert (and (<= c 1.0) (> c 0.0)))
(assert (and (<= d 1.0) (> d 0.0)))
(assert (and (<= e 1.0) (>= e 0.0)))
(assert (and (<= f 1.0) (>= f 0.0)))
(assert (and (<= g 1.0) (>= g 0.0)))
(assert (and (<= h 1.0) (>= h 0.0)))
(assert (= (* (+ a b) (+ a c)) a))
(assert (= (* (+ a b) (+ b d)) b))
(assert (= (* (+ a c) (+ c d)) c))
(assert (= (* (+ b d) (+ c d)) d))
(assert (= (+ a b c d e f g h) 1.0))
(check-sat)
有効な解決策:
a = 1/12, b = 1/4, c = 1/6, d = 1/2, e = f = g = h = 0
私はZ3はUNSAT言う理由を把握することはできませんよ。
z3バージョンはz3-4.3.0-x64です。
githubの最新バージョンも正解です。私はバグが4.3.0バージョンから修正されたと思います。 – Logan