2.1 Finite Domains and Constraints

A finite domain is a finite set of nonnegative integers. The notation m\# n stands for the finite domain m,\ldots,n.

A constraint is a formula of predicate logic. Here are typical examples of constraints occurring with finite domain problems:

\begin{array}{rcl}
&X=67
\qquad
X\in0\#9
\qquad
X=Y\\
&X^2-Y^2=Z^2
\qquad
X+Y+Z<U
\qquad
X+Y\neq5\cdot Z\\
&X_1,\ldots,X_9\;\hbox{are pairwise distinct}
\end{array}

domain constraints

A domain constraint takes the form x\in D, where D is a finite domain. Domain constraints can express constraints of the form x=n since x=n is equivalent to x\in n\#n.

basic constraints

A basic constraint takes one of the following forms: x=n, x=y, or x\in D, where D is a finite domain.

finite domain problems

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.

solutions

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).


Christian Schulte and Gert Smolka
Version 1.4.0 (20080702)