是否可以估计z3的运行时间，或DPLL（T）算法的运行时间？即使是最坏的情况

Question

我正在研究可视化 microsoft z3 的原型。我想知道是否可以估计z3或算法的运行时间？如果我能得到最坏情况下的运行时间，那就太好了。

另外，在z3中，有没有什么方法可以通过理论求解器获取每个检查过程的运行时间？

感谢您的回答。

Answer 1

一般情况下是不可能的。 SAT 是一个 NP 完全问题，SMT 至少和 SAT 一样难。