1

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

结果如下：

使用

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

(2) 我知道，如果我在没有优化模块的情况下使用Z3py API，我将不得不执行@Leonardo de Moura在（整数变量的最小值和最大值）中描述的典型顺序搜索。它永远不会给我结果。

我的方法

（3）我试图通过实现类似于它在（Z3 是否支持优化问题）中解释@Philippe 的二进制搜索来改进顺序搜索方法，当我运行我的算法时它会等待并且我没有得到任何结果。

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

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

而且，这是我在初始测试中使用的另一个实例（代码短实例），它在任何情况下都运行良好。

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

问候，亚历克斯

4

1 回答 1

1

我不认为你的问题与最小化本身有关。如果你在你的程序中添加一个print rafter r = s.check()，你会发现 z3 很难返回一个结果。所以你的循环甚至不会执行一次。

因为它真的很大，所以不可能通读你的程序！但我看到了很多形式的东西：

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

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

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

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

于 2019-06-25T17:50:59.077 回答