#!/usr/bin/env python3
from z3 import And, Int, Solver, sat
# 矩阵
m = [
[1, 2, 3, 4, 5],
[2, 3, 4, 5, 6],
[3, 4, 5, 6, 7],
[4, 5, 6, 7, 8],
[5, 6, 7, 8, 9],
]
# 每一行的系数
vars = [Int(f'v{i}') for i in range(5)]
# 将系数乘上去并计算每列的和
final = []
for i in range(5):
final.append(sum([a * b for a, b in zip([l[i] for l in m], vars)]))
s = Solver()
# 添加约束条件
s.add(final[0] > 5)
s.add(final[1] < 600)
s.add(final[2] > 7)
s.add(final[3] < 800)
s.add(final[4] > 9)
while s.check() == sat:
m = s.model()
print(m)
# 排除掉这个解
s.add(And(*[i != m[i] for i in vars]))
print('finish')