Z3 Max SMT 优化是否适合最小化违反约束？

如何解决Z3 Max SMT 优化是否适合最小化违反约束？

我正在尝试解决一个线性方程组，并附加一个约束，即每个变量都应该来自一个小的有限数字集。

然而，在我的情况下，这不能适用于所有变量，因为这样就不存在解决方案。因此，我试图将其表述为一个 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 来实现这一点，除非另有说明，默认设置。