X2 - Y2 = Z2 X + Y + Z < U X + Y 5 . Z
X1,..., X9 are pairwise distinct
A domain constraint (also called basic constraint) takes the form x D, where D is a finite domain.
A finite domain problem is a finite set P of quantifier-free constraints such that P contains a domain constraint for every variable occurring in a constraint of P. A variable assignment is a function mapping variables to integers.
A solution of a finite domain problem P is a variable assignment that satisfies every constraint in P.
Notice that a finite domain problem has at most finitely many solutions, provided we consider only variables that occur in the problem (since the problem contains a finite domain constraint for every variable occurring in it).
Andreas Rossberg 2006-08-28