z3编码参数关系表

Question

假设我有如下所示的A,B,C的参数关系表

╔══════════╦═══╦════════════╗
║    A     ║ B ║     C      ║
╠══════════╬═══╬════════════╣
║ [0...10] ║ 2 ║ [0...10]%4 ║
║ [0...10] ║ 3 ║ [0...10]%3 ║
╚══════════╩═══╩════════════╝

这意味着对于A、B、C的任何值，它必须满足表中的至少一行。这隐含地意味着，例如，B受2 <= B <= 3的约束。我将如何在z3求解器中对此进行编码？

我目前的方法是使用z3.隐含并采用参数的组合：

import z3
# encode only the first row
A_cond = z3.And(A>=0, A<=10)
B_cond = B==2
C_cond = z3.And(z3.And(C>=0, C<=10), C%4==0)
s = z3.Solver()
s.add([z3.Implies(z3.And(A_cond, B_cond), C_cond),
z3.Implies(z3.And(A_cond, C_cond), B_cond),
z3.Implies(z3.And(B_cond, C_cond), A_cond),]
# solve some real constraint
s.add(A + B - C > 0)
s.check()

返回的模型不属于第一行条件，因为它只是implies。对于这种情况，有什么有效且更清洁的方法吗？

Answer 1

我认为单独声明每一行并取其析取值要容易得多：

from z3 import *
A, B, C = Ints('A B C')
row1 = And(A >= 0, A <= 10, B == 2, C >= 0, C <= 10, C % 4 == 0);
row2 = And(A >= 0, A <= 10, B == 3, C >= 0, C <= 10, C % 3 == 0);
rows = [row1, row2]
s = Solver()
s.add(Or(rows))
s.add(A+B-C > 0)
print (s.check())
print (s.model())

这很容易扩展到许多行，并且您可以根据需要以编程方式简化常见条件。运行时，它会打印：

sat
[A = 10, B = 2, C = 4]

你甚至可以通过运行来找出哪一行满意

m = s.model()
print([i+1 for i, row in enumerate(rows) if m.evaluate(row)])

打印：

[1]

这意味着row1满意，但row2不满意。