About solver speed

[carbonium14]

We are using a solver to solve a procedural synthesis problem, but it's running really slow. I don't know if it's a problem with the solver or a problem with our coding.

1. What is the time complexity of the solver? In previous tests, we generated about two thousand expressions, and the solution time was between 10 seconds and 30 seconds. This is a simplified result, but it is too time-consuming. If the problem is more complex, the solution time may be It can take dozens of minutes or even hours. So our question is, how many expressions can the solver solve in a certain amount of time, in other words, what is the time complexity?
2. Are there any configuration options for the solver that can speed things up? In issue263, we used Array for solving. We guessed that there may be some configuration options that can speed up the solver's solution. However, after checking the documentation, we did not find the corresponding configuration. So do these configurations exist? If it exists, how can it be configured to speed up the solver?

[Pat-Lafon]

I saw this issue again, unfortunately I'm not sure this is the right venue for these kinds of questions:

• It depends on the logic you are working with and it's complexity. In the worst case, you are solving an undecideable NP-Complete problem and the time complexity is exponential. Hopefully/most likely you are working in a decideable/semi-decidable theory with a better time complexity. The simplest version of this is the theory of equality which is linear.
• Possibly? I'm not so well versed with the knobs you can turn here. Usually, the answer is to find a way to better encode your problem such that the solver has an easier time. Depending on the domain, this might require an expert. I'm not sure I can be of much help.

[carbonium14]

Thank you for your reply. This issue has been going on for a long time and we have found a corresponding solution. There is no problem with z3, and the solving speed is not particularly slow. The problem lies in the architecture of our program. When we reduce unnecessary component calculations and minimize duplicate calculations caused by immutable variables in componentized program synthesis, the speed improves significantly. Finally, thank you again for taking the time to answer my question.