z3py中枚举关系的基本方法

Question

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

（假设）

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

预期结果）

• B杀了A
• B杀了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您必须适当地修改它们，以解释这里的未解释函数，这有点冗长，但不是特别困难。如果新问题给你带来困难，请随时提问