查找可能的值

Question

我要验证表格的公式：

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

所有变量都是实数。

按照here 的建议，我将此列表添加到求解器中：

[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很难，有没有办法解决这个问题？

Answer 1

当您说“Exists”后跟“Forall”时，您是在说该公式对于每个 x0、x1 都应该是正确的。 Z3 告诉你，事实并非如此。

如果您有兴趣找到一个这样的P 和相应的x 值，只需删除量化并将所有内容都设为*变量：

from z3 import *

def f(x0, x1, P0, P1, P2, P3):
    return P0*x0*x0 + P1*x0*x1 + P2*x0*x1 + P3*x1*x1

def g(x0, x1, P0, P1, P2, P3):
    return -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

p0, p1, p2, p3  = Reals('p0 p1 p2 p3')

x0, x1 = Reals('x0 x1')
fmls = [Implies(Or(x0 != 0, x1 != 0), And(f(x0, x1, p0, p1, p2, p3) > 0, g(x0, x1, p0, p1, p2, p3) < 0))]

while True:
    s = Solver()
    s.add(fmls)
    res = s.check()
    print res
    if res == sat:
        m = s.model()
        print m
        fmls += [Or(p0 != m[p0], p1 != m[p1])]
    else:
       print "giving up"
       break

当我运行它时，我得到：

sat
[x0 = 1/8, p0 = -1/2, p1 = -1/2, x1 = 1/2, p2 = 1, p3 = 1]

还有很多其他的；这就是我相信你所追求的。

请注意，您还可以根据您所在的位置进行一些编程来摆脱存在量化；即，从量化版本开始，如果您收到unsat，则切换到新的求解器并使用未量化版本来自动化此过程。当然，这只是编程，目前与 z3 没有任何关系。