Sturm chain analogue for exponential polynomials?

Question

I'm going to define an exponential polynomial of degree $k$ as a function $f$ of the form

$f(x) = \sum_{i=1}^k c_ie^{\alpha_ix}$ ($\alpha_i$s real).

My first question is: is there an algorithm for counting the number of real roots of such an expression, with complexity depending only on the degree $k$?

I strongly suspect that the answer to this question is yes, and that the answer is known (seeing as Tarski's exponential function problem is all but solved), but I can't find it described anywhere.

My second question is: can somebody tell me what this algorithm is? Or give me a hint?

I vaguely remember reading somewhere that there was a known method analogous to the method of Sturm chains for polynomials... But I haven't been able to figure out what it should be, nor have I been able to find where I read that claim. My best guess is that we can get rid of terms of such an expression by first dividing $f$ by an exponential $e^{\alpha x}$ to make a term constant, differentiating, and then multiplying by that same exponential. If we call this operation $D_{\alpha}$, we get $D_{\alpha}f(x) = \sum_{i=1}^k c_i(\alpha_i-\alpha)e^{\alpha_ix}$. The nice thing is that $D_{\alpha}f$ acts analogously to the derivative of $f$, i.e. between any consecutive zeroes of $f$ there is a zero of $D_{\alpha}f$. The problem is that I can't think of a good analogue to the division algorithm for exponential polynomials (maybe we don't need one?).

Edit: When I say that Tarski's exponential function problem is "all but solved," I mean that all that is missing from the full solution is a proof of Schanuel's conjecture. I'm not saying that Schanuel's conjecture is easy, but given this result it seems to me that we should be able to describe some sort of explicit algorithm for deciding problems like this one, although the proof of correctness of such an algorithm might require us to assume Schanuel's conjecture holds.

Answer 1

Tarski's problem is not all but solved, or at least not last I checked. Precisely, the gap between Wilkie's theorem and solving Tarski's problem is decidability of exponential systems, for which the best result so far as been that Wilkie and Macintyre showed it was true if you assume that the Schanuel conjecture holds. So if decidability is not known, let's not even get into counting!

Of course, this does not mean that we have to be pessimistic about your question, since you restricted yourself to the single variable case. I don't believe there is currently such a result, at least in full generality.

Added Later: If we do assume Schanuel's Conjecture, there is a recent algorithm for root isolation (thus I suppose for counting as well). This is the reference I was able to find (I have not read it yet):

Real root isolation for tame elementary functions
Adam Strzebonski, Wolfram Research Inc.
In ISSAC '09
https://doi.org/10.1145/1576702.1576749

The abstract hits all the important points: it's univariate-only, and relies on Schanuel's conjecture to determine the signs of certain expressions.

Answer 2

Wilkie's proof of o-minimality of exponentiation tells you (without needing to assume Schanuel's Conjecture) that for each $k$ there is a bound $M_k$ such that any exponential polynomial $\sum_{i=1}^k c_ie^{\alpha_i x}$ has at most $M_k$ real zeros [assuming that the $c_i$ and $\alpha_i$ are real.]

Perhaps Khovanskii's work gives an explicit bound on the $M_k$.