如何解决参数的z3编码关系表
说我有下面显示的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,z3.Implies(z3.And(B_cond,A_cond),]
# solve some real constraint
s.add(A + B - C > 0)
s.check()
返回的模型仅属于implies
,因此不属于条件的第一行。
对于这种情况,是否有任何可行且更清洁的方法?
解决方法
我认为单独陈述每一行并加以分离很容易:
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,B == 3,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
不满意。
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。