finite set select intersection (Raphael Collet)

[Irene Geary]

Thanks Raph for the helpful suggestion.  Your version is cleaner and 
more complete, although for my particular problem I can't rule out 
empty sets, which weakens the propagation.   I tried a sample run, and 
didn't notice any change in search tree size or significant difference 
in run time, which seems a little surprising.

Anyway, sorry for the delayed response, but I just gave birth to my 
second son on Jan 6th.  :)
Irene


Hi Irene,

Here is a slightly improved definition for SelectPartition.  Your
definition with FD.reified.sum is too weak.  It does not enforce mutual
disjunction between sets in the partition, for instance.  Notice that I
use FD.sumCN in order to avoid the plethora of FD.conj in your
definition.


proc {SelectPartition Sets SelectorSet ResultSet}
    UB Selector Ones
    fun {ListWise Xs Ys} {List.zip Xs Ys fun {$ X Y} [X Y] end} end
in
    %% UB is the union of all upper bounds in Sets
    UB={FS.value.make {Flatten {Map Sets FS.reflect.upperBound}}}
    ResultSet={FS.var.upperBound {FS.reflect.upperBound UB}}

    %% Selector reifies the presence of each set
    SelectorSet={FS.var.upperBound 1#{Length Sets}}
    Selector={FS.reified.areIn 1#{Length Sets} SelectorSet}

    %% I is in ResultSet iff I is in exactly one of the selected Sets
    Ones={Map Sets fun {$ _} 1 end}
    {FS.forAllIn UB
     proc {$ I}
        InResultSet={FS.reified.isIn I ResultSet}
        InSets={Map Sets fun {$ S} {FS.reified.isIn I S} end}
     in
        {FD.sumCN Ones {ListWise Selector InSets} '=:' InResultSet}
     end}

    %% selected sets must be non-empty
    for S in Sets  Sel in Selector do Sel =<: {FS.card S} end

    %% cardinalities
    {FD.sumCN Ones {ListWise Selector {Map Sets FS.card}}
     '=:' {FS.card ResultSet}}
end


Cheers,

raph