Don't say SAT. That refers to a very particular decision problem that is known to be NPC. This problem may or may not be similar (we'll see).

(Also: someone check my argument here just to make sure I'm not full of ****. Thanks!)

To approach this I would consider atomic formulas and work my way up. Iff there's an effective procedure to calculate the answer without running forever for some case, it should be decidable. Since there are no function symbols, this is a relational language without equality. For each predicate in the discourse P(<x0, x1, x2,...>) (where x0, x1, x2, ... can only be atomic objects), there will be an assignment of true or false to the result. To a limited extent, we can model functions with equality by using predicates. For example, I can define + by defining triples where a + b = c: {(0, 0, 0), (0, 1, 1), (1, 0, 1), (1, 1, 2), ... }. The problem is I can't define + so that it can taketerms, unless I allow for an infinite number of predicates to handle every possible equation (and without function symbols I would need an infinite language, which is generally not allowed unless expressly stated).

The question is, can we decidably answer "there exists x with property P" in this restricted language? Well, each evaluation of P(<a>) for some P and some finite sequence of x is an atomic operation that takes constant time to determine (by table lookup), so will be linear by the number of predicates appearing. The only thing that takes variable amounts of time to perform is the evaluation of each of the logical connectives. This is already known to be decidable by Godel's completeness theorem, since completeness applies to a complete set of logical connectives and therefore also applies to any incomplete subset.

You should be able to frame any SAT sentence as en existentially-bounded sentence in a vocabulary where each variable is a predicate or its inverse, and an additional predicate keeps those two mutually separate. You have to design the vocab after the fact but that's not a problem since we're trying to prove something aboutanyexistentially-bounded sentence. Similarly, you should be able to translate any existentially-bounded sentence into SAT, by trading predicates for variables. Both of these translations can be done in polynomial time (this is intuitive but not hard to show).

So existentially-bounded first-order sentences are reducible to SAT and vice versa, which means they are NPC, and thus they fall within EXPTIME. However, NP is not known to be a strict subset of EXPTIME (this is widely believed but not proven) so it is possible it may be EXPTIME-complete for all we know.