16.3.7 Solution Predicate

The functional procedure MakePredicate inputs a dominance constraint and computes a solution predicate for it which in turn can be explored by encapsulated search, e. g. Search.all or Explorer.all.

The input dominance constraint - the graph - comes as a record which contains the number of nodes N, i.e. the number of variables in the input constraint, and a procedure P which represents the dominance constraint itself. Recall that such a procedure takes a list of node representations of length N and imposes the set constraints encoding the dominance constraint.

A search predicate always has the same form: it is a unary predicate whose argument denotes a solution. First it posts all constraints on the solution, then it specifies a search/distribution strategy:

<DC: make predicate>=

fun {MakePredicate 'unit'(domCon:DomCon vars:N)}  
   proc {$ Nodes}  
     <DC: create nodes>  
     <DC: translation to set constraints>  
     <DC: impose treeness>  
   in 
     <DC: distribute> 
   end  
end

The solution Nodes must be a list of N nodes. Each variable is represented by a distinct integer between 1 and N. Thus sets of variables can be represented by sets of integers. (We store the specification of the finite domain from 1 to N in the variable VDom.) For each variable, MakeNode creates a term representing the node that is the interpretation of this variable.

<DC: create nodes>=

VDom = [1#N]
{List.make N Nodes}   % constrains Nodes to a list
                      % [_ ... _] of length N
for Node in Nodes I in 1..N do {MakeNode I VDom Node} end

Then we constrain these nodes using the procedure DomCon that implements the dominance constraint. After this we execute choice skip end whose only effect is to wait for stability; i. e. until constraint propagation has inferred as much as it could. Typically the dominance constraint DomCon provides very strong constraints and it is a good idea to impose them first and wait until they have achieved full effect before going on with the quadratic number of expensive treeness constraints.

<DC: translation to set constraints>=

{DomCon Nodes}
% waits for stability
{Space.waitStable}

Now we impose the treeness constraint between every pair of nodes Ni and Nj. For every such pair we impose a choice which is controlled by its own choice variables with domain [1..4]. We collect the quadratic number of choice variables within the list ChoiceVariables.

<DC: impose treeness>=

ChoiceVariables =
{List.foldRTail Nodes
 fun {$ Ni|Ns Cs}
    {List.foldR Ns
     fun {$ Nj Cs}  
        <DC: treeness condition between Ni and Nj> 
        C|Cs
     end Cs}
 end nil}

Finally, we specify the distribution strategy: here we use First Fail on the choice variables. Each choice variable is a finite domain variable in [1..4]. First fail is a strategy which attempts to minimize the branching factor in the search tree: it picks a (non-determined) variable with the minimum number of remaining possible assignments.

<DC: distribute>=

{FD.distribute ff ChoiceVariables}