CODEWITHSUNDEEP
z3z3py
Jenni
Jenni

Reputation: 121

Performance issues with z3py using modulo and optimization

I'm experimenting with Z3 (using the python api) where I'm building up a scheduling model for a class assignment, where I have to use modulo quite often (because its periodic). Modulo seems already to slow down z3 by a lot, but if I try do some optimization on top (minimize a cost function which is a sum), then it takes quite some time for fairly small problems.

Without optimization it works okayish (few seconds for a smaller problem). So that being said, I have now 2 questions:

1) Is there any trick with the modulo function of how to use it? I already assign the modulo value to a function. Or is there any other way to express periodic/ring behavior?

2) I am not interested in finding THE best solution. A good one, will be good enough. Is there a way to set some bounds for the cost function. Like, if know the upper and lower bound of it? Any other tricks, where I could use domain knowledge to find solutions fast. Furthermore, I thought that if I ll use timeout option solver.set("timeout" 10000), then the solver would time out with the best solution so far. That doesnt seem to be the case. It just times out.

Upvotes: 2

Views: 488

Answers (2)

Malte Schwerhoff
Malte Schwerhoff

Reputation: 12852

Instead of using the built-in modulo and division, you could introduce uninterpreted functions mymod and mydiv, for which you only provide the necessary axioms of division and modulo that your problem requires. If I remember correctly, Microsoft's Ironclad and/or Ironfleet team did that when they had modulo/division-related performance problems (using the pipeline Dafny -> Boogie -> Z3).

Upvotes: 1

alias
alias

Reputation: 30418

Impossible to comment on the mod function without seeing some code. But as a rule of thumb, division is difficult. Are you using Int values, or bit-vectors? If you are using unbounded integers, you might want to try bit-vectors which might benefit from better internal heuristics. Or try Real values, and then do a proper reduction.

Regarding how to get the "best so far" optimal value, see this answer: Finding suboptimal solution (best solution so far) with Z3 command line tool and timeout

Upvotes: 1

Related Questions