z3：如何求解一组常数的组合？答案

【问题标题】：z3: How to solve for combinations for a set of constants?z3：如何求解一组常数的组合？
【发布时间】：2017-10-21 00:38:22
【问题描述】：

我对数学不是很精通，所以如果我在这里使用了错误的术语，请不要毁了我。

我想用 z3 解决的问题是这样的：

x + y = z

假设 x 和 z 是整数。

其中 y 是一个常量数组，例如 (12,13,14,-13)，可以在求解器认为合适的情况下使用、重用或不使用。

如何将其转化为 z3 的功能？我怀疑答案是为这些常量的每个可能组合生成一个约束，但我还没有看到一个与我正在尝试做的非常相似的例子。

换句话说，我将如何翻译许多编程面试中发现的“总和组合”之类的问题，例如：

Finding all possible combinations of numbers to reach a given sum

或者

https://leetcode.com/problems/combination-sum/description/

到 z3 符号？

确切地说，尚不清楚的部分是如何与求解器通信，它从 array 的选择中支付 pick 次次 em> 随心所欲。

【问题讨论】：

想解释一下您为什么拒绝投票？其他类似的问题之前在 SO 上也被接受过。
对于初学者：什么是x，什么是z；并取决于这些：+ 是什么？这个例子是纯偶然的吗？
这有什么关系？我会改变这个问题，但根据我的经验，对于你想给它的任何数据类型，它在 z3 中的工作方式都是一样的。假设它们是整数。我的问题是让 z3 在一组组合中随意选择。
听起来我没有违反规则。你没有因为正确的理由投票。另外，我改了。假设它是整数好吗？
也许这可行？我仍然无法想象我如何将 z3 传递给 python 数组并将其转换为一堆类似的“或”。您将如何传达它可以随意重复使用一个值，或者根本不重复使用？

标签： python z3 smt

【解决方案1】：

当然，这对于任何 SMT 求解器来说都相当容易。这是一种编码方式：

from z3 import *

s = Solver()
x = Int("x")
y = Int("y")
z = Int("z")

s.add(Or(y == 12, y == 13, y == 14, y == -13))
s.add(x + y == z)

while s.check() == sat:
    m = s.model ()
    if not m:
        break
    print m
    s.add(Not(And([v() == m[v] for v in m])))

请注意，有无限多的三元组可以满足这组特定的约束，因此当您运行上述程序时，它将永远打印解决方案！

要解决求和为一个数字的数字子集，您可以进行类似的操作。为每个元素声明一个布尔值。然后，编写一个求和表达式，将所有数字相加，使得相应的布尔值为True，并断言该总和等于所需数字的约束。有趣的小练习，使用 Z3 也很容易表达。如果您试一试并遇到问题，请随时提出更多问题。

【讨论】：

问题：如何让求解器区分 Y 的每个值都可以重复使用？另外，你如何告诉求解器只给你它找到的前 n 个解决方案？我怀疑需要在约束本身中添加进一步的边界。
你试过上面的代码了吗？它将重用y 的每个值。对于第一个n 解决方案，只需保持计数并在多次迭代后退出while 循环。