CODEWITHSUNDEEP
pythonalgorithmruntimez3z3py
Pravesh Agrawal
Pravesh Agrawal

Reputation: 1

how do we calculate runtime of Z3 sat solver

I am using z3py to solve a set of equations. How would I calculate the runtime order of it? It has bitvecs variables which need to be satisfied in a set of linear equations. The documentation and the guide does not give a way to calculate the runtime.

Upvotes: 0

Views: 698

Answers (1)

Malte Schwerhoff
Malte Schwerhoff

Reputation: 12852

Are you asking for the (worst-case) time complexity of the used solvers? If so, I don't think that you'll be able to get a good answer: it depends on the (combination of) logic(s) into which your problem falls, e.g. QF_BV or UFNIA, and then on the ((semi) decision) procedures that the solver implements for that (combination of) logic(s).

Have a look at papers from the Z3 authors (https://github.com/Z3Prover/z3/wiki/Publications) - they might provide some details.

Upvotes: 1

Related Questions