CODEWITHSUNDEEP
algorithmz3smt
Steven
Steven

Reputation: 13

Is it possible to estimate the running time of z3, or the running time of DPLL(T) algorithm? Even the worst case

I am working on visualize a prototype of microsoft z3. I wonder if it is possible to estimate the running time of z3 or the algorithm? Even it would be great if I could get a worst case running time.

Also, in z3, is there any method to get the running time of each checking process by theory solver?

Thanks for answer.

Upvotes: 0

Views: 256

Answers (1)

sean
sean

Reputation: 1832

It's not possible in general. SAT is an NP-complete problem, and SMT is at least as hard as SAT.

Upvotes: 1

Related Questions