exception FalseInput; fun steiner n space = if ((n mod 6) = 1) orelse ((n mod 6) = 3) then let val n' = (n *(n - 1)) div 6 val ss = List.tabulate(n',(fn x => FS.upperBound(space,#[(1,n)]))) fun intersect(space,[y])= () | intersect(space,y::ys)= (List.app(fn x => let val tmp = FS.setvar space in (FS.relOp(space,y,FS.INTER,x,FS.SEQ,tmp); FS.cardRange(space,0,1,tmp)) end) (ys);intersect(space,ys)) in List.app(fn x => FS.cardRange(space,3,3,x))ss; intersect(space,ss); FS.setvarbranch(space,Vector.fromList ss, FS.FSB_NONE,FS.FSB_MIN); ss end else raise FalseInput
Solving the Steiner problem of order 9 by invoking the Alice Explorer
Explorer.exploreOne(Steiner 9)yields as solution
{ss = [setvar{| < 1..3 > (3)|}, setvar{| < 1, 4..5 > (3)|}, setvar{| < 1, 6..7 > (3)|},The search tree has 4529 choice nodes, and 4505 failure nodes.mathend000#
setvar{| < 1, 8..9 > (3)|}, setvar{| < 2, 4, 6 > (3)|}, setvar{| < 2, 5, 8 > (3)|},mathend000#
setvar{| < 2, 7, 9 > (3)|}, setvar{| < 3..4, 9 > (3)|}, setvar{| < 3, 5, 7 > (3)|},mathend000#
setvar{| < 3, 6, 8 > (3)|}, setvar{| < 4, 7..8 > (3)|}, setvar{| < 5..6, 9 > (3)|}]}mathend000#
N1 * N1 * y1mathend000# + N1 * y2 mathend000# + y3 < mathend000# N1 * N1 * x1 mathend000# + N1 * x2 mathend000# + x3 mathend000#.
let val n1 = n + 1 val n1n1 = n1 * n1 val ivarlist = List.map(fn x => let val tmp = FD.rangeVec(space,3,(1,n)) in (FS.match(space,x,tmp);Vector.toList tmp) end)(ss) fun redundantconstr(s,[y]) = () | redundantconstr(space,y as [y1,y2,y3]::ys)= (List.map(fn x as [x1,x2,x3] => post(space,`n1n1 `* FD(y1) `+ `n1 `* FD(y2) `+ FD(y3) `< `n1n1 `* FD(x1) `+ `n1 `* FD(x2) `+ FD(x3),FD.DOM))(ys); redundantconstr(space,ys)) in redundantconstr(space,ivarlist) end;
This code is to be inserted right before the branching. Solving the Steiner problem of order 9 results in the following search tree.
We see that the number of choice nodes decreases from 4529 to 419 and the number of failure nodes decreases from 4505 to 359.
Guido Tack 2007-04-26