In many programming languages, branching efficiency is dependent on the order in which the clauses are provided. E.g., in Python,
if p or q :
will branch into the if statement as soon as p evaluates to true, so it is generally a good idea to provide computationally light clauses first. I'm wondering if the same is true for satisfiability checking in Z3. In other words, is there any difference between checking And(P, Q) and And(Q, P), provided that one of the formulas is significantly more complex than the other?
Yes, it make can make a difference what order you specify the clauses. However, there is probably not much to be gained by rearranging the clauses when it comes to Z3. Also, it might be difficult (and perhaps not worth your while) to determine a generic "optimal order" beforehand.
With other SMT solvers, I have observed what you are describing in an extreme fashion. With some solvers, it can make or break the computation, in the sense that I have seen certain cases where a solver times out when the clauses are presented in one order, but quickly finds a solution when the same clauses are presented in a different order. However, to me, this is an indication of a poorly designed solver. Z3 and other modern SMT solvers such as CVC4 are much less vulnerable to this kind of problem than older or less robust SMT solvers.
Regarding actually finding the optimal ordering, what constitutes "computationally light" or "more complex" for an SMT solver is different than a traditional computer language. What really matters is whether or not a certain clause in a conjunction is likely to lead to a conflict, or whether a particular clause in a disjunction is likely to lead to a solution. This is akin to trying to find your way out of a maze -- if you make a wrong turn early on, then you might spend a long time following a dead end, before you finally decided to go back to the beginning and take a different branch. Again, modern SMT and SAT solvers have techniques for mitigating this.
Also, When it comes to Z3 specifically, if Z3 could be made more efficient in real-world applications by sorting the clauses in terms of some human-understandable and generic measure of complexity, then that has probably already added as a pre-processing step to Z3. In general, for such complicated optimization questions where there are multiple factors at play (e.g. the particulars of the Z3 implementation) you have to try multiple things and benchmark over a suite of test examples relevant for your application.
As a bit of evidence for some of my claims above, I wrote this little example SMT problem:
(declare-fun p () Int)
(declare-fun q () Int)
(declare-fun n () Int)
(assert (> p 1))
(assert (> q 1))
(assert (and (= n 18679565357) (= n (* p q))))
(check-sat)
(get-value (p q n))
(exit)
Swapping the order of the clauses in the and statement makes very little difference on my system (less than 1%). If I break it up into two separate assertions, then the difference is larger, but to know if this difference holds in general (across different SMT problems of this class) I would have to run a benchmark suite with many such problems.