Z3의 버그입니까? Real 및 ForAll에 대한 잘못된 대답이 적용되었습니다.

Question

포물선 y = (x + 2) ** 2-3의 최소값을 찾으려고합니다. 분명히 대답은 y == - 3, x == 일 것입니다. -2. 그러나 z3은 ForAll 어설 션을 충족시키지 않는 [x = 0, y = 1] 응답을 제공합니다.

내가 잘못 생각하나요?

from z3 import * 

x, y, z = Reals('x y z') 

print(Tactic('qe').apply(And(y == (x + 2) ** 2 - 3, 
          ForAll([z], y <= (z + 2) ** 2 - 3)))) 

solve(y == x * x + 4 * x +1, 
     ForAll([z], y <= z * z + 4 * z +1)) 

그리고 결과 :

[[y == (x + 2)**2 - 3, True]] 
[x = 0, y = 1] 

결과는 항상 사실이 아니다 있지만, '양적 완화'전술이 참으로 그 FORALL의 주장을 제거 보여줍니다 여기에

는 파이썬 코드입니다. 그 이유는 해답이 잘못된 답을주는 이유입니까? 이러한 표현식의 최소 (또는 최대) 값을 찾으려면 어떻게 코딩해야합니까?

현재, Z3 버전은 Mac의 경우 4.3.2입니다.

Answer 1

How does Z3 handle non-linear integer arithmetic? 을 언급했으며 'qfnra-nlsat'및 'smt'전술을 사용하여 부분적인 해결책을 찾았습니다.

from z3 import * 

x, y, z = Reals('x y z') 

s1 = Then('qfnra-nlsat','smt').solver() 
print s1.check(And(y == (x + 2) ** 2 - 3, 
          ForAll([z], y <= (z + 2) ** 2 - 3))) 
print s1.model() 

s2 = Then('qe', 'qfnra-nlsat','smt').solver() 
print s2.check(And(y == (x + 2) ** 2 - 3, 
          ForAll([z], y <= (z + 2) ** 2 - 3))) 
print s2.model() 

그리고 결과 :

sat 
[x = -2, y = -3] 
sat 
[x = 0, y = 1] 

는 여전히 '양적 완화'전술 기본 해결사가 버그를 보인다. 그들은 올바른 결과를주지 않습니다. 추가 의견 및 토론이 필요합니다.