每次运行项目时，都会生成不同顺序的 Z3 公式。即使公式完全相同，也会在不同的运行中重新排序，因此，从 Z3 获得的答案在每次运行中都不同。这会导致问题，因为我需要一个在每次运行中应该完全相同的最佳集。
例如
- 第一次运行是：
(declare-const l1 (_ BitVec 1))
(declare-const l2 (_ BitVec 1))
(declare-const l3 (_ BitVec 1))
(declare-const l4 (_ BitVec 1))
(declare-const l5 (_ BitVec 1))
(declare-const l6 (_ BitVec 1))
(declare-const l7 (_ BitVec 1))
(declare-const l8 (_ BitVec 1))
(declare-const l9 (_ BitVec 1))
(declare-const l10 (_ BitVec 1))
(minimize (bvadd l1 l2 l3 l4 l5 l6 l7 l8 l9 l10))
(maximize
(bvand
(bvor (bvand l3 l4 l1 l2) (bvand l4 l2) (bvand l4 l1 l2) (bvand l2 l3 l4))
(bvor (bvand l4 l2) (bvand l2 l3 l4))
(bvor (bvand l5 l7 l8 l10 l6) (bvand l5 l7 l8 l6) (bvand l5 l7 l8 l9 l6) (bvand l5 l7 l8 l9 l10 l6) (bvand l5 l7 l6) (bvand l5 l7 l9 l10 l6) (bvand l5 l7 l10 l6))
)
)
(check-sat)
(get-model)
给出的解决方案是：l7、l5、l2、l4、l6、l8。
在这种情况下，6 为真。
- 第二次运行是：
(declare-const l1 (_ BitVec 1))
(declare-const l2 (_ BitVec 1))
(declare-const l3 (_ BitVec 1))
(declare-const l4 (_ BitVec 1))
(declare-const l5 (_ BitVec 1))
(declare-const l6 (_ BitVec 1))
(declare-const l7 (_ BitVec 1))
(declare-const l8 (_ BitVec 1))
(declare-const l9 (_ BitVec 1))
(declare-const l10 (_ BitVec 1))
(minimize (bvadd l1 l2 l3 l4 l5 l6 l7 l8 l9 l10))
(maximize
(bvand
(bvor (bvand l2 l3 l4) (bvand l2 l4) (bvand l1 l2 l4) (bvand l2 l3 l4 l1))
(bvor (bvand l2 l3 l4) (bvand l2 l4))
(bvor (bvand l10 l6 l5 l7 l9) (bvand l10 l6 l5 l7) (bvand l10 l6 l5 l7 l8 l9) (bvand l10 l6 l5 l7 l8) (bvand l7 l6 l5) (bvand l7 l8 l9 l6 l5) (bvand l7 l8 l6 l5))
)
)
(check-sat)
(get-model)
它给出了解决方案：l7、l9、l5、l2、l4、l6、l8、l3。
在这种情况下，8 为真。
对于我的项目，我需要一个最佳的、最小化的集合。根据前面解释的条件，我需要尽可能少的变量为真。对于这两个运行，正确的最佳答案应该是：l2、l4、l5、l6、l7(5 true(。基本上我需要最小化成本并满足maximize条件内部的条件。
但是，我不会给出 5 个变量为 true 的最佳解决方案，而是获得 6、8、10 个 true 值。
我也尝试过的东西(assert (= (bvand ...) #b1) )代替(maximize (bvand ...) )，但无济于事。
如何获得最小、最佳数量的真变量，这些变量也满足条件，并且每次都给出相同的结果，即使在重新排序时也是如此？
注意：我不能使用 Int 或 Bool，因为我的程序可能会很大，int/bool 将无法处理它。
这里有几个问题。首先，您使用执行机器算术的bvadd最小化总和。也就是说，它将溢出位向量大小。(也就是说，该值始终为 0 或 1。为避免这种情况，请在较大的位向量大小上执行加法：
(define-fun ext ((x (_ BitVec 1))) (_ BitVec 8)
((_ zero_extend 7) x))
(minimize (bvadd (ext l1) (ext l2) (ext l3) (ext l4) (ext l5) (ext l6) (ext l7) (ext l8) (ext l9) (ext l10)))
在这里，我在添加之前将值扩展到 8 位：由于您有 10 个变量，因此 8 位足以表示10的总和。(在这种情况下，您也可以使用4位;这并不是说这很重要。只需确保它足够宽，可以表示要添加的变量总数。
但这里还有第二个问题。您要求 z3 首先最小化此总和，然后最大化第二个表达式。Z3 将进行词典优化，这意味着它将首先处理您的第一个约束，然后使用第二个约束。但是你的第一个变量将使所有变量0，以最小化总和。为避免这种情况，请确保交换约束的顺序。
最后评论：你确实明确说过"注意：我不能使用 Int 或 Bool，因为我的程序可能会很大，int/bool 将无法处理它。我觉得这很可疑。对于这样的问题，Bool是最明显和最佳的选择。特别是，优化器处理布尔值比处理位向量和整数要容易得多。因此，我建议在没有实际实验并有一些证据表明它无法扩展的情况下不要放弃这个想法。