问题描述
我正在尝试解决一个线性方程组，并附加一个约束，即每个变量都应该来自一个小的有限数字集。
然而，在我的情况下，这不能适用于所有变量，因为这样就不存在解决方案。因此，我试图将其表述为一个 Max-SMT 问题，我想在其中最大化源自各自集合的变量数量。对许多变量执行此操作导致远非最佳解决方案。
一个例子是：
(declare-fun B () Int)
(declare-fun A () Int)
(declare-fun D () Int)
(declare-fun C () Int)
(declare-fun E () Int)
(assert (= (- (+ 0 (* 1 C) (* 1 D)) (+ 0 (* 1 A) (* 1 B))) 0))
(assert (= (- (+ 0 (* 1 E)) (+ 0 (* 1 D) (* 2 C))) 0))
(assert (= (- (+ 0 (* 1 D)) (+ 0 (* 1 E) (* 1 A))) 0))
(assert-soft (or (= A 0) (= A 1) (= A 2)) :weight 10)
(assert-soft (or (= B 0) (= B (- 1))) :weight 10)
(assert-soft (or (= C 0) (= C (- 1)) (= C (- 2))) :weight 10)
(assert-soft (or (= D 0) (= D 2)) :weight 10)
(assert-soft (or (= E 5)) :weight 10)
(check-sat)
即对于 A + B = C + D，
D + 2 C = E 和
D = E + A：
A 在 {0,2} 中，B 在 {0,-1} 中，C 在 {0,-1,-2} 中，D 在 {0,2} 中且 E = 5。>
最优解是 A = 2、B = -1、C = -1、D = 2 和 E = 0。
对于这样一个使用 Z3 的 Max-SMT 的小例子来说效果很好。当我尝试将其放大时，使用 ~1000 个变量和 2000 个方程，检查确实返回 sat 但所提供的解决方案（~600 个违反条款）远比我使用简单的贪婪算法（ ~ 50 条违反条款）。
这不是 Z3 的用例还是我使用错误？我已经使用 z3py 来实现这一点，除非另有说明，默认设置。
解决方法
暂无找到可以解决该程序问题的有效方法，小编努力寻找整理中！
如果你已经找到好的解决方法，欢迎将解决方案带上本链接一起发送给小编。
小编邮箱:dio#foxmail.com (将#修改为@）