使用 Z3 从约束 space 中采样
Using Z3 to sample from a constrained space
我对变量有很多约束，我正在寻找一种方法来有效地对这些约束 space 进行采样。我试用了 Z3，它似乎能够告诉我 space 是否重要（即约束是否可满足），但我看不到从 space 中获取示例的方法，除非我正在最小化或最大化某些东西。
我是不是遗漏了什么，或者这不是 Z3 的用途？
Z3 可以给你一个模型，即一个满足约束的变量赋值示例（尝试 SMT2 中的 (get-model) 命令或 .NET [=15] 中的 Solver.Model =]（以及其他 API 中的类似名称））。然后您可以断言模型的否定以强制求解器为下一个查询生成不同的分配。许多应用程序都使用这种方案，但不一定 "efficient"，但这实际上取决于您要实现的采样类型（例如，Z3 模型不会在搜索中随机分布 space).
您可以使用一些技巧从 SAT 解决方案中取样 space。参见 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
我对变量有很多约束，我正在寻找一种方法来有效地对这些约束 space 进行采样。我试用了 Z3，它似乎能够告诉我 space 是否重要（即约束是否可满足），但我看不到从 space 中获取示例的方法，除非我正在最小化或最大化某些东西。
我是不是遗漏了什么，或者这不是 Z3 的用途？
Z3 可以给你一个模型，即一个满足约束的变量赋值示例（尝试 SMT2 中的 (get-model) 命令或 .NET [=15] 中的 Solver.Model =]（以及其他 API 中的类似名称））。然后您可以断言模型的否定以强制求解器为下一个查询生成不同的分配。许多应用程序都使用这种方案，但不一定 "efficient"，但这实际上取决于您要实现的采样类型（例如，Z3 模型不会在搜索中随机分布 space).
您可以使用一些技巧从 SAT 解决方案中取样 space。参见 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