使用 Z3 从受限空间中采样答案

【问题标题】：Using Z3 to sample from a constrained space使用 Z3 从受限空间中采样
【发布时间】：2017-01-06 07:21:10
【问题描述】：

我对变量有很多限制，我正在寻找一种在这个受限空间中有效采样的方法。我尝试了 Z3，它似乎能够告诉我空间是否重要（即约束是否可以满足）但我看不到从空间中获取示例的方法，除非我正在最小化或最大化某些东西.

是我遗漏了什么还是这不是 Z3 的用途？

【问题讨论】：

【解决方案1】：

您可以使用一些技术从 SAT 解空间中进行采样。见https://simons.berkeley.edu/sites/default/files/docs/4393/moshevardi.pdf

或许可以在 Z3 之上实现其中一些技术。

还有一个existing implementation of the UniGen algorithm for almost-uniform sampling of SAT solution space on github，不过是基于不同的SAT求解器，不确定是否支持SMT求解。

编辑：这里似乎有基于 Z3 的 SMT 采样器：https://github.com/RafaelTupynamba/SMTSampler

【讨论】：

【解决方案2】：

Z3 可以为您提供一个模型，即分配给满足约束的变量的一个示例（尝试 SMT2 中的 (get-model) 命令或 .NET API 中的 Solver.Model（在另一个中类似命名的命令）蜜蜂））。然后，您可以断言模型的否定，以强制求解器为下一个查询生成不同的分配。这种方案被许多应用程序使用，但它不一定“高效”，但这实际上取决于您尝试实现的采样类型（例如，Z3 模型不会在搜索空间中随机分布）。

【讨论】：

是的，我正在寻找随机抽样。我将不得不使用其他东西。有什么建议吗？
我在考虑使用欧几里得距离的策略：在生成第一个点后，开始优化以最大化您的常数和现有解决方案的距离。我希望在 Java 堆栈上的 github.com/groostav/sojourn-cvg 中执行此操作。问题在于措辞：SMT2 lisp-like 比 java API 好得多，我在导航时遇到了麻烦。结果可能很慢，但我希望它会在可行区域周围创建一种全因子边界框——不是均匀分布，但对我来说已经足够了。