枚举z3py中关系的基本方法

Question

我想建立一个基本模型来搜索两个对象之间的关系。

假设]

• 对象：有属于个人类别的A和B。
• 规则：人可以杀死人。如果有人杀了人，人就会死。
• 事实：A已死。 B还没死。

预期结果]

• B杀死A
• B杀死A. A杀死A。
• 被杀死的A。

我的代码指的是由正式z3py（凡人苏格拉底）分发的示例程序。但是，我找不到如何描述这种关系。

from z3 import *

Person, (a,b) = EnumSort("Person",["a","b"])

Kill = Function('Kill', Person,Person, BoolSort())
Dead = Function('Dead', Person, BoolSort())

# free variables used in forall must be declared Const in python
x = Const('x', Person)
y = Const('y', Person)

s = Solver()

s.add(ForAll([x,y],Implies(Kill(x,y),Dead(y))))
s.add(Dead(a))
s.add(Not(Dead(b)))

print(s.check()) # prints sat so axioms are coherent    
m=s.model()
print(m)

Answer 1

您非常接近！只需在末尾添加以下内容：

res = s.check()

if res == sat:
   m = s.model()
   print "Is A dead   : %s" % m.eval(Dead(a))
   print "Is B dead   : %s" % m.eval(Dead(b))
   print "Did A kill A: %s" % m.eval(Kill(a, a))
   print "Did A kill B: %s" % m.eval(Kill(a, b))
   print "Did B kill A: %s" % m.eval(Kill(b, a))
   print "Did B kill B: %s" % m.eval(Kill(b, b))
else:
    print "Not satisfiable, got: %s" % res

有了这个，z3说：

Is A dead   : True
Is B dead   : False
Did A kill A: False
Did A kill B: False
Did B kill A: False
Did B kill B: False

模型可能看起来有些奇怪。如果A已死，谁杀死了它？它发现的模型说，没有人杀死任何人。片刻的想法表明它与您提出的公理是完全一致的：有人可以刚开始就死定了。但这也许不是您想要的。因此，让我们添加一些效果：如果您死了，一定有人杀死了您：

s.add(ForAll([x], Implies(Dead(x), Exists([y], Kill(y, x)))))

我们现在得到：

Is A dead   : True
Is B dead   : False
Did A kill A: True
Did A kill B: False
Did B kill A: True
Did B kill B: False

更好！但是哦，现在z3说A被A和B杀死。我们可能需要谈一谈是否有人死亡，然后只有一个人杀死它。至少，死者没有参与其中。 （第一个模型很难建模，但是在您的世界中有两个Person时，应该不那么难。）因此，让我们禁止自杀：

s.add(ForAll([x], Not(Kill(x, x))))

哪个生产：

Is A dead   : True
Is B dead   : False
Did A kill A: False
Did A kill B: False
Did B kill A: True
Did B kill B: False

这看起来很合理！

尽管诸如此类的问题很有趣，但是SMT求解器通常不善于在存在量词的情况下进行推理。有了这样的有限模型，就不会有太大的问题了。但是，如果您开始包括Int，Real等类型的对象，尤其是交替量词，则z3不太可能响应这样的查询。您很可能会收到unknown响应，这是SMT解决方案人员所说的问题，对于基于SMT的基本推理而言，这个问题太难了。

枚举所有可能的解决方案

如果您不想添加新的公理，而只是找到满足原始集合的所有模型，则可以通过添加阻塞子句来做到这一点。也就是说，您可以获取一个模型，找到它指定的值，并断言这些值不好。并重复。关于堆栈溢出的答案很多，描述了如何做到这一点，例如：(Z3Py) checking all solutions for equation您必须适当地修改它们，以解决此处具有的未解释函数，这虽然有些冗长，但并不是特别困难。随时问一个新问题，是否会给您带来麻烦！