1%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 2% Lightweight Dynamic Symmetry Breaking 3% 4% Implemented by Chris Mears, 2009. 5% 6% 7% Copyright 2010 Chris Mears. All rights reserved. 8% 9% Redistribution and use in source and binary forms, with or without modification, are 10% permitted provided that the following conditions are met: 11% 12% 1. Redistributions of source code must retain the above copyright notice, this list of 13% conditions and the following disclaimer. 14% 15% 2. Redistributions in binary form must reproduce the above copyright notice, this list 16% of conditions and the following disclaimer in the documentation and/or other materials 17% provided with the distribution. 18% 19% THIS SOFTWARE IS PROVIDED BY CHRIS MEARS ``AS IS'' AND ANY EXPRESS OR IMPLIED 20% WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND 21% FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL CHRIS MEARS OR 22% CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR 23% CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR 24% SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON 25% ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING 26% NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF 27% ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. 28% 29% The views and conclusions contained in the software and documentation are those of the 30% authors and should not be interpreted as representing official policies, either expressed 31% or implied, of Chris Mears. 32% 33%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 34 35:- module(ldsb). 36 37:- comment(categories, ["Constraints","Techniques"]). 38:- comment(summary, "Lightweight dynamic symmetry breaking for finite domains."). 39:- comment(author, "Chris Mears"). 40 41:- comment(desc, html("</p> 42 43 The LDSB (lightweight dynamic symmetry breaking) library adds 44 symmetry breaking to search. Its aim is to provide easy-to-use 45 symmetry breaking to their finite domain constraint models. The 46 method is described in \"<i>Lightweight Dynamic Symmetry 47 Breaking</i>. C. Mears, M. Garcia de la Banda, B. Demoen, 48 M. Wallace. <i>SymCon'08</i>\". 49 50 <p/> 51 52 To use LDSB, first call ldsb_initialise/2 with the search variables 53 for which you want to use symmetry breaking and a specification of 54 the symmetries. LDSB supports binary search branching of the form 55 <tt>Var = Val</tt> and <tt>Var /= Val</tt>, or <tt>Val in Var</tt> 56 and <tt>Val notin Var</tt> for sets. Use ldsb_indomain/1 and 57 ldsb_indomain_set/1 to instantiate variables during search, or 58 ldsb_try/3 and ldsb_try_set/3 for a custom branching.")). 59 60:- comment(status, "evolving"). 61 62:- lib(ic). 63:- lib(ic_sets). 64 65:- lib(listut). 66:- lib(ordset). 67 68:- lib(test_util). 69 70:- import append/3 from eclipse_language. 71 72%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 73% Export list 74%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 75 76:- export 77 ldsb_initialise/2, 78 ldsb_try/3, 79 ldsb_try_set/3, 80 81 ldsb_indomain/1, 82 ldsb_indomain_set/1, 83 84 run_tests/0. 85 86%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 87% Attributes 88%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 89 90:- meta_attribute(ldsb, [print:print_ldsb/2]). 91 92:- local struct(ldsb_shared(matrix, 93 global_symmetries)). 94 95:- local struct(ldsb_local(idx, 96 local_symmetries, 97 shared)). 98 99print_ldsb(_{ldsb:Attr}, String) :- -?-> 100 Attr = ldsb_local{idx:Idx}, 101 String = ldsb(Idx). 102 103get_index(_{ldsb:(ldsb_local{idx:Idx0})}, Idx) :- -?-> 104 Idx = Idx0. 105 106get_symmetries(_{ldsb:(ldsb_local{local_symmetries:Syms})}, S) :- -?-> 107 S = Syms. 108 109get_shared(_{ldsb:(ldsb_local{shared:Shared})}, S) :- -?-> 110 S = Shared. 111 112%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 113% Symmetry processing. 114%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 115 116% Primitive symmetries. 117process_sym(_, variable_interchange(X), variable_interchange(X)). 118process_sym(_, parallel_variable_interchange(X), parallel_variable_interchange(X)). 119process_sym(_, value_interchange(X), value_interchange(X)). 120process_sym(_, parallel_value_interchange(X), parallel_value_interchange(X)). 121% All variables interchangeable. 122process_sym(Xs, variables_interchange, variable_interchange(L)) :- 123 collection_to_list(Xs, L). 124% All values interchangeable. Determines the minimum and maximum 125% value by looking at the first variable. Works for set variables 126% too. 127process_sym(Xs, values_interchange, value_interchange(L)) :- 128 term_variables(Xs, [X|_]), 129 ( ic_sets : is_solver_type(X) -> 130 potential_members(X, PM), 131 eclipse_language:min(PM, Min), eclipse_language:max(PM, Max) 132 ; get_min(X, Min), get_max(X, Max) ), 133 ( for(I,Min,Max), foreach(I, L) do true ). 134% Rows interchangeable. 135process_sym(Xs, rows_interchange, parallel_variable_interchange(L)) :- 136 seqs_to_lists(Xs, L). 137% Columns interchangeable. 138process_sym(Xs, columns_interchange, parallel_variable_interchange(L)) :- 139 m_transpose(Xs, Transpose), 140 seqs_to_lists(Transpose, L). 141% Reflection around main diagonal. 142process_sym(Xs, diagonal_reflection, parallel_variable_interchange(L)) :- 143 dim(Xs, [N,N]), 144 ( ((for(_I,2,N)) >> 145 (for(J,1,_I-1), param(_I))), 146 foreach(Pair, Pairs) do 147 Pair = [ [_I,J], [J,_I] ] 148 ), 149 length(Pairs, SeqLength), 150 dim(Seqs, [2,SeqLength]), 151 ( foreach([I1,I2], Pairs), 152 param(Xs,Seqs), 153 count(I,1,_) do 154 arg(I1,Xs,V1), 155 arg(I2,Xs,V2), 156 arg([1,I], Seqs, V1), 157 arg([2,I], Seqs, V2) 158 ), 159 seqs_to_lists(Seqs, L). 160% Reflection around horizontal axis. 161process_sym(Xs, row_reflection, parallel_variable_interchange([G1,G2])) :- 162 dim(Xs, [M,N]), 163 div(M, 2, Lim), 164 ( ((for(_I,1,Lim), param(N)) >> 165 (for(J,1,N), param(_I))), 166 foreach(V1, G1), 167 foreach(V2, G2), 168 param(Xs,M) do 169 E1 = [_I,J], 170 I2 is M - _I + 1, 171 E2 = [I2,J], 172 arg(E1, Xs, V1), 173 arg(E2, Xs, V2) 174 ). 175% Reflection around vertical axis. 176process_sym(Xs, column_reflection, S) :- 177 m_transpose(Xs, Transpose), 178 process_sym(Transpose, row_reflection, S). 179% Value reflection. 180process_sym(Xs, value_reflection, S) :- 181 term_variables(Xs, [X|_]), 182 get_min(X, Min), get_max(X, Max), 183 process_sym(Xs, value_reflection(Min,Max), S). 184% Value reflection with explicit bounds. 185process_sym(_Xs, value_reflection(Lower, Upper), parallel_value_interchange(Ls)) :- 186 N is Upper - Lower + 1, 187 N2 is N // 2, 188 dim(Seqs, [2, N2]), 189 ( for(I,1,N2), 190 param(Seqs,Lower,Upper) do 191 Val1 is Lower+(I-1), 192 Val2 is Upper-(I-1), 193 arg([1,I], Seqs, Val1), 194 arg([2,I], Seqs, Val2) 195 ), 196 seqs_to_lists(Seqs, Ls). 197 198%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 199% Variable initialisation. 200%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 201 202:- comment(ldsb_initialise/2, 203 [ amode: (ldsb_initialise(+, +) is det), 204 args: [ "Xs": "Array of search variables", 205 "Syms": "List of symmetries" ], 206 summary: "Initialise LDSB search variables.", 207 resat: no, 208 see_also: [ldsb_try/3, ldsb_indomain/1, ldsb_indomain_set/1], 209 210 desc: html(" <p/> Initialise an array of search variables 211to use LDSB with the given symmetries. A variables must be 212initialised with ldsb_initialise before it can be used with ldsb_try 213or any predicate that relies on it such as ldsb_indomain. 214 215</p> Each element of Syms must be a symmetry specifier from the 216following set: 217 218<ul> 219 220<li> variable_interchange(L). This specifies that the variables in 221the list L are interchangeable. 222 223<li> value_interchange(L). This specifies that the values in the list 224L are interchangeable. 225 226<li> parallel_variable_interchange(Ls). This specifies that the lists 227of variables in the list L are interchangeable. Each list in Ls must 228have the same length. For example, 229parallel_variable_interchange([A,B,C],[D,E,F],[G,H,I]) says that the 230sequence A-B-C can be interchanged with the sequence D-E-F and the 231sequence G-H-I. 232 233<li> parallel_value_interchange(Ls). This specifies that the lists of 234values in the list L are interchangeable. It is the same as 235parallel_variable_interchange, but for values. 236 237<li> variables_interchange. This specifies that all variables in Xs 238are interchangeable. 239 240<li> values_interchange. This specifies that all values in the 241domains of the variables in Xs are interchangeable. Note that for 242this specifier it is assumed that all variables in Xs have the same 243domain. 244 245<li> rows_interchange. This specifies that the rows of variables in 246Xs are interchangeable. Assumes that Xs is a 2D matrix of variables. 247 248<li> columns_interchange. This specifies that the columns of 249variables in Xs are interchangeable. Assumes that Xs is a 2D matrix 250of variables. 251 252<li> diagonal_reflection. This specifies that the variables of Xs can 253be reflected around the main diagonal. Assumes that Xs is a 2D matrix 254of variables. 255 256<li> row_reflection. This specifies that the rows of Xs can be 257reflected around their centre. Assumes that Xs is a 2D matrix of 258variables. 259 260<li> column_reflection. This specifies that the columns of Xs can be 261reflected around their centre. Assumes that Xs is a 2D matrix of 262variables. 263 264<li> value_reflection(L, U). This specifies that the values in the 265sequence L..U can be reflected; i.e. value L+i maps to U-i. 266 267<li> value_reflection. This is the same as value_reflection(L,U), 268where L and U are taken from the minimum and maximum values in the 269domain of the first variable in Xs. 270 271</ul> " ), 272 273 eg: " 274% A vector of interchangeable variables. 275dim(Xs, [N]), 276[...] 277ldsb_initialise(Xs, [variables_interchange]) 278 279% Vector of piecewise interchangeable variables. 280Xs = [](A,B,C,D,E,F), 281[...] 282% A,B,C are interchangeable; D,E,F are interchangeable. 283ldsb_initialise(Xs, [variable_interchange([A,B,C]), 284 variable_interchange([D,E,F])]) 285 286% Variables with interchangeable values. 287dim(Xs, [N]), 288Xs #:: 1..M, 289ldsb_initialise(Xs, [values_interchange]) 290 291% N-queens, with one boolean variable per square. 292dim(A, [N,N]), 293A #:: 0..1, 294[...] 295ldsb_initialise(A, [row_reflection, column_reflection, diagonal_reflection]) 296 297% N-queens with one integer variable per queen. 298% Note that only half of the symmetries are represented. 299dim(Xs, [1,N]), % make Xs a 1xN matrix. 300Xs #:: 1..N, 301[...] 302ldsb_initialise(Xs, [column_reflection, value_reflection]) 303 304% Latin square of order N. 305dim(Xs, [N,N]), 306Xs #:: 1..N, 307[...] 308ldsb_initialise(Xs, [rows_interchange, columns_interchange, values_interchange, diagonal_reflection]) 309 310% Social Golfers problem with one set variable per group. 311dim(Xs, [W,G]), 312[...] 313% Within each week, the groups are interchangeable. 314( for(I, 1, W), foreach(Subsym, Subsyms), param(Xs,G) do 315 subscript(Xs, [I, 1..G], Submatrix), 316 variables_interchange(Submatrix, Subsym) ), 317% rows_interchange: weeks are interchangeable 318% values_interchange: golfers are interchangeable 319ldsb_initialise(Xs, [rows_interchange, values_interchange | Subsyms]) 320"]). 321 322 323ldsb_initialise(Matrix, Symmetries) :- 324 ( foreach(S, Symmetries), foreach(S2, Syms2), param(Matrix) do 325 process_sym(Matrix, S, S2) ), 326 index_syms(Matrix, Syms2). 327 328index_syms(Matrix, Syms) :- 329 % Extract parallel_variable_interchange symmetries from other 330 % symmetries. 331 ( foreach(Sym,Syms), 332 fromto([], PVIIn, PVIOut, PVISyms), 333 fromto([], OtherIn, OtherOut, OtherSyms) do 334 ( Sym = parallel_variable_interchange(_) -> 335 PVIOut = [Sym|PVIIn], OtherOut = OtherIn 336 ; OtherOut = [Sym|OtherIn], PVIOut = PVIIn ) ), 337 338 % Create shared LDSB structure. 339 Shared = ldsb_shared{matrix : Matrix, 340 global_symmetries : OtherSyms}, 341 342 (foreachelem(Var,Matrix,Idx), param(PVISyms,Shared) do 343 index_syms2(Var, PVISyms, LocalSyms), 344 % Create local LDSB structure. 345 Local = ldsb_local{idx : Idx, 346 local_symmetries : LocalSyms, 347 shared : Shared}, 348 add_attribute(Var, Local, ldsb) ). 349 350index_syms2(Var, Syms, Out) :- 351 ( foreach(S, Syms), 352 foreach(O, Out2), 353 param(Var) do 354 ( S = parallel_variable_interchange(VarLists), 355 find_equality(Var, VarLists, Set, Pos) -> 356 O = [sym(S, Set, Pos)] 357 ; 358 O = [] 359 ) 360 ), 361 flatten(Out2, Out). 362 363%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 364% Updating of symmetry state. 365%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 366 367copy_value_symmetries(X, ValueSymmetries) :- 368 get_shared(X, Shared), 369 Shared = ldsb_shared{global_symmetries:Syms}, 370 ( foreach(Sym,Syms), 371 fromto([], VSIn, VSOut, ValueSymmetries) do 372 ( Sym = value_interchange(_) -> 373 VSOut = [Sym|VSIn] 374 ; VSOut = VSIn ) ). 375 376% Alter the symmetry as if X=Val had just happened. 377alter_symmetry(value_interchange(Values), _Var, Val, ReducedSym) :- 378 delete_first(Val, Values, Rest), 379 ReducedSym = value_interchange(Rest), 380 !. 381alter_symmetry(variable_interchange(Vars), Var, _Val, ReducedSym) :- 382 delete_equality(Var, Vars, Rest), 383 ReducedSym = variable_interchange(Rest), 384 !. 385alter_symmetry(parallel_value_interchange(ValueLists), _Var, Val, ReducedSym) :- 386 ( find_equality(Val, ValueLists, WhichSet, _WhichPosition) -> 387 delete_nth1(WhichSet, ValueLists, Rest), 388 ReducedSym = parallel_value_interchange(Rest) 389 ; 390 ReducedSym = parallel_value_interchange(ValueLists) 391 ), 392 !. 393alter_symmetry(S, _, _, S). 394 395%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 396 397member_equality(X,[Y|Ys]) :- 398 ( X == Y -> true 399 ; member_equality(X, Ys) ). 400 401delete_equality(X, [Y|Ys], Rest) :- 402 ( X == Y -> Rest = Ys 403 ; delete_equality(X, Ys, Rest2), 404 Rest = [ Y | Rest2 ] ). 405 406%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 407 408% in in in out out 409apply_symmetry(value_interchange(Values), Var, Val, SymLiterals, ReducedSyms) :- 410 ( memberchk(Val, Values) -> 411 delete_first(Val, Values, Rest), 412 ( foreach(R, Rest), 413 foreach(L, SymLiterals), 414 param(Var) do 415 L = Var - R 416 ), 417 ( Rest = [_] -> ReducedSyms = [] 418 ; ReducedSyms = [value_interchange(Rest)] ) 419 ; 420 % The value isn't in the set of interchangeable values, so nothing happens. 421 SymLiterals = [], 422 ReducedSyms = [value_interchange(Values)] 423 ). 424apply_symmetry(parallel_value_interchange(ValueLists), Var, Val, SymLiterals, ReducedSyms) :- 425 ( find_equality(Val, ValueLists, WhichSet, WhichPosition) -> 426 delete_nth1(WhichSet, ValueLists, Rest), 427 ( foreach(R, Rest), 428 foreach(L, SymLiterals), 429 param(Var, WhichPosition) do 430 nth1(WhichPosition, R, SymValue), 431 L = Var - SymValue 432 ), 433 ( Rest = [_] -> ReducedSyms = [] 434 ; ReducedSyms = [parallel_value_interchange(Rest)] ) 435 ; 436 SymLiterals = [], 437 ReducedSyms = [parallel_value_interchange(ValueLists)] 438 ). 439apply_symmetry(variable_interchange(Vars), Var, Val, SymLiterals, ReducedSyms) :- 440 ( member_equality(Var, Vars) -> 441 delete_equality(Var, Vars, Rest), 442 ( foreach(R, Rest), 443 foreach(L, SymLiterals), 444 param(Val) do 445 L = R - Val 446 ), 447 ( Rest = [_] -> ReducedSyms = [] 448 ; ReducedSyms = [variable_interchange(Rest)] ) 449 ; 450 % The index isn't in the set of interchangeable indices, so nothing happens. 451 SymLiterals = [], 452 ReducedSyms = [variable_interchange(Vars)] 453 ). 454apply_symmetry(parallel_variable_interchange(_VarLists), _Var, _Val, _SymLiterals, _ReducedSyms) :- 455 writeln(error, "error: apply_symmetry called on parallel_variable_interchange term."), 456 abort. 457 458apply_symmetry2(parallel_variable_interchange(VarLists), _Var, Val, WhichSet, WhichPosition, SymLiterals) :- 459 delete_nth1(WhichSet, VarLists, OtherLists), 460 % The list containing the chosen variable. 461 nth1(WhichSet, VarLists, ThisList), 462 463 ( foreach(OtherList, OtherLists), 464 fromto([], PruningsIn, PruningsOut, SymLiterals), 465 param(WhichPosition, ThisList, Val) do 466 check_pruning_ok(ThisList, OtherList, PruningOk), 467 468 ( PruningOk = yes, nth1(WhichPosition, OtherList, PruneVar) -> 469 PruningsOut = [ ( PruneVar - Val ) | PruningsIn ] 470 ; PruningsOut = PruningsIn ) 471 ). 472 473check_pruning_ok([], [], yes). 474check_pruning_ok([T|Ts], [O|Os], PruningOk) :- 475 % See if both corresponding variables are ground and equal, or 476 % both non-ground. 477 OtherVariable = O, 478 ThisVariable = T, 479 ( 480 ground_and_equal(ThisVariable, OtherVariable) -> 481 check_pruning_ok(Ts, Os, PruningOk) 482 ; PruningOk = no 483 ). 484 485% Succeeds if two variables are ground and equal, or both non-ground. 486% Works for sets too, but in the case of set variables, checks that 487% their domains are equal. 488ground_and_equal(X, Y) :- 489 % are they both set variables? 490 ( ic_sets : is_solver_var(X), ic_sets : is_solver_var(Y) -> 491 % if both set variables, are their domains equal? 492 set_range(X, L, U), set_range(Y, L, U), 493 #(X, XC), #(Y, YC), get_domain(XC, D), get_domain(YC, D) 494 % are they both integer variables? 495 ; ( ic : is_solver_var(X), ic : is_solver_var(Y) -> true 496 % are they both ground and equal? 497 ; ( nonvar(X), nonvar(Y), X = Y -> true 498 ; fail ))). 499 500%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 501% Utilities for list processing. 502%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 503 504% Delete the first occurrence of X in a list. 505delete_first(X, [Y|Ys], Rest) :- 506 ( X == Y -> Rest = Ys 507 ; delete_first(X, Ys, Rest2), 508 Rest = [X|Rest2] ). 509 510% Delete the nth element from a list. The first element of the list 511% has index 1. 512delete_nth1(1, [_|Xs], Rest) :- 513 Rest = Xs, !. 514delete_nth1(Index, [X|Xs], Rest) :- 515 Index \= 1, 516 succ(IndexMinus1, Index), 517 delete_nth1(IndexMinus1, Xs, RestTail), 518 Rest = [ X | RestTail ]. 519 520% Retrieve the nth element of a list. The first element of the list 521% has index 1. 522nth1_equality(I, [Y|Ys], X) :- nth1_equality(I, [Y|Ys], X, 1). 523nth1_equality(I, [Y|Ys], X, N) :- 524 ( X == Y -> I = N 525 ; N1 is N + 1, 526 nth1_equality(I, Ys, X, N1) ). 527 528% find_equality(+X, +L, -N, -P) finds the first occurrence of X in L, 529% where L is a list of lists. Fails if X is not found. On success, 530% instantiates N and P such that X is the Pth element of the Nth list 531% in L, where N and P both are indexed from 1. 532find_equality(Element, ListOfLists, WhichList, WhichPosition) :- 533 find_equality(Element, ListOfLists, 1, WhichList, WhichPosition). 534find_equality(Element, [L|Ls], N, WhichList, WhichPosition) :- 535 ( nth1_equality(Position, L, Element) -> 536 WhichList = N, 537 WhichPosition = Position 538 ; 539 N1 is N+1, 540 find_equality(Element, Ls, N1, WhichList, WhichPosition) 541 ). 542 543%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 544% Miscellaneous utilities. 545%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 546 547% Transpose a matrix. 548m_transpose(A, T) :- 549 dim(A, [R,C]), 550 dim(T, [C,R]), 551 ( foreachelem(X,A,[I,J]), 552 param(T) do 553 subscript(T, [J,I], X) 554 ). 555 556% Convert a 2D array into a list of lists. 557seqs_to_lists(Seqs, Lists) :- 558 ( foreacharg(Seq, Seqs), 559 foreach(List, Lists) do 560 Seq =.. [[]|List] ). 561 562 563%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 564% Determine symmetries. 565%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 566 567determine_symmetries(Symmetries, Var, Value, KeptSymmetries) :- 568 ( foreach(S, Symmetries), 569 foreach(R, KeptSymmetries), 570 param(Var, Value) do 571 alter_symmetry(S, Var, Value, R) 572 ). 573 574determine_symmetries_value(ValueInterchanges, Symmetries, Value, KeptSymmetries) :- 575 ( foreach(S, ValueInterchanges), 576 foreach(R, KeptValues2), 577 param(Value) do 578 S = value_interchange(SymVals), 579 eclipse_language:intersection(SymVals, Value, Intersection), 580 eclipse_language:subtract(SymVals, Value, RestSymVals), 581 ( Intersection = [] -> Intersection2 = [] 582 ; Intersection2 = [value_interchange(Intersection)]), 583 ( RestSymVals = [] -> RestSymVals2 = [] 584 ; RestSymVals2 = [value_interchange(RestSymVals)]), 585 R = [Intersection2, RestSymVals2] 586 ), 587 flatten(KeptValues2, KeptValueSyms), 588 589 % Separate the value_interchange symmetries from the rest of the symmetries. 590 ( foreach(S, Symmetries), 591 foreach(VI, ValueInterchange2), 592 foreach(Other, OtherSymmetries2) do 593 ( S = value_interchange(_) -> VI = [S], Other = [] 594 ; VI = [], Other = [S] ) 595 ), 596 flatten(ValueInterchange2, _ValueInterchanges), 597 flatten(OtherSymmetries2, OtherSymmetries), 598 599 append(OtherSymmetries, KeptValueSyms, KeptSymmetries). 600 601%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 602 603% determine_prunings collects all the variable-value pairs that are 604% symmetric to the given Var-Value (including Var-Value itself). It 605% does so by finding all pairs directly symmetric to Var-Value, then 606% the pairs symmetric to those pairs, etc. until no more pairs can be 607% added. 608 609% This case (where Var is ground) is needed for branch-and-bound 610% searches (because the cost imposition may make the search variable 611% ground). 612determine_prunings(_Symmetries, Var, _Value, Prunings) :- 613 nonvar(Var), Prunings = []. 614determine_prunings(Symmetries, Var, Value, Prunings) :- 615 var(Var), 616 ( fromto([Var - Value], [(X - V)|PRest], POut, []), 617 fromto([Var - Value], FinalPruningsIn, FinalPruningsOut, Prunings2), 618 param(Symmetries) do 619 determine_prunings2(Symmetries, X, V, PsList), 620 list_to_ord_set(PsList, Ps), 621 ord_union(FinalPruningsIn, Ps, FinalPruningsOut, New), 622 ord_union(PRest, New, POut) 623 ), 624 ord_subtract(Prunings2, [Var - Value], Prunings). 625 626% determine_prunings2 finds the variable-value pairs *directly* 627% symmetric to Var-Value. (Here "directly" means not via 628% composition). 629% in in in out 630determine_prunings2(Symmetries, Var, Value, Prunings) :- 631 ( foreach(S, Symmetries), 632 foreach(P, PruningsList), 633 param(Value, Var) do 634 635 % Make sure Var is an LDSB variable. 636 ( get_index(Var, _Idx) -> true ; writeln(error, 'VERY BAD; should not happen'), abort ), 637 638 ( S = parallel_variable_interchange(_) -> P = [] 639 ; apply_symmetry(S, Var, Value, P, _NewSyms) ) 640 ), 641 get_symmetries(Var, Syms), 642 (foreach(sym(S,Set,Pos), Syms), 643 foreach(P, PruningsList2), 644 param(Var, Value) do 645 apply_symmetry2(S, Var, Value, Set, Pos, P) 646 ), 647 flatten(PruningsList, Prunings1), 648 flatten(PruningsList2, Prunings2), 649 append(Prunings1, Prunings2, PruningsL), 650 Prunings = PruningsL. 651 652prune(Prunings) :- 653 ( foreach(P, Prunings) do 654 Var - Val = P, 655 Var #\= Val 656 ). 657 658prune_set(Prunings) :- 659 ( foreach(P, Prunings) do 660 Var - Val = P, 661 Val notin Var 662 ). 663 664%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 665 666:- comment(ldsb_try/3, 667 [ amode: (ldsb_try(+, ++, ?)), 668 args: [ "X": "Variable to try", 669 "Value": "Value to try", 670 "Success": "Whether the assignment succeeded or not"], 671 resat: yes, 672 see_also: [ldsb_indomain/1, ldsb_initialise/2, ldsb_try_set/3], 673 674 summary: "Try assigning a value to an LDSB variable.", 675 676 desc: html("<p/> Tries to assign Value to X. Upon 677 backtracking, excludes Value from the domain of X. The 678 value of Success tells whether the assignment succeeded; 679 Success is 1 if X #= Value and 0 if X #\\= Value."), 680 681 eg: " 682ldsb_indomain(X) :- nonvar(X), !. 683ldsb_indomain(X) :- 684 ic:is_solver_var(X), !, 685 get_min(X,V), 686 ldsb_try(X, V, _), 687 ldsb_indomain(X)."]). 688 689% LDSB equivalent of ic_gap_sbds:sbds_try/3. 690ldsb_try(Var{ldsb:(ldsb_local{shared:Shared})}, Value, Success) :- -?-> 691 Shared = ldsb_shared{global_symmetries:GlobalSymmetries}, 692 ( 693 % Positive branch. 694 695 % Update global symmetries. 696 determine_symmetries(GlobalSymmetries, Var, Value, KeptSymmetries), 697 setarg(global_symmetries of ldsb_shared, Shared, KeptSymmetries), 698 699 % Make assignment. 700 Var = Value, 701 Success = 1 702 ; 703 % Negative branch. 704 determine_prunings(GlobalSymmetries, Var, Value, Prunings), 705 Var #\= Value, 706 prune(Prunings), 707 Success = 0 708 ). 709 710:- comment(ldsb_try_set/3, 711 [ amode: (ldsb_try_set(+, ++, ?)), 712 args: [ "X": "Variable to try", 713 "Value": "Value to try", 714 "Success": "Whether the inclusion succeeded or not"], 715 resat: yes, 716 see_also: [ldsb_indomain_set/1, ldsb_initialise/2, ldsb_try/3], 717 718 summary: "Try including a value in an LDSB set variable.", 719 720 desc: html("<p/> Tries to include Value in X. Upon 721 backtracking, excludes Value from X. The value of 722 Success tells whether the inclusion succeeded; Success is 723 1 if (Value in X) and 0 if Value has been excluded. 724 725 <p/> Note that due to the interaction between set 726 variable searching and value symmetries, using this 727 predicate in discouraged. Use ldsb_indomain_set/1 728 instead.")]). 729 730ldsb_try_set(Var{ldsb:(ldsb_local{shared:Shared})}, Value, Success) :- -?-> 731 Shared = ldsb_shared{global_symmetries:GlobalSymmetries}, 732 ( 733 % Positive branch. 734 735 % Update global symmetries. 736 determine_symmetries(GlobalSymmetries, Var, Value, KeptSymmetries), 737 setarg(global_symmetries of ldsb_shared, Shared, KeptSymmetries), 738 739 % Make assignment. 740 Value in Var, 741 Success = 1 742 ; 743 % Negative branch. 744 determine_prunings(GlobalSymmetries, Var, Value, Prunings), 745 Value notin Var, 746 prune_set(Prunings), 747 Success = 0 748 ). 749 750%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 751% Predicates to instantiate variables. 752%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 753 754:- comment(ldsb_indomain/1, 755 [ amode: (ldsb_indomain(?)), 756 args: [ "X": "Variable or integer" ], 757 resat: yes, 758 see_also: [ldsb_indomain_set/1, ldsb_initialise/2], 759 760 summary: "Instantiates an LDSB integer variable to an 761 element of its domain.", 762 763 desc: html("<p/> Simple predicate for instantiating an 764 integer LDSB variable to an element of its domain. It 765 starts with the smallest element, and upon backtracking 766 tries successive elements until the entire domain has 767 been explored, at which point the predicate fails. 768 769 <p/>If X is already a ground integer, then this predicate 770 simply succeeds exactly once without leaving a 771 choicepoint. 772 773 <p/>This predicate can be used with the search/6 774 predicate (see example)."), 775 776 eg:" 777go :- 778 dim(Xs, [3]), 779 Xs #:: 1..5, 780 collection_to_list(Xs, L), sum(L) #= 10, 781 ldsb_initialise(Xs, [variables_interchange]), 782 ( search(Xs, 0, input_order, ldsb_indomain, complete, []), 783 writeln(Xs), 784 fail 785 ; true ). 786" ]). 787 788% Tries values for X in ascending order. 789ldsb_indomain(X) :- nonvar(X), !. 790ldsb_indomain(X) :- 791 ic:is_solver_var(X), !, 792 get_min(X,V), 793 ldsb_try(X, V, _), 794 ldsb_indomain(X). 795 796:- comment(ldsb_indomain_set/1, 797 [ amode: (ldsb_indomain_set(?)), 798 args: [ "X": "Set variable or set" ], 799 resat: yes, 800 see_also: [ldsb_indomain/1, ldsb_initialise/2], 801 802 summary: "Instantiates an LDSB set variable to an element 803 of its domain.", 804 805 desc: html("<p/> Simple predicate for instantiating a set 806 LDSB variable to an element of its domain. If a set 807 value is considered a binary number, where 1 is inclusion 808 and 0 is exclusion, the value ordering is descending. 809 For example: 810 811 <pre> 812go :- 813 intset(S, 1, 3), 814 Xs = [](S), 815 ldsb_initialise(Xs, []), 816 ( ldsb_indomain_set(S), writeln(S), fail 817 ; true). 818 </pre> 819 820 would produce the following output: 821 822 <pre> 823[1, 2, 3] 824[1, 2] 825[1, 3] 826[1] 827[2, 3] 828[2] 829[3] 830[] 831 </pre> 832 833 <p/>If X is already a ground set, then this predicate 834 simply succeeds exactly once without leaving a 835 choicepoint. 836 837 <p/>This predicate can be used with the search/6 838 predicate (see example)."), 839 840 eg:" 841go :- 842 intsets(L, 3, 1, 10), 843 ( foreach(S, L) do #(S, 3) ), 844 ( fromto(L, [X|Xs], Xs, []) do 845 ( foreach(Y, Xs), param(X) do 846 #(X /\\ Y, 0) ) ), 847 Xs =.. [[]|L], 848 ldsb_initialise(Xs, [values_interchange]), 849 ( search(Xs, 0, input_order, ldsb_indomain_set, complete, []), 850 writeln(Xs), 851 fail 852 ; true ). 853" ]). 854 855% Tries values for a set variable in ascending order, inclusion before 856% exclusion. 857ldsb_indomain_set(X) :- nonvar(X), !. 858ldsb_indomain_set(X) :- var(X), !, 859 % Remember state of value symmetries. 860 copy_value_symmetries(X, ValueSymmetries), 861 get_shared(X, Shared), 862 % Assign a value. 863 ldsb_indomain_set2(X), 864 % Replace the current value symmetries with the result of the 865 % old ones applied to the given value. 866 Shared = ldsb_shared{global_symmetries : Symmetries}, 867 determine_symmetries_value(ValueSymmetries, Symmetries, X, KeptSymmetries), 868 setarg(global_symmetries of ldsb_shared, Shared, KeptSymmetries). 869ldsb_indomain_set2(X) :- nonvar(X), !. 870ldsb_indomain_set2(X) :- var(X), !, 871 potential_members(X, [V|_]), 872 ldsb_try_set(X, V, _), 873 ldsb_indomain_set2(X). 874 875%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 876% Testing. 877%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 878 879example_case1 :- 880 dim(Xs, [3]), 881 Xs #:: 1..5, 882 collection_to_list(Xs, L), sum(L) #= 10, 883 ldsb_initialise(Xs, [variables_interchange]), 884 ( search(Xs, 0, input_order, ldsb_indomain, complete, []), 885 writeln(Xs), 886 fail 887 ; true ). 888 889example_case2 :- 890 intsets(L, 3, 1, 10), 891 ( foreach(S, L) do #(S, 3) ), 892 ( fromto(L, [X|Xs], Xs, []) do 893 ( foreach(Y, Xs), param(X) do 894 #(X /\ Y, 0) ) ), 895 Xs =.. [[]|L], 896 ldsb_initialise(Xs, [values_interchange]), 897 ( search(Xs, 0, input_order, ldsb_indomain_set, complete, []), 898 writeln(Xs), 899 fail 900 ; true ). 901 902example_case3 :- 903 intset(S, 1, 3), 904 Xs = [](S), 905 ldsb_initialise(Xs, []), 906 ( ldsb_indomain_set(S), writeln(S), fail 907 ; true). 908 909example_case4 :- 910 intset(S, 1, 3), 911 Xs = [](S), 912 ldsb_initialise(Xs, [values_interchange]), 913 ( ldsb_indomain_set(S), writeln(S), fail 914 ; true). 915 916:- comment(run_tests/0, hidden). 917 918% Initialising variables should set attributes. 919test_case(init1) :- dim(Xs, [4]), Xs #:: 1..10, ldsb_initialise(Xs, []), Xs = [](X,_,_,_), get_index(X, _) should_give true. 920test_case(init2) :- dim(Xs, [4]), Xs #:: 1..10, Xs = [](X,_,_,_), get_index(X, _) should_fail. 921test_case(init3) :- dim(Xs, [4]), Xs #:: 1..10, ldsb_initialise(Xs, []), Xs = [](X,_,_,_), get_symmetries(X, _) should_give true. 922test_case(init4) :- dim(Xs, [4]), Xs #:: 1..10, Xs = [](X,_,_,_), get_symmetries(X, _) should_fail. 923test_case(init5) :- dim(Xs, [4]), Xs #:: 1..10, ldsb_initialise(Xs, []), Xs = [](X,_,_,_), get_shared(X, _) should_give true. 924test_case(init6) :- dim(Xs, [4]), Xs #:: 1..10, Xs = [](X,_,_,_), get_shared(X, _) should_fail. 925 926% Test composition of symmetry. 927test_case(compos1) :- 928 Xs = [](A,_,_,_), 929 Xs #:: 1..6, 930 ic_global:alldifferent(Xs), 931 ldsb_initialise(Xs, [variables_interchange, value_interchange([1,2,3])]), 932 ldsb_try(A, 1, 0) should_fail. 933 934% Test variable and value interchange. 935test_case(var1) :- Xs = [](A,_,_,_), Xs #:: 1..10, ldsb_initialise(Xs, [variables_interchange]), ldsb_try(A, 1, 0) should_give true. 936test_case(value1) :- Xs = [](A,_,_,_), Xs #:: 1..10, ldsb_initialise(Xs, [values_interchange]), ldsb_try(A, 1, 0) should_fail. 937 938% Test process_sym. 939test_case(process_sym1) :- Xs = [](A,B,C,D), Xs #:: 1..10, process_sym(Xs, variables_interchange, variable_interchange([A,B,C,D])) should_give true. 940test_case(process_sym2) :- Xs = [](_,_,_,_), Xs #:: 1..3, process_sym(Xs, values_interchange, value_interchange([1,2,3])) should_give true. 941test_case(process_sym3) :- Xs = []([](A,B,C), 942 [](D,E,F), 943 [](G,H,I)), Xs #:: 1..3, process_sym(Xs, rows_interchange, parallel_variable_interchange([[A1,B1,C1], 944 [D1,E1,F1], 945 [G1,H1,I1]])), 946 [A,B,C,D,E,F,G,H,I] == [A1,B1,C1,D1,E1,F1,G1,H1,I1] should_give true. 947test_case(process_sym4) :- Xs = []([](A,B,C), 948 [](D,E,F), 949 [](G,H,I)), Xs #:: 1..3, process_sym(Xs, columns_interchange, parallel_variable_interchange([[A1,D1,G1], 950 [B1,E1,H1], 951 [C1,F1,I1]])), 952 [A,B,C,D,E,F,G,H,I] == [A1,B1,C1,D1,E1,F1,G1,H1,I1] should_give true. 953test_case(process_sym5) :- Xs = []([](_,B,C), 954 [](D,_,F), 955 [](G,H,_)), Xs #:: 1..3, process_sym(Xs, diagonal_reflection, parallel_variable_interchange([[D1,G1,H1],[B1,C1,F1]])), 956 [B,C,D,F,G,H] == [B1,C1,D1,F1,G1,H1] should_give true. 957test_case(process_sym6) :- Xs = []([](A,B,C), 958 [](_,_,_), 959 [](G,H,I)), Xs #:: 1..3, process_sym(Xs, row_reflection, parallel_variable_interchange([[A1,B1,C1],[G1,H1,I1]])), 960 [A,B,C,G,H,I] == [A1,B1,C1,G1,H1,I1] should_give true. 961test_case(process_sym7) :- Xs = []([](A,_,C), 962 [](D,_,F), 963 [](G,_,I)), Xs #:: 1..3, process_sym(Xs, column_reflection, parallel_variable_interchange([[A1,D1,G1],[C1,F1,I1]])), 964 [A,C,D,F,G,I] == [A1,C1,D1,F1,G1,I1] should_give true. 965test_case(process_sym8) :- Xs = [](_,_,_,_), Xs #:: 1..5, process_sym(Xs, value_reflection, parallel_value_interchange([[1,2],[5,4]])) should_give true. 966test_case(process_sym9) :- Xs = [](_,_,_,_), Xs #:: 1..6, process_sym(Xs, value_reflection, parallel_value_interchange([[1,2,3],[6,5,4]])) should_give true. 967 968run_tests :- 969 findall(X, (test_case(X), writeln(X)), _). 970