求解带量词的实变量存在性问题：Z3返回unsat的解决方法与替代工具

我正在尝试验证一个实变量的量化公式，形式如下：

Exists p . ForAll x != 0 . f(x, p) > 0 and g(x, p) < 0

按照相关建议，我把下面的公式列表提交给了Z3求解器：

[ForAll([x0, x1], Implies(Or(x0 != 0, x1 != 0), And(P0*x0*x0 + P1*x0*x1 + P2*x0*x1 + P3*x1*x1 > 0, -2*P0*x0*x1 + P1*x0*x0 - P1*x0*x1 - P1*x1*x1 + P2*x0*x0 - P2*x0*x1 - P2*x1*x1 + 2*P3*x0*x1 - 2*P3*x1*x1 < 0 ) ) ) ]

但求解器返回了unsat，可实际上存在一个可行解：P=[[1.5, -0.5], [-0.5, 1]]，代入后得到的公式完全满足要求：

And(3/2*x0*x0 - 1*x0*x1 + x1*x1 > 0, -1*x0*x0 - 1*x1*x1 < 0)

我现在有两个疑问：

• 怎么才能计算得到这样的可行解p？
• 如果Z3不太适合处理这类问题，有没有其他可以替代的工具？

内容的提问来源于stack exchange，提问作者nyuw