如何从z3py计算中获得结果？

Question

我想用z3py来说明以下家谱练习（pa是“父母”，而grpa是“祖父母”]

pa（Rob，Kev）∧pa（Rob，Sama）∧pa（Sama，Tho）∧pa（Dor，Jim）∧pa（Bor，Jim）∧pa（Bor，Eli）∧pa（Jim，Tho） ∧pa（Sama，Samu）∧pa（Jim，Samu）∧pa（Zel，Max）∧pa（Samu，Max）

∀X，Y，Z pa（X，Z）∧pa（Z，Y）→grpa（X，Y）

练习在于找出X的哪个值具有以下值：

∃Xgrpa（Rob，X）∧pa（X，Max）

（（答案是：对于X == Samu。）我想在z3py中重写此问题，因此我引入了一种新的类型Hum（对于“人类”），并编写了以下内容：

import z3

Hum = z3.DeclareSort('Hum')
pa = z3.Function('pa',Hum,Hum,z3.BoolSort())
grpa = z3.Function('grpa',Hum,Hum,z3.BoolSort())
Rob,Kev,Sama,Tho,Dor,Jim,Bor,Eli,Samu,Zel,Max = z3.Consts('Rob Kev Sama Tho Dor Jim Bor Eli Samu Zel Max', Hum)
s=z3.Solver()
for i,j in ((Rob,Kev),(Rob,Sama),(Sama,Tho),(Dor,Jim),(Bor,Jim),(Bor,Eli),(Jim,Tho),(Sama,Samu),(Jim,Samu),(Zel,Max),(Samu,Max)):
    s.add(pa(i,j))
x,y,z=z3.Consts('x y z',Hum)
whi=z3.Const('whi',Hum)
s.add(z3.ForAll([x,y,z],z3.Implies(z3.And(pa(x,z),pa(z,y)),grpa(x,y))))
s.add(z3.Exists(whi,z3.And(grpa(Rob,whi),pa(whi,Max))))

该代码已被Python接受并用于

print(s.check())

我知道

sat

现在我知道有解决方案。问题是：如何获得whi的值？

[当我要求print(s.model()[whi])时，我会得到None。当我要求s.model().evaluate(whi)时会得到whi，这不是很有帮助。

如何获取有关最后一个公式为真的whi必须为Samu的信息？

（（辅助问题：为什么常量和变量之间没有区别？当我将x,y,z定义为常量，尽管它们是变量时，我有点困惑）。为什么我不能写x=Hum('x')来表明x是排序为Hum的变量？）

Answer 1

当您写类似的东西时：

X, Y = Const('X Y', Hum)

它确实是[[not”表示您要声明两个名为X的常量Y和Hum。 （是的，这确实令人困惑！尤其是如果您来自像Prolog这样的背景！）

相反，它的意思是说两个对象X和Y属于类别Hum。它甚至不表示X和Y不同。除非您明确声明，否则它们可能完全相同，如下所示：

s.assert(z3.Distinct([X, Y]))

这也可以解释您对常量和变量的困惑。在您的模型中，一切都是变量。您根本没有声明任何常量。
您关于whi不是Samu的问题的解释有点棘手，但这源于您拥有的全部是变量而根本没有常量的事实。此外，whi当用作量化变量时，在模型中永远不会有值：如果要为变量提供值，则它必须是具有自己的断言的顶级声明变量。这通常会使不熟悉z3py的人们绊倒：对变量进行量化时，顶层声明只是在范围内获取名称的一个绝招，它实际上与量化变量无关。如果您发现这令人困惑，那么您并不孤单：这是一个“骇客”，也许最终比对新手有用而令人困惑。如果您有兴趣，请在此处进行详细说明：https://theory.stanford.edu/~nikolaj/programmingz3.html#sec-quantifiers-and-lambda-binding但是我建议您仅考虑一下绑定变量whi和您在顶层声明的whi只是两个不同的变量。一旦熟悉了z3py的工作原理，就可以查看此hack的详细信息和原因。
回到您的建模问题：您确实希望这些常量出现在模型中。尤其要说的是，这些人是我宇宙中的人类，没有其他人，它们都是截然不同的。 （类似于Prolog的封闭世界假设。）这类事情是通过z3py中的所谓枚举排序完成的。这就是我要为您的问题建模的方式：
from z3 import *

# Declare an enumerated sort. In this declaration we create 'Human' to be a sort with
# only the elements as we list them below. They are guaranteed to be distinct, and further
# any element of this sort is guaranteed to be equal to one of these.
Human, (Rob, Kev, Sama, Tho, Dor, Jim, Bor, Eli, Samu, Zel, Max) \
   = EnumSort('Human', ('Rob', 'Kev', 'Sama', 'Tho', 'Dor', 'Jim', 'Bor', 'Eli', 'Samu', 'Zel', 'Max'))

# Uninterpreted functions for parent/grandParent relationship.
parent      = Function('parent',      Human, Human, BoolSort())
grandParent = Function('grandParent', Human, Human, BoolSort())

s = Solver()

# An axiom about the parent and grandParent functions. Note that the variables
# x, y, and z are merely for the quantification reasons. They don't "live" in the
# same space when you see them at the top level or within a ForAll/Exists call.
x, y, z = Consts('x y z', Human)
s.add(ForAll([x, y, z], Implies(And(parent(x, z), parent(z, y)), grandParent(x, y))))

# Express known parenting facts. Note that unlike Prolog, we have to tell z3 that
# these are the only pairs of "parent"s available.
parents = [ (Rob, Kev), (Rob, Sama), (Sama, Tho),  (Dor, Jim)  \
          , (Bor, Jim), (Bor, Eli), (Jim, Tho),  (Sama, Samu)  \
          , (Jim, Samu), (Zel, Max), (Samu, Max)               \
          ]

s.add(ForAll([x, y], Implies(parent(x, y), Or([And(x==i, y == j) for (i, j) in parents]))))

# Find what makes Rob-Max belong to the grandParent relationship:
witness = Const('witness', Human)
s.add(grandParent(Rob, Max))
s.add(grandParent(Rob, witness))
s.add(parent(witness, Max))

# Let's see what witness we have:
print s.check()
m = s.model()
print m[witness]

为此，z3说：
sat
Samu

我相信这是您想要实现的目标。
请注意，z3的Horn逻辑可以更好地表达此类问题。为此，请参见：https://rise4fun.com/Z3/tutorialcontent/fixedpoints。这是z3支持的扩展，它在SMT求解器中不可用，使其更适合于关系编程任务。
已经说过，虽然确实有可能使用SMT求解器来表达这种类型的关系，但是这些问题实际上并不是SMT求解器所设计的。它们更适合涉及算术，位向量，数组，未解释函数，浮点数等的无量纲逻辑片段。尝试将这类问题作为学习练习总是很有趣的，但是如果这样做您真正关心的是某种问题，您应该真正遵循Prolog及其更适合这种建模的变体。