z3 的可扩展性 [英] Scalability of z3

问题描述

我想提高 SMT 求解的可扩展性.我实际上已经实现了增量求解.但我想提高更多.在不了解问题本身的情况下，还有其他一般方法可以改进它吗?

I would like to improve the scalability of SMT solving. I have actually implemented the incremental solving. But I would like to improve more. Any other general methods to improve it without the knowledge of the problem itself?

推荐答案

没有单一的技巧"可以让 z3 更好地解决任意问题.这实际上取决于实际问题是什么以及您有什么样的限制.当然，这适用于任何一般计算问题，但它确实适用于 SMT 求解器的上下文.

There's no single "trick" that can make z3 scale better for an arbitrary problem. It really depends on what the actual problem is and what sort of constraints you have. Of course, this goes for any general computing problem, but it really applies in the context of an SMT solver.

话虽如此，以下是基于我的经验的一些总体思路，大致按照易用性的顺序:

Having said that, here're some general ideas based on my experience, roughly in the order of ease of use:

阅读 Programming Z3 一书 这是一篇非常好的文章，将教您大量有关 z3 的架构以及最佳习语的知识.您可能会遇到直接适用于您的问题的内容:https://theory.stanford.edu/~nikolaj/programmingz3.html

将布尔值保留为布尔值而不是整数 切勿使用整数来表示布尔值.(也就是说，使用 1 表示真，0 表示假；乘法表示 and 等等.这是一个可怕的想法，它扼杀了强大的 SAT 引擎在下面.)如有必要，显式转换.人们倾向于使用此类技巧的大多数问题都涉及计算有多少布尔值为真等:此类问题应该使用求解器内置的伪布尔策略来解决.(查找pbEq、pbLt等)

Keep booleans as booleans not integers Never use integers to represent booleans. (That is, use 1 for true, 0 for false; multiplication for and etc. This is a terrible idea that kills the powerful SAT engine underneath.) Explicitly convert if necessary. Most problems where people tend to deploy such tricks involve counting how many booleans are true etc.: Such problems should be solved using the pseudo-boolean tactics that's built into the solver. (Look up pbEq, pbLt etc.)

除非绝对必要，否则不要优化 优化引擎不是增量式的，也不是优化得很好(双关语).与所有其他引擎相比，它的工作速度相当慢，这是有充分理由的:优化模理论是一件非常棘手的事情.除非您真的有优化问题需要解决，否则请避免使用它.您还可以尝试在求解器的外部"进行优化:进行 SAT 调用，获取结果，然后进行后续调用，要求更小"的成本值.使用此技巧您可能无法达到最佳值，但经过几次迭代后，这些值可能已经足够好了.当然，结果如何完全取决于您的问题.

Don't optimize unless absolutely necessary The optimization engine is not incremental, nor it is well optimized (pun intended). It works rather slowly compared to all other engines, and for good reason: Optimization modulo theories is a very tricky thing to do. Avoid it unless you really have an optimization problem to tackle. You might also try to optimize "outside" the solver: Make a SAT call, get the results, and making subsequent calls asking for "smaller" cost values. You may not hit the optimum using this trick, but the values might be good enough after a couple of iterations. Of course, how well the results will be depends entirely on your problem.

案例拆分 尝试通过对关键变量进行案例拆分来减少约束.示例:如果您正在处理浮点约束，请说；分别对正常、非正常、无穷大和 NaN 值进行大小写拆分.根据您的特定领域，您可能有这样的语义类别，其中底层算法采用不同的路径，混合和匹配它们总是会给求解器带来困难.基于上下文的案例拆分可以加快速度.

Case split Try reducing your constraints by case-splitting on key variables. Example: If you're dealing with floating-point constraints, say; do a case split on normal, denormal, infinity, and NaN values separately. Depending on your particular domain, you might have such semantic categories where underlying algorithms take different paths, and mixing-and-matching them will always give the solver a hard time. Case splitting based on context can speed things up.

使用更快的机器和更多的内存这是不言而喻的；但是拥有足够的内存确实可以加快某些问题的速度，尤其是当您有很多变量时.获得最大的机器！

Use a faster machine and more memory This goes without saying; but having plenty of memory can really speed up certain problems, especially if you have a lot of variables. Get the biggest machine you can!

利用您的内核您可能拥有一台具有多个内核的机器，而且您的操作系统很可能提供细粒度的多任务处理.利用这一点:启动 z3 的许多实例来解决相同的问题，但使用不同的策略、随机种子等；并取第一个完成的结果.如果您有一个巨大的约束集，随机种子可以发挥重要作用，因此运行更多具有不同种子值的实例可以让您平均幸运".

Make use of your cores You probably have a machine with many cores, further your operating system most likely provides fine-grained multi-tasking. Make use of this: Start many instances of z3 working on the same problem but with different tactics, random seeds, etc.; and take the result of the first one that completes. Random seeds can play a significant role if you have a huge constraint set, so running more instances with different seed values can get you "lucky" on average.

尝试使用并行求解 大多数 SAT/SMT 求解器算法本质上都是顺序的.已经有许多关于如何并行化某些算法的论文，但大多数引擎没有并行对应物.z3 有一个用于并行求解的接口，尽管它的广告较少且相当挑剔.试一试，看看它是否有帮助.详细信息在这里:https://theory.stanford.edu/~nikolaj/programmingz3.html#sec-parallel-z3

Try to use parallel solving Most SAT/SMT solver algorithms are sequential in nature. There has been a number of papers on how to parallelize some of the algorithms, but most engines do not have parallel counterparts. z3 has an interface for parallel solving, though it's less advertised and rather finicky. Give it a try and see if it helps out. Details are here: https://theory.stanford.edu/~nikolaj/programmingz3.html#sec-parallel-z3

配置文件 配置 z3 源代码本身，因为它在您的问题上运行，并查看热点在哪里.看看您是否可以向开发人员推荐代码改进来解决这些问题.(更好的是，提交拉取请求！)不用说，这需要对 z3 本身进行深入研究，可能不适合最终用户.

Profile Profile z3 source code itself as it runs on your problem, and see where the hot-spots are. See if you can recommend code improvements to developers to address these. (Better yet, submit a pull request!) Needless to say, this will require a deep study of z3 itself, probably not suitable for end-users.

底线:天下没有免费的午餐.没有一种方法可以让 z3 更好地解决您的问题.但上述想法可能有助于改善运行时间.如果您详细描述您正在处理的特定问题，您很可能会得到更好的建议，因为它适用于您的限制条件.

Bottom line: There's no free lunch. No single method will make z3 run better for your problems. But above ideas might help improve run times. If you describe the particular problem you're working on in some detail, you'll most likely get better advice as it applies to your constraints.

这篇关于z3 的可扩展性的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！