Is branching necessary when proving a sum of non-negative terms?

Consider an inequality system of N inequalities and N variables a1..aN of uninterpreted sort:

(a1==a1 ? 1 : 0) + ... + (a1==aN ? 1 : 0) >= 1
(a2==a1 ? 1 : 0) + ... + (a2==aN ? 1 : 0) + (a2==a1 ? -1 : 0) >= 1
...
(aN==a1 ? 1 : 0) + ... + (aN==aN ? 1 : 0) + (aN==a1 ? -1 : 0) + ... + (aN==a(N-1) ? -1 : 0) >= 1

This inequality system has a property that for each term that has -1 in it, there is a term with 1 that has exactly the same guard (for example, a2==a1 in the second inequality). This property allows regrouping the terms in such a way that each summand is guaranteed to be non-negative. Also, each inequality contains a term whose guard is trivially true (for example, a1==a1 in the first equality). Therefore, we can conclude that the inequalities are guaranteed to always hold without branching on whether any of the variables a1..aN are equal to each other.

Here is an encoding of the inequality system for N=3 into smt2 (auto_config false does not seem to have an effect here, but I added it because we need it for the more general problem):

(set-option :auto_config false)
(declare-sort Address 0)
(declare-fun a1 () Address)
(declare-fun a2 () Address)
(declare-fun a3 () Address)
(assert
   (not
      (and
         (<= 1.0 (+ (ite (= a1 a1) 1.0 0.0) (ite (= a1 a2) 1.0 0.0) (ite (= a1 a3) 1.0 0.0)))
         (<= 1.0 (+ (ite (= a2 a1) 1.0 0.0) (ite (= a2 a2) 1.0 0.0) (ite (= a2 a3) 1.0 0.0) (ite (= a2 a1) (- 1.0) 0.0)))
         (<= 1.0 (+ (ite (= a3 a1) 1.0 0.0) (ite (= a3 a2) 1.0 0.0) (ite (= a3 a3) 1.0 0.0) (ite (= a3 a1) (- 1.0) 0.0) (ite (= a3 a2) (- 1.0) 0.0)))
      )
   )
)
(check-sat)

If I run Z3 with different N, I get that it scales exponentially. If I check the trace generated with trace=true proof=true, I see many [push] and [pop] entries, which (as far as I understand) mean that Z3 branches.

My question is: is there a configuration option I could enable or additional contraints I could add to help Z3 to avoid branching?

I tried the following:

Assuming that variables a1..aN are different from each other.
Rearranging the terms into non-negative groups (putting them under the same guard).
Asserting that groups are non-negative.
Both 2 and 3 together.

All of these changes improve the scalability, but the runtime still remains exponential.

A side note: the general problem I am trying to solve almost always involves quantifiers and more complex arithmetic expressions, but it is always guaranteed that the terms can be groupped into non-negative groups.

Solution

Since your constraints, as stated, do not restrict the search space at all, I don't think you can do any better than this.

This sort of "cardinality" problems are actually best addressed with:

Use QF_LIA
Express your constraints using pseudo-boolean predicates. Search for the phrase "Pseudo-boolean" in https://theory.stanford.edu/~nikolaj/programmingz3.html.

But these tricks will only help if you actually had constraints that limited the search space in some way. They might still be worth a try though. Since you presented an abstract version of your problem, it's hard to opine on the applicability to your real issue.