在像gecode这样的约束求解器中，我们可以借助分支功能来控制搜索空间的探索。例如branch(home,x,INT_VAL_MIN )这将开始从变量x在其域中的最小可能值中探索搜索空间，并尝试寻找解决方案。（有许多这样的选择。）
对于z3，我们内置了这种灵活性吗？有其他选择吗？
Gecode branch（）函数的z3替代方案？
•
问答
iCMS 回答：Gecode branch（）函数的z3替代方案？
SMT求解器通常不允许给出此类“提示”，它们更多地充当黑匣子。
话虽如此，每个求解器都使用大量内部启发法，并且z3本身具有许多设置，您可以使用这些设置来给出提示。如果您运行：
z3 -pd
它将显示您可以提供的所有选项，实际上有600多个！不幸的是，这些选项没有得到很好的记录，而且它们如何影响求解器还很神秘。找出问题的唯一可靠方法是研究源代码，看看它们在做什么，这不是出于胆小。但是无论如何，它不会像您引用gecode的分支功能那样明显。
但是，还有其他一些技巧可以用来加快SMT求解器的求解速度，但是不幸的是，这些事情通常都是针对特定问题的。如果您发布特定实例，则可能会得到更好的建议。