本文介绍了z3:是否可以调整Z3中的分支启发法?的处理方法,对大家解决问题具有一定的参考价值,需要的朋友们下面随着小编来一起学习吧!

问题描述

这是

鉴于Z3使用DPLL算法.假设我对哪些变量更为关键有所了解.评估逻辑问题时,是否可以让Z3解算器首先分支这些变量,以提高性能或效率?

Given that Z3 uses DPLL algorithms. Suppose I have some knowledge about which variables are more critical. Is it possible that I make Z3 solver to branch on these variables first when evaluating my logic problem so as to boost the performance or efficiency?

推荐答案

这是可能的,但是目前没有方便的界面.您必须稍微修改一下源代码,但是如果您真的知道必须首先在特定变量上进行分支,那么值得付出努力.

This is possible but there is no convenient interface for it at the moment. You'd have to hack the source code a bit, but if you really know that you have to branch on particular variables first it may be worth the effort.

这篇关于z3:是否可以调整Z3中的分支启发法?的文章就介绍到这了,希望我们推荐的答案对大家有所帮助,也希望大家多多支持!

07-23 15:24
查看更多