Z3每次重新排序参数后，都会给出不同的答案。优化问题

Question

每次运行我的项目时，都会生成不同顺序的Z3公式。即使公式是完全相同的，但在不同的运行中会重新排序，因此，在每次运行中从Z3中得到的答案都是不同的。这就造成了问题，因为我需要一个最佳集合，它应该在每次运行中完全相同。

例如，我需要一个最佳集合，这个集合在每次运行中都应该是完全相同的。

1. 第一次运行是。

(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在这种情况下是真的。

2. 第二次运行是。

(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个真)。基本上，我需要将成本降到最低，并满足里面的条件。maximize 的条件。

然而，我并没有给出5个变量为真的最优解，而是得到6、8、10个真值。 我还尝试了一些方法 (assert (= (bvand ...) #b1) ) 代替 (maximize (bvand ...) )但无济于事。

如何才能获得最小的、最优的真变量数，同时也满足条件，并且每次都能得到相同的结果，甚至在重新排序时也是如此？

注：我不能使用Int或Bool，因为我的程序可能会很大，intbool将无法处理它。

Answer 1

这里有几个问题。首先，你是在用以下方法使总和最小化 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，因为我的程序很可能会很庞大，而intbool是我的程序的一部分。你明确说过 "注意: 我不能使用Int或Bool 因为我的程序很可能是巨大的 而intbool将无法处理" 我觉得这一点非常可疑。对于这样的问题，一个 Bool 将是最明显和最佳的选择。特别是，优化器在处理布尔函数时，会比处理位向量和整数时容易得多。所以，我建议在没有实际实验和掌握一些证据证明它不能扩展的情况下，不要放弃这个想法。