Vocabulary RevisitedMore Advanced Topics
You will have noticed that every time we define a predicate or function symbol we append a pair of braces. You may even suspect that there is a reason for this, that it probably has to do with stuff that can be written between the braces, and that it is there to make life more complicated. All of this is true except for the last bit. It is there to make life simpler!
Every symbol declared in the “Vocabulary” box comes with a set of properties. Some are logical properties: for example, in the Four Spies and the Inconsequential Seminars problems, the functions were stipulated to be “all_different”. Others are to do with presentation: for example, we may add a stipulation to suppress printing of a particular item when the models are reported. The options are:
total or partial (default: total)
Total functions have a value for every possible argument. Partial functions may be undefined for certain arguments. See below for more explanation and examples. Predicates and names may also be declared partial.
all_different (may be written injective)
Injective functions are such that no two arguments give the same value. This is sometimes called an “all-different” constraint on the function, because the values (for different arguments) are all different. Most injective functions in normal cases have just one argument, but injectiveness can also make sense where there are two or more arguments.
surjective
Function f is surjective if for every possible value y there is at least one x such that f(x) = y. An injective function between two sorts of equal size is automatically surjective, and vice versa. The solver can work this out for itself: if a function is declared “all_different” and the sorts involved are of the same cardinality, the “surjective” flag is turned on automatically.
commutative
A binary function f is commutative if it satisfies the condition
∀x ∀y ( f(x,y) = f(y,x) ).
More generally, the annotation “commutative” means that the order of arguments of the function is irrelevant, so it can also be applied to functions with more than 2 arguments. Predicates may also be declared commutative, meaning that the relations they symbolise are symmetric – i.e. again that the order of arguments is irrelevant.
scope: N (default scope 5)
The ranking of this symbol for purposes of reducing the number of parentheses. See the section below on notation. Small numbers mean narrow scope. Pre-defined binary connectives like “AND” have scope 10 (the maximum), and pre-defined relations like “=” have scope 9. Quantifiers, however, have minimal scope, as do all unary operators including negation. If you are not sure of the scope conventions, put in the parentheses: these can never do any harm!
print: full or print: none (default print: full)
“Full” means the value of the name, predicate or function is to be printed. “None” suppresses printing.
cut or no_cut (default no_cut)
Controls backtracking in the sense that the most significant difference (i.e. the first in the declaration order of vocabulary items) between two solutions may not be in a symbol on which a cut has been placed. For logic puzzles this is rarely needed and can cause unexpected results, so it is probably best avoided.
hidden
This is much more commonly used. It is a synonym for “print:none cut”, which also moves the hidden functions to the end of the declaration order and gives non-hidden functions priority over them. It suppresses printing of the function and ensures that no two solutions differ only on hidden variables. Placing a “no_cut” after the “hidden” undoes the effects except for suppressing printing.
priority or no_priority (default no_priority)
If a function (or predicate or name) f is declared with priority, after the solver sets its value it will search for solutions by trying different values for the symbols declared below f, and will not backtrack to change the value of f (or anything above it) until that part of the search space is exhausted. There are two main uses for this: it may be used to assign values to the most important symbols first and then let the values of other things fall into place. This can (sometimes) improve the efficiency of the search. It may also be used to ensure that the first solution found will be one that minimises the value of a particular item, by declaring that one first with priority. This can force the solver to return a solution that is optimal in some sense. For logic puzzles the priority toggle is rarely needed and best avoided.