1/*
    2  examplesFLOPS2024.pl
    3  
    4  @author Francois Fages
    5  @email Francois.Fages@inria.fr
    6  @institute Inria, France
    7  @license LGPL-2
    8
    9  @version 1.1.0
   10
   11  
   12
   13*/
   14
   15:- module(examplesFLOPS2024,
   16	  [
   17	   queens/2,
   18	   queens_distinct/2,
   19	   queens_sym/2,
   20	   sym_elim/2,
   21	   queens_sym_distinct/2,
   22
   23	   queens_list/2,
   24	   queens_distinct_list/2,
   25	   queens_sym_list/2,
   26	   sym_elim_list/2,
   27	   queens_sym_distinct_list/2,
   28
   29	   show/1,
   30
   31	   fourier/4,
   32
   33	   benchmark/0
   34	   ]).

examplesFLOPS2024

author
- Francois Fages
version
- 1.1.0

Examples of use of SWI-Prolog pack modeling described in

F. Fages. A Constraint-based Mathematical Modeling Library in Prolog with Answer Constraint Semantics. 17th International Symposium on Functional and Logic Programming, FLOPS 2024. May 15, 2024 - May 17, 2024, Kumamoto, Japan. LNCS, Springer-Verlag.

?- queens(8,Queens), show(Queens).
Q . . . . . . .
. . . . . . Q .
. . . . Q . . .
. . . . . . . Q
. Q . . . . . .
. . . Q . . . .
. . . . . Q . .
. . Q . . . . .

Queens = array(1, 5, 8, 6, 3, 7, 2, 4) .

?- fourier(3, X, Y, 1).
X = Y, Y = 6.666666666666667.

?- fourier(3.1, X, Y, 1).
false.

?- fourier(2, X, Y, 1).
{Y=20.0-10.0*_A-10.0*_B, X=10.0*_B, _=2.0-_A-_B, _A+_B>=1.0, _B=<1.0, _A=<1.0}.

?- fourier(0, X, Y, 1).
true.
  
?- fourier(2, X, Y, 1), minimize(X).
X = 0.0,
Y = 10.0.

?- fourier(2, X, Y, 1), maximize(X).
X = 10.0,
{Y=10.0-10.0*_A, _=1.0-_A, _A=<1.0, _A>=0.0}.

?- fourier(2, X, Y, 1), maximize(Y).
Y = 10.0,
{X=10.0*_A, _A>=0.0, _A=<1.0, _=1.0-_A}.

?- fourier(2, X, Y, 1), minimize(Y).
X = 10.0,
Y = 0.0.

*/

   92:- reexport(library(modeling)).   93
   94				% N-QUEENS PLACEMENT MODELS USING SUBSCRIPTED VARIABLES
   95
   96
   97%! queens(+N, ?Queens)
   98%
   99% solves the N Queens problems using arrays.
  100
  101queens(N, Queens):-
  102  int_array(Queens, [N], 1..N),
  103  for_all([I in 1..N-1, D in 1..N-I],
  104          (Queens[I] #\= Queens[I+D],
  105           Queens[I] #\= Queens[I+D]+D,
  106           Queens[I] #\= Queens[I+D]-D)),
  107  satisfy(Queens).
  108
  109
  110
  111%! queens_distinct(+N, ?Queens)
  112%
  113% solves the N Queens problems using arrays and the global constraint all_distinct/1 of library(clpfd)
  114
  115queens_distinct(N, Queens):-
  116    int_array(Queens, [N], 1..N),
  117    
  118    int_array(Indices, [N]),
  119    for_all(I in 1..N, cell(Indices, I, I)),
  120    
  121    op_rel(Queens, +, Indices, #=, QueensPlusI), 
  122    op_rel(Queens, -, Indices, #=, QueensMinusI),
  123
  124    all_distinct(QueensPlusI),
  125    all_distinct(Queens),
  126    all_distinct(QueensMinusI),
  127
  128    satisfy(Queens).
  129
  130
  131%! queens_sym(+N, ?Queens)
  132%
  133% solves the N Queens problems with symmetry breaking using arrays.
  134
  135queens_sym(N, Queens):-
  136  int_array(Queens, [N], 1..N),
  137  for_all([I in 1..N-1, D in 1..N-I],
  138          (Queens[I] #\= Queens[I+D],
  139           Queens[I] #\= Queens[I+D]+D,
  140           Queens[I] #\= Queens[I+D]-D)),
  141  sym_elim(N, Queens),
  142  satisfy(Queens).
  143
  144
  145sym_elim(N, Queens) :-
  146  
  147  Queens[1] #< Queens[N], % vertical reflection
  148  Queens[1] #=< (N+1)//2, % horizontal reflection
  149  
  150  int_array(Dual, [N], 1..N), 
  151  for_all([I, J] in 1..N, Queens[I] #= J #<==> Dual[J] #= I),
  152  lex_leq(Queens, Dual),  % first diagonal reflection
  153  
  154  int_array(SecondDiagonal, [N], 1..N),
  155  for_all(I in 1..N, SecondDiagonal[I] #= N + 1 - Dual[N+1-I]),
  156  lex_leq(Queens, SecondDiagonal), 
  157
  158  int_array(R90, [N], 1..N),
  159  for_all(I in 1..N, R90[I] #= Dual[N+1-I]),
  160  lex_leq(Queens, R90),   % rotation 90°
  161
  162  int_array(R180, [N], 1..N),
  163  for_all(I in 1..N, R180[I] #= N + 1 - Queens[N+1-I]),
  164  lex_leq(Queens, R180),
  165  
  166  int_array(R270, [N], 1..N),
  167  for_all(I in 1..N, R270[I] #= N + 1 - Dual[I]),
  168  lex_leq(Queens, R270).
  169
  170
  171
  172%! queens_sym_distinct(+N, ?Queens)
  173%
  174%  solves the N Queens problems with symmetry breaking using arrays and global constraint all_distinct/1.
  175
  176queens_sym_distinct(N, Queens):-
  177    int_array(Queens, [N], 1..N),
  178    int_array(Indices, [N]),
  179    for_all(I in 1..N, cell(Indices, I, I)),
  180    op_rel(Queens, +, Indices, #=, QueensPlusI), 
  181    op_rel(Queens, -, Indices, #=, QueensMinusI),
  182    all_distinct(QueensPlusI),
  183    all_distinct(Queens),
  184    all_distinct(QueensMinusI),
  185    
  186    sym_elim(N, Queens),
  187    
  188    satisfy(Queens).
  189
  190
  191				% N-QUEENS PLACEMENT PROGRAMS USING LISTS
  192
  193
  194%! queens_list(+N, ?Queens)
  195%
  196% standard program using lists for the N Queens problem.
  197
  198queens_list(N, Queens):-
  199  length(Queens, N),
  200  Queens ins 1..N,
  201  safe(Queens),
  202  labeling([ff], Queens).
  203
  204safe([]).
  205safe([QI | Tail]) :-
  206  noattack(Tail, QI, 1),
  207  safe(Tail).
  208
  209noattack([], _, _).
  210noattack([QJ | Tail], QI, D) :-
  211  QI #\= QJ,
  212  QI #\= QJ + D,
  213  QI #\= QJ - D,
  214  D1 #= D + 1,
  215  noattack(Tail, QI, D1).
  216
  217
  218%! queens_distinct_list(+N, ?Queens)
  219%
  220% program using lists and the global constraint all_distinct/1 of library(clpfd)
  221
  222queens_distinct_list(N, Queens):-
  223    length(Queens, N),
  224    Queens ins 1..N,
  225
  226    length(Indices, N),
  227    for_all(I in 1..N, nth1(I, Indices, I)),
  228    
  229    op_rel(Queens, +, Indices, #=, QueensPlusI), 
  230    op_rel(Queens, -, Indices, #=, QueensMinusI),
  231
  232    all_distinct(QueensPlusI),
  233    all_distinct(Queens),
  234    all_distinct(QueensMinusI),
  235
  236    labeling([ff], Queens).
  237
  238
  239%! queens_sym_list(+N, ?Queens)
  240%
  241% list program to break symmetries in the N Queens problem.
  242
  243queens_sym_list(N, Queens) :- 
  244  length(Queens, N),
  245  Queens ins 1..N,
  246  safe(Queens),
  247
  248  sym_elim_list(N, Queens),
  249
  250  labeling([ff], Queens).
  251
  252
  253sym_elim_list(N, Queens) :-
  254  last(Queens, Last),
  255  Queens = [First | _],
  256  First #< Last,
  257  First #=< (N+1) // 2,
  258
  259  dual(N, Queens, Dual),
  260  lex_leq(Queens, Dual),
  261
  262  length(CounterDiagonal, N),
  263  reverse(Dual, DualReversed),	% in order N+1-I
  264  counterdiag(CounterDiagonal, 1, N, DualReversed),
  265  lex_leq(Queens, CounterDiagonal),
  266
  267  length(R90, N),
  268  r90(R90, 1, N, DualReversed),
  269  lex_leq(Queens, R90),
  270  
  271  length(R180, N),
  272  reverse(Queens, QueensReversed), % in order N+1-I
  273  r180(R180, 1, N, QueensReversed),
  274  lex_leq(Queens, R180),
  275  
  276  length(R270, N),
  277  r180(R270, 1, N, Dual), % not a typo ! since applied here to the dual instead of the reversed primal
  278  lex_leq(Queens, R270).
  279
  280
  281dual(N, Queens, Dual):-
  282    length(Dual, N),
  283    forall_IJ(Queens, 1, Dual).
  284
  285forall_IJ([],  _, _).
  286forall_IJ([QI |Qs], I, Dual):-
  287    forall_J(Dual, 1, QI, I),
  288    I1 #= I+1,
  289    forall_IJ(Qs, I1, Dual).
  290
  291forall_J([], _, _,  _).
  292forall_J([RJ | R], J, QI, I):-
  293    (QI#=J) #<==> (RJ#=I),
  294    J1 #= J+1,
  295    forall_J(R, J1, QI, I).
  296
  297counterdiag([], _, _, _).
  298counterdiag([CI | CounterDiagonal], I, N, [DI | Dual]):-
  299    CI #= N+1-DI,
  300    I1 is I+1,
  301    counterdiag(CounterDiagonal, I1, N, Dual).
  302
  303r90([], _, _, _).
  304r90([RI | R90], I, N, [DI | Dual]):-
  305    RI #= DI,
  306    I1 is I+1,
  307    r90(R90, I1, N, Dual).
  308
  309r180([], _, _, _).
  310r180([RI | R90], I, N, [DI | Dual]):-
  311    RI #= N+1-DI,
  312    I1 is I+1,
  313    r180(R90, I1, N, Dual).
  314
  315
  316%! queens_sym_distinct_list(+N, ?Queens)
  317%
  318% list program with symmetry breaking and global constraint all_distinct/1
  319
  320queens_sym_distinct_list(N, Queens) :- 
  321    length(Queens, N),
  322    Queens ins 1..N,
  323    
  324    length(Indices, N),
  325    for_all(I in 1..N, nth1(I, Indices, I)),
  326    
  327    op_rel(Queens, +, Indices, #=, QueensPlusI), 
  328    op_rel(Queens, -, Indices, #=, QueensMinusI),
  329    
  330    all_distinct(QueensPlusI),
  331    all_distinct(Queens),
  332    all_distinct(QueensMinusI),
  333
  334    sym_elim_list(N, Queens),
  335    
  336    labeling([ff], Queens).
  337
  338
  339				% PRETTY-PRINT OF THE CHESSBOARD PLACEMENT
 show(+Queens)
pretty prints chessboard Queens (either array or list).
  346show(Queens):-
  347    (array(Queens)
  348    ->
  349     show_array(Queens)
  350    ;
  351     show_list(Queens)).
  352
  353show_array(Queens):-
  354    array(Queens, [N]),
  355    for_all([I, J] in 1..N,
  356    	    let([QJ = Queens[J],
  357    		 Q = if(QJ = I, 'Q', '.'),
  358    		 B = if(J = N, '\n', ' ')],
  359		format("~w~w",[Q,B]))),
  360    nl.
  361
  362show_list(Queens):-
  363    length(Queens, N),
  364    for_all([I, J] in 1..N,
  365	    exists(QJ,
  366		   (nth1(J, Queens, QJ),
  367		    let([Q = if(QJ = I, 'Q', '.'),
  368			 B = if(J = N, '\n', ' ')],
  369			format("~w~w",[Q,B]))))),
  370    nl.
  371
  372
  373				% BENCHMARKING
  374/*
  375  ?- benchmark.
  376user:queens(100,_69028)
  377% 4,552,518 inferences, 0.373 CPU in 0.387 seconds (96% CPU, 12212181 Lips)
  378user:queens_list(100,_2790392)
  379% 4,472,406 inferences, 0.298 CPU in 0.310 seconds (96% CPU, 15025469 Lips)
  380user:queens_distinct(100,_8210576)
  381% 63,565,626 inferences, 3.611 CPU in 3.641 seconds (99% CPU, 17603740 Lips)
  382user:queens_distinct_list(100,_1467832)
  383% 63,502,308 inferences, 3.470 CPU in 3.484 seconds (100% CPU, 18298489 Lips)
  384user:(queens(8,_1913650),fail)
  385% 757,835 inferences, 0.041 CPU in 0.041 seconds (99% CPU, 18435668 Lips)
  386user:(queens_list(8,_1914304),fail)
  387% 757,303 inferences, 0.042 CPU in 0.043 seconds (99% CPU, 17926877 Lips)
  388user:(queens_distinct(8,_1914958),fail)
  389% 4,025,643 inferences, 0.297 CPU in 0.303 seconds (98% CPU, 13541040 Lips)
  390user:(queens_distinct_list(8,_79224),fail)
  391% 4,012,622 inferences, 0.289 CPU in 0.295 seconds (98% CPU, 13908424 Lips)
  392user:(queens_sym(8,_33346),fail)
  393% 667,850 inferences, 0.045 CPU in 0.046 seconds (98% CPU, 14860595 Lips)
  394user:(queens_sym_list(8,_34000),fail)
  395% 664,708 inferences, 0.048 CPU in 0.049 seconds (97% CPU, 13812975 Lips)
  396user:(queens_sym_distinct(8,_34654),fail)
  397% 1,471,542 inferences, 0.125 CPU in 0.132 seconds (95% CPU, 11760763 Lips)
  398user:(queens_sym_distinct_list(8,_34510),fail)
  399% 1,509,989 inferences, 0.128 CPU in 0.132 seconds (97% CPU, 11818117 Lips)
  400true.
  401*/
 benchmark
computation time benchmark of problems used in FLOPS paper for comparing bounded quantifiers on subscripted variables, to recursion on lists.
  406benchmark :-
  407    % first solution
  408    test(queens(100, _)),
  409    test(queens_list(100, _)),
  410    test(queens_distinct(100, _)),
  411    test(queens_distinct_list(100, _)),
  412    % all solutions
  413    test((queens(8, _), fail)),
  414    test((queens_list(8, _), fail)),
  415    test((queens_distinct(8, _), fail)),
  416    test((queens_distinct_list(8, _), fail)),
  417    % non symmetrical solutions
  418    test((queens_sym(8, _), fail)),
  419    test((queens_sym_list(8, _), fail)),
  420    test((queens_sym_distinct(8, _), fail)),
  421    test((queens_sym_distinct_list(8, _), fail)),
  422    % clpr interface
  423    test(fourier(2, _, _, 1)).
  424
  425
  426test(Goal):-
  427    writeln(Goal),
  428    (time(Goal) -> true ; true).
  429
  430
  431
  432
  433				% FOURIER'S EXAMPLE OVER THE REAL NUMBERS
  434
  435
  436%! fourier(?P, ?X, ?Y, ?F)
  437%
  438% Placing a weight P at coordinates X Y on an isocel triangle table with 3 legs at coordinates (0,0), (20, 0) and (0, 20)
  439% and with a maximum force F exerted on each leg.
  440
  441fourier(P, X, Y, F):-
  442    float_array(Force, [3], 0