我正在制作一个微软z3的原型。我想知道是否可以估计z3的运行时间或算法？如果我能得到一个最坏的运行时间那就太好了。
此外，在z3中，是否有任何方法可以通过理论求解器得到每个检查过程的运行时间？
谢谢你的回答。
最佳答案
总的来说这是不可能的。SAT是一个NP完全问题，SMT至少和SAT一样难。
关于algorithm - 是否可以估计z3的运行时间或DPLL(T)算法的运行时间？即使是最坏的情况，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/38878804/