z3 参数关系编码表答案

【问题标题】：z3 encoding table of relations for parametersz3 参数关系编码表
【发布时间】：2020-10-13 08:57:21
【问题描述】：

假设我有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.Implies 并采用参数组合：

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。对于这种情况，是否有任何有效且更清洁的方法？

【问题讨论】：

标签： python z3 z3py

【解决方案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 不满意。

【讨论】：