z3 - Z3 寻找部分赋值的策略

Question

假设我有一个公式 F，其中包含变量 w、x、y、z。

Z3 是否有任何策略可以找到 F 的部分模型，但部分模型必须包含 y 和 z 的分配。（我不在乎 w 和 x。）

通过应用这种策略，Z3 查找部分模型所花费的时间比查找完整模型所花费的时间更少。

有这样的战术存在吗？

Answer 1

没有内置的策略可以做到这一点。找到精确的“不在乎”的集合并不便宜。此外，如果w和x真的“不在乎”，那么它们应该不会对 Z3 的性能产生重大影响。