z3 - 输入顺序对约束求解器性能的影响
问题描述
输入(布尔和算术方程)顺序对 Gecode 等约束求解器和 Microsoft Z3 等 SMT 求解器是否重要?如果是,如果我可以利用 Gecode 中的分支功能利用一些已知的启发式方法,这两者中的哪一个会表现得更好?
(注:我不知道Gecode中类似branch()的函数是否存在于Z3中)
解决方案
理论上,没有;顺序应该无关紧要。断言的顺序不应该有所作为。但在实践中,它们可能会产生影响,因为启发式方法最终可能会在死胡同中花费大量时间。SMT 求解器通常作为黑盒工作,也就是说,除非您知道它们的确切内部结构,否则很难看到它们的进展情况。但是,您可以调高详细程度(使用 z3 的-v
标志)并可能查看输出以查看是否发现任何不同的行为。
与任何一般的“SMT 求解器性能”问题一样,不可能抽象地回答。每个问题实例都有特定的特征,并且可能有不同的编码方式以使求解器更容易。如果您发布特定问题,您可以获得更好的建议。
推荐阅读
- reactjs - TypeError - undefined 不是一个对象(评估'c.currentObservable.query.refetch')。在本机反应
- unity3d - 为道路系统获得 1x1 大小的地形形状的最佳方法?
- python - 找不到 Heroku Flask Gunicorn 命令
- magento - Magento 2 退款错误 - 交易已被拒绝
- karate - 如何检查响应是否为数组
- c++ - 如何让实例化在我的 OpenGL 程序中工作?
- python - 从 python 运行 libreoffice 本地宏?
- wso2 - WSO2 社区版 - 权利扩展
- aem - 在 AEM 中使用多字段对话框时注入的数据结构不正确
- assembly - 为什么我们在汇编中使用 sub esp, 4 而不是 push a register?