这是一个Z3模型。
Z3 是微软的定理证明器。该模型与之前提出的MIP模型非常相似。
在MIP中枚举整数解并不完全是微不足道的(可以通过一些努力
[链接] 或使用高级MIP求解器中的“解池”技术来完成)。使用
Z3会更容易一些。甚至更容易的方法是使用约束编程(CP)求解器:它们可以自动枚举解决方案。
我们开始吧:
from z3 import *
A = [[1, 2, 1], [3, 1, -1]]
b = [20, 12]
n = len(A[0])
m = len(b)
X = [ Int('x%d' % i) for i in range(n) ]
s = Solver()
s.add(And([ X[i] >= 0 for i in range(n) ]))
for i in range(m):
s.add( Sum([ A[i][j]*X[j] for j in range(n) ]) == b[i])
while s.check() == sat:
print(s.model())
sol = [s.model().evaluate(X[i]) for i in range(n)]
forbid = Or([X[i] != sol[i] for i in range(n)])
s.add(forbid)
它解决了什么问题。
x0+2x1+x2 = 20
3x0+x1-x2 = 12
解决方案如下:
[x2 = 2, x0 = 2, x1 = 8]
[x2 = 7, x1 = 4, x0 = 5]
[x2 = 12, x1 = 0, x0 = 8]
我们可以打印最终模型,以便查看如何添加“禁止”约束:
[And(x0 >= 0, x1 >= 0, x2 >= 0),
1*x0 + 2*x1 + 1*x2 == 20,
3*x0 + 1*x1 + -1*x2 == 12,
Or(x0 != 2, x1 != 8, x2 != 2),
Or(x0 != 5, x1 != 4, x2 != 7),
Or(x0 != 8, x1 != 0, x2 != 12)]