A constraint domain specifies the rules for constructing constraints for the problem under consideration: it defines the set of values which may be used, and the constants, and functions and relations which may be used to define constraints

A primitive constraint is just a single relation between variables, constants and functions from the constraint domain

A constraint is a conjunction of primitive constraints

There are two special constraints: true (which always holds) and false (which never does); true is the same as an empty constraint

A constraint is satisfiable if there is a valuation which is a solution; otherwise it is unsatisfiable

Two constraints are equivalent if they have the same set of solutions

See section 1.2 of the text.

Another example: John’s electricity supply example 1 (Notes, page 5):

Constraint Domain:

Values: real numbers

Functions: +, -, *, /

Relations: <, £ , =, ³ , >

Constants: 0, the numbers in the table above

Variables: S1C1, S1C2,…, S3C4

Primitive constraints:

S1C1 + S2C1 + S3C1 = 45

Etc (the supply and demand equations)

S1C1 ³ 0

Etc

The overall constraint is the conjunction of the primitive constraints

A valuation is an assignment of values to the variables S1C1 etc

Since it’s possible to come up with valuations which satisfy the constraint, we know the problem is satisfiable.

We don’t (yet) have the language in which to specify that we require the minimum solution (and CLP is probably not the ideal technology to solve this problem anyway).

The most obvious way to determine satisfiability is to enumerate all possible valuations in some order, checking in turn whether each is a solution. But it has problems:

Some domains cannot be enumerated (eg the real numbers)

• Where a domain can in principle be enumerated (eg the rational numbers), it may be difficult, or even impossible, to write an algorithm to guarantee that the enumeration is complete
• In any case, unsatisfiability can’t be determined until the enumeration is complete — which may be never
• Even in finite domains, enumeration is usually unacceptably inefficient

One approach is to transform a constraint into an equivalent one which is easier to solve (and perhaps to do this repeatedly until solution is trivial — a "solved form")

A linear real subterm is either:

• a variable multiplied by a real number
• a real number on its own

A linear term is the sum of linear subterms

A linear equation is an equality between a pair of linear terms

A linear constraint is a conjunction of linear equations (ie the equations are the primitive constraints)

Gauss-Jordan elimination (text, P21) is the process you doubtless learnt at school, of transforming linear real equations by eliminating one real variable for each equation

At the end, the set of constraints C either

• Is empty, in which case every valuation for every variable on the right hand side of the last equation you added to S is a solution
• Contains an equation of the form "r = 0", where r is non-zero (in which case C is unsatisfiable)

Abstractly, trees are built using a tree constructor;

A tree constructor is simply an operation which constructs new trees out of ordered lists of other trees:

A tree of height 1 is simply a constant from the base domain

A tree of height n > 1 consists of a tree constructor applied to a list of trees of height < n

The text gives examples of tree construction in C, prolog and (something like) lisp

Finally, terms are in essence trees which may contain variables

Primitive tree constraints assert the equality of two tree terms

The algorithm on P26 (unification) is a solver for tree constraints

The set of values for a Boolean domain is just {true, false}

The function symbols are simply and (&), or (v) and not(~) (the text refers to other operations, which however may be defined in terms of these)

(Usually) the only predicate symbol is equality

Since Boolean domains are finite, there are complete solvers: enumeration solvers (known as truth table solvers)

However they run in time exponential in the number of variables (and there is good reason to believe that it is unlikely to be possible to do better)

However if we are only interested in satisfiability, not unsatisfiability, then simply randomly guessing valuations can be a way of finding a solution

The solver given on page 30 transforms the given problem into a particular form called Conjunctive Normal Form (CNF); it then bounds its search in such a way that the probability of not finding a solution is bounded (on the assumption that the CNF is randomly chosen from the set of all CNFs)

We can think of sequence constraints as a special form of tree constraint, in which the right hand branch of each subtree is empty (or alternatively, you can read the account on P32)

The discussion on Pp32 and 33 of the text isn’t completely careful about what the domain is, so there is some confusion as to exactly what the variables stand for

We can probably work with it as stands in the book for now, but you need to be aware that to fully formalise this in the terms of section 1, we would need to consider it as an extension of the earlier boolean constraint problem, in which the items which are true or false are now more complex things like red(X) or on(X,Y)

If true is returned, C must be satisfiable

If false is returned, C must be unsatisfiable.

That is, the order of the primitives in C does not affect the value of solv(C)

That is, if solv(C1) is false, then so is solv(C1 ^ C2)

If C2 is a (renaming) variant of C1, then solv(C1) = solv(C2)

For some problems, there are practical, complete solvers (we’ve already seen some)

For most problems, it may either be provably impossible to define a complete solver, or impractical (in the sense that the solver would be unacceptably inefficient)

Thus we typically are prepared to accept incomplete solvers