Gecode branch() 函数的 z3 替代方案? [英] z3 alternative for Gecode branch() function?

问题描述

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

In constraint solver like Gecode , We can control the exploration of search space with help of branching function. for e.g. branch(home , x , INT_VAL_MIN ) This will start exploring the search space from the minimum possible value of variable x in its domain and try to find solution.(There are many such alternatives .)

对于 z3，我们有这种内置的灵活性吗??任何可能的替代方案??

For z3, do we have this kind of flexibility in-built ?? Any alternative possible??

推荐答案

SMT 求解器通常不允许给出此类提示"，它们更像是黑匣子.

SMT solvers usually do not allow for these sorts of "hints" to be given, they act more as black-boxes.

话虽如此，每个求解器都使用大量内部启发式方法，而 z3 本身具有许多设置，您可以使用这些设置来提供提示.如果你运行:

Having said that, each solver uses a ton of internal heuristics, and z3 itself has a number of settings that you can play with to give it hints. If you run:

z3 -pd

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

it will display all the options you can provide, and there are literally over 600 of them! Unfortunately, these options are not really well documented, and how they impact the solver is rather cryptic. The only reliable way to find out would be to study the source code and see what they do, which isn't for the faint of heart. But in any case, it will not be as obvious as the branch feature you cite for gecode.

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

There are, however, other tricks one can use to speed up solving for SMT-solvers, unfortunately, these things are usually very problem-specific. If you post specific instances, you might get better suggestions.

这篇关于Gecode branch() 函数的 z3 替代方案?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！