CODEWITHSUNDEEP
z3smtz3py
Yi Zhao
Yi Zhao

Reputation: 346

General principles and directions to accelerate the solving of Z3 problem

I am using Z3 to solve a problem and I find it is very slow. Are there any general principles or guidelines about the acceleration of Z3 solver? Such as:

  1. Try to reduce the number of constraints.
  2. Try specifying the tactics.
  3. ...

Upvotes: 1

Views: 531

Answers (2)

alias
alias

Reputation: 30525

As Christoph mentioned, there's no "one-size-fits-all" advice that applies uniformly to all problems. However, this sort of performance question comes up often enough, and there has been previous discussion on stack-overflow with a summary of how to think about scalability before: Scalability of z3

I'd start by reviewing this answer, and see if you have specific questions. In particular, sharing the particulars of your actual problem and how you modeled it in z3 will be essential to get better guidance.

Upvotes: 1

Christoph Wintersteiger
Christoph Wintersteiger

Reputation: 8392

There are no generally applicable rules; otherwise we would have implemented and automated them. Without further information about the problem, there is no way to help you. A good place for performance investigations is a Z3 GitHub discussion.

Upvotes: 1

Related Questions