如何在 Z3py 中建模 [英] How to model in Z3py
问题描述
我一共有七个(A, B, C, D, E, r, c) Z3个布尔变量，其中A, B, C, D, E代表从一个点开始的边，用黑点表示如下图1.
I have a total of seven (A, B, C, D, E, r, c) Z3 Boolean variables, where A, B, C, D, E represent the edges from a point, represented as a black dot in the following Fig.1.
剩下的两个变量，即r和c是黑点点的变量，其值取决于边缘值如下:
The remaining two variables, i.e, r and c are the variables for the black dot point, whose values depend on edges values as follows:
变量‘r’的条件:情况 1:如果 A 为真，则只有来自 C 或 D 的一个变量可以为真情况 2:同样，如果 B 为真，则只有变量 C 或 D 为真.只有在情况 1 或情况 2 之一为真且 r 值应始终为真时，变量 r 才能为真.这些条件在 Z3 求解器中求解为:
The conditions for variable ‘r’: Case1: If A is true then only one variable from C or D can be true Case2: Similarly, if B is true then only variable either C or D can be true. The variable r can be true only if one of the either Case 1 or Case 2 is true and r value should always be True. These conditions are solved in Z3 solver as:
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"包含以下条件:
Now I have to include the following conditions for variable ‘c’ in Z3 solver:
变量‘c’可以为真，也可以为假.只有满足以下任一条件时，c"才会为真:
The variable ‘c’ can be true or false. And ‘c’ will be true only if any of the following conditions meet:
情况 3:如果 A 和 C 为真，那么如果 E 和 D 都为真，则 c 为真
Case 3: if A and C are True then c will be true if both E and D are true
情况 4:如果 A 和 D 为真，那么如果 E 和 C 都为真，则 c 为真
Case 4: if A and D are True then c will be true if both E and C are true
情况 5:如果 B 和 C 为真，那么如果 E 和 D 都为真，则 c 为真
Case 5: if B and C are True then c will be true if both E and D are true
情况 6:如果 B 和 D 为真，那么如果 E 和 C 都为真，则 c 为真
Case 6: if B and D are True then c will be true if both E and C are true
如何添加这些条件，因为我无法在 Z3 求解器中为c"变量的条件建模.
How to add these conditions as I am not able to model the conditions for ‘c’ variable in Z3 solver.
推荐答案
您的描述有点难以理解，但是您应该能够几乎按字面意思表达这些内容如下.(我添加了一些内联注释，以便您可以按照编码逻辑进行适当的修改.)
Your description is a bit hard to follow, but you should be able to express these almost literally as follows. (I added some inline comments so you can follow the coding logic and modify as appropriate.)
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
这会打印所有可能的模型.您当然可以进一步限制它.
This prints all possible models. You can of course constrain it further.
这篇关于如何在 Z3py 中建模的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
