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

Question

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

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

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

有什么想法吗？

Answer 1

我认为 x <2, x> 3 和 x> 5 没有解。您可以找到第一个解决方案，然后将其添加到条件中。例如

from z3 import *
solver = Solver()
x = Int('x')

constraints = [
    x < 5
]

for i in constraints:
    solver.add(i)
print(solver.check())
while solver.check() == sat:
    print(solver.model()[x])
    solver.add(x < solver.model()[x])

Output:
sat
4
0
-1
-2
-3
-4
-5
-6
-7
....
-to minus infinity

第二种解法

 from z3 import *
import itertools
solver = Solver()
x = BitVec('x', 64)

combinations = [
    x < 2,
    x > 3,
    x > 5
]

#I create a list of all possible combinations of conditions
stuff = [0, 1, 2]
conditionLst = []
for L in range(0, len(stuff)+1):
    for subset in itertools.combinations(stuff, L):
        conditionLst.append(subset)
print(conditionLst)


#for every combination I am looking for solutions
for cond in conditionLst:
    solver = Solver()
    for i in cond:
        solver.add(combinations[i])
    solver.check()
    if solver.check() == sat:
        for j in cond:
            print(combinations[j], end=", ")
        print(solver.model())
    elif solver.check() == unsat:
        for j in cond:
            print(combinations[j], end=", ")
        print(solver.check())
    del solver


x < 2, [x = 1]
x > 3, [x = 4]
x > 5, [x = 6]
x < 2, x > 3, unsat
x < 2, x > 5, unsat
x > 3, x > 5, [x = 6]
x < 2, x > 3, x > 5, unsat

如果一次无法解决所有组合，则转到下面的级别。如果有 2 个条件的解决方案，则查看是否有第三个条件的解决方案。你可以为此制定一个算法。

Answer 2

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

基于此策略，我将为每个约束创建一个跟踪器变量 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]，但我相信这也是一个有效的解决方案。

如果您还想获得更严格的边界，您还可以向优化求解器添加条件（通过 minimize/maximize 调用）。但是，这可能会运行出现问题：例如，对于您的原始约束集，没有 x 的 minimum/maximum 值可以唯一地满足它们，因此您可以运行进入优化器将失败的情况。如果你知道你所有的变量都是有界的，那么你可以走那条路。否则，您可以尝试调用优化器，如果它没有 return 固定结果，请像我上面那样使用 sat 调用的结果。当然，所有这些都取决于您的特定限制，但与 z3 无关。

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

z3 to find minimal combinations to satisfy multiple conflicting constraints

python

z3