On the computational limits of infinite satisfaction

We study the computational limits of Constraint Satisfaction Problems (CSP's) allowing infinitely, or unboundedly, many indexed variables as in, e.g., X _i > x _i+2 for each i = 1, 2, .... We refer to these CSP's as Infinite CSP's (ICSP's). These problems arise in contexts in which the number of variables is unknown a priori as well as in optimization problems wit the number of variables satisfying a given finite set of constraints. In particular, we investigate the decidability of the satisfiability problem for ICSP's wrt (a) the first-order theory specifying the indices of variables and (b) the dimension of the indices. We first show that (1) if the indices are one-dimensional and specified in the theory of the natural numbers with linear order (the theory of (ℕ, 0, succ, <)) then the satisfiability problem is decidable. We then prove that, in contrast to (1), (2) if we move to the two-dimensional case then the satisfiability problem is undecidable for indices specified in (ℕ, 0, succ, <) and even in (ℕ, 0, succ). Finally, we show that, in contrast to (1) and (2), already in the one-dimensional case (3) if we also allow addition, we get undecidabili.ty. I.e., if the one-dimensional indices are specified in Presburger arithmetic (i.e., the theory of (ℕ, 0, succ, <, +)) then satisfiability is undecidable.