z3py中关系枚举的基本方法

Question

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

(假设)

• Object :存在属于Person类的A和B。
• 规则:人可以杀人。如果有人杀了人，人就会死。--
• 事实:A已经死了。B没有死。

预期结果)

• B杀A
• B杀A 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，您必须适当地修改它们，以说明您在这里所拥有的未解释函数，这有点冗长，但并不特别困难。如果新问题给你带来困难的话，尽管问吧！