时间戳

首页 > 解决方案 > 量词中的非零向量

z3 - 量词中的非零向量

问题描述

我想验证以下形式的公式：

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.

标签： z3solverz3py

解决方案

跟进 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

推荐阅读