Gecode branch()函数的z3替代方案？

Posted 2023-01-28

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

对于z3，我们有这样的灵活性内置吗？有可能的替代方案吗？

答案

SMT求解器通常不允许给出这类 "提示"，它们更多的是作为黑盒。

尽管如此，每个求解器都会使用大量的内部启发式方法，而且z3本身也有一些设置，你可以通过这些设置来给它提示。如果你运行:

z3 -pd

它会显示所有你能提供的选项 有超过600个！不幸的是，这些选项并没有被很好地记录下来，它们如何影响解算器是相当神秘的。唯一可靠的方法是研究源代码，看看它们是怎么做的，这对胆小的人来说并不可靠。但无论如何，都不会像你举的gecode的分支功能那样明显。

不过，对于SMT-solvers来说，还有其他的技巧可以用来加快求解速度，不幸的是，这些东西通常都是非常具体的问题。如果你贴出具体的实例，可能会得到更好的建议。