具有 forall 量词的公式的可满足性

Question

这是我的 Python 代码：

s = z3.Solver()

f = z3.Function('f', z3.IntSort(), z3.IntSort())
g = z3.Function('g', z3.IntSort(), z3.IntSort())
h = z3.Function('h', z3.IntSort(), z3.IntSort())

a, b, c = z3.Ints('a b c')

imp_a = z3.And(f(a) == b, g(a) == c)
imp_b = h(c) == b
ax = z3.ForAll(a, z3.Implies(imp_a, imp_b))

l = [
    ax,
    f(1) == 5,
    g(1) == 2,
    h(2) != 5
]
s.add(l)

if s.check() == z3.sat:
    print s.model()
else:
    print 'Unsat'

在这段代码中，我用 Z3Py 语法编写了以下公式：

forall a, (f(a) == b and g(a) == c) => h(c) == b

当我运行这个脚本找到一个模型时，我认为它应该是 unsat。怎么可能？我错过了什么吗？

Answer 1

您忘记绑定 b 和 c:

ax = z3.ForAll([a,b,c], z3.Implies(imp_a, imp_b))

绑定b、c后，则结果为unsat。如果你不绑定b,c，那么它们就被当作自由常量，并且有公式的模型。

具有 forall 量词的公式的可满足性

Satisfiability of a formula having forall quantifier

python

z3

smt

z3py

first-order-logic