如何在 Z3py 中建模

Question

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

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

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

s.add(Implies(A, Xor(C,D) ))
s.add(Implies(B, Xor(C,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”变量的条件建模。

Answer 1

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

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, Xor(C,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, D), Implies(And(E, C), 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), Implies(And(E, D), 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, D), Implies(And(E, C), c)))

vars = [A, B, C, D, E, r, 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, m.evaluate(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

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

如何在 Z3py 中建模

How to model in Z3py

python

z3

z3py