python - z3 找到满足多个冲突约束的最小组合

Question

假设我有约束:x < 2 , x > 3和 x > 5 ，如何让 z3 生成最小解决方案，例如x = [1, 6] ？

我想我可以使用 Or 来实现它, 并为每个解决方案阻止解决条件，但这并不能保证它会产生最小集合。

我的另一个解决方案是单独解决每个条件并收集尽可能多的结果，并有一个算法来为每个条件选择重叠的结果。

有什么想法吗？

Answer 1

这种“跟踪”约束经常出现。虽然可能有多种解决方案，但我认为最好的解决方案是显式添加跟踪变量，然后迭代直到满足所有约束。您应该为此目的使用优化求解器，最大限度地增加每次调用中释放的约束数量。通过这种方式，您将确保解决方案的数量保持最少。

基于此策略，我将为每个约束创建一个跟踪器变量 pN，并将它们与蕴涵配对。然后，我会最大化应该满足的 pN 的数量。这是一种可能的编码:

from z3 import *

x = Int('x')

p1, p2, p3 = Bools('p1 p2 p3')
constraints = [(p1, x < 2), (p2, x > 3), (p3, x > 5)]

solutions = []
while constraints:
    o = Optimize()

    s = 0
    for (tracker, condition) in constraints:
        o.add(Implies(tracker, condition))
        s = s + If(tracker, 1, 0)
    o.maximize(s)

    remaining = []
    r = o.check()
    if r == sat:
        m = o.model()
        solutions.append(m[x])
        print("Candidate: %s" % m[x])
        for (tracker, condition) in constraints:
            if(m[tracker]):
                print("  Constraint: %s satisfied, skipping." % condition.sexpr())
            else:
                print("  Constraint: %s is not yet satisfied, adding." % condition.sexpr())
                remaining.append((tracker, condition))
    else:
        print("Call returned: %s" % r)
        exit(-1)

    constraints = remaining

print("Solution: %s" % solutions)

运行时，打印:

Candidate: 6
  Constraint: (< x 2) is not yet satisfied, adding.
  Constraint: (> x 3) satisfied, skipping.
  Constraint: (> x 5) satisfied, skipping.
Candidate: 0
  Constraint: (< x 2) satisfied, skipping.
Solution: [6, 0]

因此，这将计算解决方案 [6, 0]。您最初想要 [1, 6]，但我相信这也是一个有效的解决方案。

如果您还想获得更严格的界限，您还可以向优化求解器添加条件(通过最小化/最大化调用)。但是，这可能会遇到问题:例如，对于您的原始约束集，没有唯一满足它们的 x 的最小值/最大值，因此您可能会遇到优化器失败的情况.如果你知道你所有的变量都是有界的，那么你可以走那条路。否则，您可以尝试调用优化器，如果它没有返回固定结果，请像我上面那样使用 sat 调用的结果。当然，所有这些都取决于您的特定限制，但与 z3 无关。