如何在 Z3py 中建模

如何解决如何在 Z3py 中建模

我一共有七个(A,B,C,D,E,r,c) Z3个布尔变量，其中A,E代表从一个点开始的边，用黑点表示如下图1。

剩下的两个变量，即r和c是黑点点的变量，其值取决于边缘值如下：

变量‘r’的条件： 情况 1：如果 A 为真，则只有来自 C 或 D 的一个变量可以为真 情况 2：同样，如果 B 为真，则只有变量 C 或 D 为真。 只有在情况 1 或情况 2 之一为真且 r 值应始终为真时，变量 r 才能为真。 这些条件在 Z3 求解器中求解为：

s.add(Implies(A,Xor(C,D) ))
s.add(Implies(B,D) )) 
s.add(r1 == Xor(A,B) )
s.add(r1 == True)

现在我必须在 Z3 求解器中为变量“c”包含以下条件：

变量‘c’可以为真，也可以为假。 只有满足以下任一条件时，“c”才会为真：

情况 3：如果 A 和 C 为真，那么如果 E 和 D 都为真，则 c 为真

情况 4：如果 A 和 D 为真，那么如果 E 和 C 都为真，则 c 为真

情况 5：如果 B 和 C 为真，那么如果 E 和 D 都为真，则 c 为真

情况 6：如果 B 和 D 为真，那么如果 E 和 C 都为真，则 c 为真

如何添加这些条件，因为我无法在 Z3 求解器中为“c”变量的条件建模。

解决方法

您的描述有点难以理解，但您应该能够几乎按字面意思表达这些内容如下。 （我添加了一些内联注释，以便您可以按照编码逻辑进行适当的修改。）

from z3 import *

A,B,C,D,E,r,c = Bools('A B C D E r c')

s = Solver()

# Case 1
Case1 = Implies(A,Xor(C,D))
s.add(Case1)

# Case 2
Case2 = Implies(B,D))
s.add(Case2)

# Conditions for r. Your description is a bit confusing here,# as it says both `r` is true,and if one of Case1 or Case2
# is true. This suggests one of Case1 or Case2 must be true,# though it's not clear to me why described it in this complex
# way. Modify accordingly.
s.add(r)
s.add(Or(Case1,Case2))

# Case 3: if A and C are True then c will be true if both E and D are true
s.add(Implies(And(A,C),Implies(And(E,D),c)))

# Case 4: if A and D are True then c will be true if both E and C are true
s.add(Implies(And(A,c)))

# Case 5: if B and C are True then c will be true if both E and D are true
s.add(Implies(And(B,c)))

# Case 6: if B and D are True then c will be true if both E and C are true
s.add(Implies(And(B,c)))

vars = [A,c]
while s.check() == sat:
    m = s.model()
    for v in vars:
      print("%s = %5s" % (v,m.evaluate(v,model_completion = True))),print
    s.add(Or([p != v for p,v in [(v,model_completion = True)) for v in vars]]))

运行时，打印：

A = False B = False C = False D = False E = False r =  True c = False
A = False B = False C =  True D = False E = False r =  True c = False
A = False B = False C =  True D =  True E = False r =  True c = False
A = False B = False C = False D =  True E = False r =  True c =  True
A = False B = False C =  True D = False E = False r =  True c =  True
A = False B = False C =  True D =  True E = False r =  True c =  True
A = False B =  True C = False D =  True E = False r =  True c =  True
A = False B =  True C =  True D = False E = False r =  True c = False
A = False B =  True C =  True D = False E = False r =  True c =  True
A =  True B =  True C =  True D = False E = False r =  True c =  True
A =  True B = False C =  True D = False E =  True r =  True c =  True
A = False B =  True C =  True D = False E =  True r =  True c =  True
A =  True B =  True C =  True D = False E =  True r =  True c = False
A =  True B =  True C =  True D = False E =  True r =  True c =  True
A = False B =  True C = False D =  True E =  True r =  True c =  True
A = False B =  True C =  True D = False E =  True r =  True c = False
A = False B = False C =  True D = False E =  True r =  True c = False
A = False B = False C =  True D =  True E =  True r =  True c = False
A = False B = False C = False D =  True E = False r =  True c = False
A = False B = False C = False D =  True E =  True r =  True c = False
A = False B = False C = False D = False E =  True r =  True c = False
A = False B = False C = False D = False E =  True r =  True c =  True
A = False B = False C = False D = False E = False r =  True c =  True
A = False B = False C = False D =  True E =  True r =  True c =  True
A =  True B = False C = False D =  True E =  True r =  True c =  True
A =  True B = False C = False D =  True E =  True r =  True c = False
A =  True B =  True C = False D =  True E = False r =  True c = False
A =  True B =  True C = False D =  True E =  True r =  True c = False
A = False B =  True C = False D =  True E = False r =  True c = False
A =  True B =  True C = False D =  True E = False r =  True c =  True
A =  True B = False C = False D =  True E = False r =  True c =  True
A =  True B = False C =  True D = False E = False r =  True c =  True
A =  True B = False C =  True D = False E = False r =  True c = False
A =  True B = False C = False D =  True E = False r =  True c = False
A = False B =  True C = False D =  True E =  True r =  True c = False
A = False B = False C =  True D =  True E =  True r =  True c =  True
A = False B = False C =  True D = False E =  True r =  True c =  True
A =  True B =  True C =  True D = False E = False r =  True c = False
A =  True B = False C =  True D = False E =  True r =  True c = False
A =  True B =  True C = False D =  True E =  True r =  True c =  True

这会打印所有可能的模型。您当然可以进一步限制它。