代码之家 › 专栏 › 技术社区 › nyuw

量词中的非零向量

z3py solver z3

nyuw · 技术社区 · 6 年前

我想验证以下表单的公式:

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

实现(不起作用)如下所示:

def f0(x0, x1, x, y):
    return x1 ** 2 * y + x0 ** 2 * x

s = Solver()
x0, x1 = Reals('x0 x1')
p0, p1 = Reals('p0 p1')

s.add(Exists([p0, p1], 
                ForAll([x0, x1], 
                          f0(x0, x1, p0, p1) > 0
                      )
            ))
#s.add(Or(x0 != 0, x1 != 0))

while s.check() == sat:
    m = s.model()
    m.evaluate(x0, model_completion=True)
    m.evaluate(x1, model_completion=True)
    m.evaluate(p0, model_completion=True)
    m.evaluate(p1, model_completion=True)
    print m
    s.add(Or(x0 != m[x0], x1 != m[x1]))

公式不满足要求。

具有 f0() >= 0 ,唯一的输出是 (0, 0) 。

我想要 f0() > 0 和约束 (x0, x1) != (0, 0) 。

我所期望的是: p0, p1 = 1, 1 或 2, 2 例如,但我不知道如何删除 0, 0 从可能的值 x0, x1 。

2 回复 | 直到 6 年前

Nikolaj Bjorner 6 年前

跟进Levent的回复。在第一次检查期间,Z3使用与量词一起使用的自定义决策过程。在增量模式下,它会退回到非决策过程的状态。要强制单发解算器,请尝试以下操作:

from z3 import *

def f0(x0, x1, x, y):
    return x1 * x1 * y + x0 * x0 * x

p0, p1 = Reals('p0 p1')

x0, x1 = Reals('x0 x1')
fmls = [ForAll([x0, x1], Implies(Or(x0 != 0, x1 != 0), f0(x0, x1, p0, p1) > 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

alias 6 年前

你可以简单地把它写在量化中作为一种暗示。我想你也把其中的一些变量弄混了。以下内容似乎抓住了您的意图:

from z3 import *

def f0(x0, x1, x, y):
    return x1 * x1 * y + x0 * x0 * x

s = Solver()
p0, p1 = Reals('p0 p1')

x0, x1 = Reals('x0 x1')
s.add(ForAll([x0, x1], Implies(Or(x0 != 0, x1 != 0), f0(x0, x1, p0, p1) > 0)))

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

当然,z3不能保证为您找到任何解决方案;尽管它似乎可以做到:

$ python a.py
sat
[p1 = 1, p0 = 1]
unknown
giving up

一旦你使用了量词,所有的赌注都被取消了,因为逻辑变得半决定性。Z3在这里做得很好,返回了一个解决方案,然后就放弃了。我认为,除非您使用一些定制的决策程序,否则您不会期望有更好的结果。