如何在 Z3py 中改进基于二分搜索的优化

Question

我正在尝试使用 Z3py 优化基于最小化的集合覆盖问题 (SCP41) 的实例。

结果如下：

使用

(1) 我知道 Z3 支持优化 (https://rise4fun.com/Z3/tutorial/optimization)。很多时候我在 SCP41 和其他实例中都达到了最佳状态，但也有一些没有。

(2) 我知道，如果我在没有优化模块的情况下使用 Z3py API，我将不得不执行@Leonardo de Moura 在 (Minimum and maximum values of integer variable) 中描述的典型顺序搜索。它永远不会给我结果。

我的方法

(3) 我试图通过实现类似于它在 (Does Z3 have support for optimization problems) 中解释@Philippe 的二进制搜索来改进顺序搜索方法，当我运行我的算法时它会等待并且我没有得到任何结果。

我知道二进制搜索应该更快并且在这种情况下可以工作？我也知道实例 SCP41 很大，产生了很多限制，它变得非常具有组合性，这是我的完整代码 (Code large instance)，这是我的二进制搜索：

def min(F, Z, M, LB, UB, C):    
    i = 0
    s = Solver()

    s.add(F[0])
    s.add(F[1])
    s.add(F[2])
    s.add(F[3])
    s.add(F[4])
    s.add(F[5])

    r = s.check()

    if r == sat:
        UB = s.model()[Z]

        while int(str(LB)) <= int(str(UB)):

            C = int(( int(str(LB)) + int(str(UB)) / 2))

            s.push()
            s.add( Z > LB, Z <= C)

            r = s.check()

            if r==sat:
                UB = Z
                return s.model()
            elif r==unsat:
                LB = C
                s.pop()

            i = i + 1
            if (i > M):
                raise Z3Exception("maximum not found, maximum number of iterations was reached")
    return unsat

而且，这是我在初始测试中使用的另一个实例 (Code short instance)，它在任何情况下都运行良好。

什么是不正确的二分搜索或 Z3 的某些概念没有正确应用？

问候， 亚历克斯

Answer 1

我认为您的问题与最小化本身无关。如果您在程序中将print r 放在r = s.check() 之后，您会看到z3 很难返回结果。所以你的循环甚至不会执行一次。

您的程序实在是太大了，无法通读它！但是我看到了很多类似的东西：

 Or(X250 == 0, X500 == 1)

这表明您的变量 X250 X500 等（并且有很多）实际上是布尔值，而不是整数。如果确实如此，那么您绝对应该坚持使用布尔值。求解整数约束比求解纯布尔约束要困难得多，当您像这样使用整数对布尔值建模时，底层求解器只是探索无法到达的搜索空间。

如果确实如此，即，如果您使用 Int 值对布尔值进行建模，我强烈建议您对问题进行建模以摆脱 Int 值并仅使用布尔值。如果您提出问题的“小”实例，我们可以帮助建模。

如果您确实需要 Int 值（很可能就是这种情况），那么我会说您的问题对于 SMT 求解器来说太难了，无法有效处理。您最好使用针对此类优化问题进行调整的其他系统。