z3 - Gecode 分支（）函数的 z3 替代方案？

Question

在像 Gecode 这样的约束求解器中，我们可以借助分支函数来控制搜索空间的探索。例如，branch(home , x , INT_VAL_MIN )这将从变量 x 在其域中的最小可能值开始探索搜索空间并尝试找到解决方案。（有很多这样的替代方案。）

对于 z3，我们是否具有这种内置的灵活性？有没有可能的替代方案？？

Answer 1

SMT 求解器通常不允许给出这些类型的“提示”，它们更像是黑盒。

话虽如此，每个求解器都使用了大量的内部启发式算法，而 z3 本身有许多设置，您可以使用它们来给出提示。如果你运行：

z3 -pd

它将显示您可以提供的所有选项，实际上有 600 多个选项！不幸的是，这些选项并没有得到很好的记录，它们对求解器的影响是相当神秘的。找出答案的唯一可靠方法是研究源代码，看看它们做了什么，这不适合胆小的人。但无论如何，它不会像您为 gecode 引用的分支功能那么明显。

然而，还有其他技巧可以用来加快 SMT 求解器的求解速度，不幸的是，这些东西通常是针对特定问题的。如果您发布特定实例，您可能会得到更好的建议。