Можно ли оценить время работы z3 или время работы алгоритма DPLL (T)? Даже худший случай

Question

Я работаю над визуализацией прототипа microsoft z3. Интересно, можно ли оценить время работы z3 или алгоритм? Даже было бы здорово, если бы я мог получить худшее время работы.

Кроме того, в z3 существует ли какой-либо способ получить время работы каждого процесса проверки с помощью решателя теории?

Спасибо за ответ.

Answer 1

Это невозможно вообще. SAT является NP-полной проблемой, а SMT по крайней мере такой же сложной, как SAT.