Picat programs for most puzzles in Adrian Groza's book Modelling Puzzles in First Order Logic

[Hakan Kjellerstrand]

During the last weeks I've written #Picat models for most of the 144 puzzles in Adrian Groza's great book "Modelling Puzzles in First Order Logic" (https://users.utcluj.ro/~agroza/puzzles/maloga/ ). His solutions are in the FOL systems Mace4/Prover9.

Here are the Picat programs: http://hakank.org/picat/#groza_puzzles . Most are - perhaps unsurprisingly - constraint models.

I have not tried to port Groza's Mace4 models directly (expect in a very few cases), but tried to solve the puzzles in a "natural" way. Sometimes this is nicer, IMHO, than Groza's Mace4 models, but sometimes the use of a FOL system is really neat.

Some of these are work in progress, especially the one in "Chapter 12 Polyomino Puzzles" which are a little too slow right now. 

Best,

Hakan

[Neng-Fa Zhou]

Thanks, Hakan, for the great work.  Do you have any "open" challenging problems that you would like people in this community to help?

Best,

NF

[Hakan Kjellerstrand]

Thanks, Neng-Fa.

The puzzles that I struggled with most was the Polyomino Puzzles in chapter 12 (http://hakank.org/picat/polyominos.pi  together with http://hakank.org/picat/rectangle_symmetries.pi). My current approach is a hybrid with constraint modelling and non-deterministic approach, using member/2 for generating the rotations/flips for a given shape to fit into the grid. This works OK for the first few problems (122-126, and 131), but are too slow for the larger pentominoes problems. Puzzle 127  "The 12 pentonomoes" which is included in polyominos.pi but is way too slow, takes at least a couple of hours (but I haven't waited for it to finish). The two puzzles that use only 6 pentominoes ("Puzzle 128. Importing six pentominoes" and  "Puzzle 129. Importing other six pentominoes") takes a few minutes to solve, but that's too slow in my opinion. (The calculation of the symmetries for a shape are in http://hakank.org/picat/rectangle_symmetries.pi ).

In short, I haven't yet figured out how to make a pure constraint model that also includes placing the variant with rotations/flips etc. I would guess that it should be faster than my hybrid approach.

Years ago, I ported a MiniZinc model by Mikael Zayenz Lagerkvist which used regular/5 for these kind of problems (http://hakank.org/picat/pentonomies.pi and http://hakank.org/picat/pentonomies_data.pi ), but it requires generating DFA for the instances. But generating the DFAs for the instances in Groza's book is currently beyond me. But that seems to be a good approach.  This approach was described by Mikael and Gilles Pesant in the paper "Modeling Irregular Shape Placement Problems with Regular Constraints"  (https://zayenz.se/papers/LagerkvistPesant_BPPC_2008.pdf ).

It would be really great to have the general Geost constraint available in Picat for these kind of problems (https://sofdem.github.io/gccat/gccat/Cgeost.html).

MiniZinc supports it: https://www.minizinc.org/doc-2.7.6/en/lib-globals-packing.html#mzn-globals-packing-geost , though it hasn't been in any of the MiniZinc challenges (yet).

Another puzzle I had - and still have - problem to encode is "Puzzle 78. What is my relationship to Teresa?":

"""

Teresa’s daughter is my daughter’s mother. What is my relationship to Teresa? Are you:
1. Teresa’s grandmother.
2. her mother.
3. her daughter.
4. her granddaughter.
5. Teresa.

"""

The Mace4 encoding is at https://users.utcluj.ro/~agroza/puzzles/maloga/all_code/ch_07_love_mariage/teresa.in

but I haven't been able to translate it to Picat (using logic programming, or constraint programming).

Perhaps you or someone else can help out with any of this?

Note that many of the puzzle formulations (and the solutions) from the book are available in Groza's large paper "Measuring reasoning capabilities of ChatGPT" (https://arxiv.org/pdf/2310.05993.pdf): he ask ChatGPT (v 3.5) to solve about 100 of these puzzles, and - as expected - ChatGPT struggles with quite a few of them. Though I would expect that GPT 4 would be a little better on at least some of the puzzles.

Another thing: I have now encoded two chapter of puzzles to plain logic programming (instead of constraint modelling). It's the Smullyan type puzzles in

- Chapter 5 Lady and Tigers: http://hakank.org/picat/lady_and_tiger_lp.pi

- Chapter 7 Island of Truth: http://hakank.org/picat/knights_and_knaves_lp.pi

Best,

Hakan

[Neng-Fa Zhou]

Puzzle 78 is easier to solve by hand than using a program. Below is my program for the puzzle. It is a plain Prolog program, which uses generate-and-test to search for the answer.

Cheers,

NF

/*

Teresa’s daughter is my daughter’s mother. What is my relationship to Teresa? Are you:
1. Teresa’s grandmother.
2. her mother.
3. her daughter.
4. her granddaughter.
5. Teresa.

*/

main :-
    given_condition(I),
    grandmother(I,teresa),
    println("Teresa’s grandmother."), !.
main :-
    given_condition(I),
    mother(I,teresa),
    println("Teresa’s mother."), !.
main :-
    given_condition(I),
    mother(teresa,I),
    println("Teresa’s daughter."), !.
main :-
    given_condition(I),
    grandmother(teresa,I),
    println("Teresa’s granddaughter."), !.
main :-
    given_condition(teresa),
    println("Teresa."), !.
main :-
    println("Unknown.").

given_condition(I) =>
    person(I),
    person(X),
    mother(teresa,X),
    person(Y),    
    mother(I,Y),
    mother(X,Y).
   
% X is Y's mother
mother(teresa,teresas_daughter).
mother(teresas_mother,teresa).
mother(teresas_grandmother,teresas_mother).
mother(teresas_daughter,teresas_granddaughter).

% X is Y's grandmother
grandmother(X,Y) :- mother(X,Z), person(Z), mother(Z,Y).

person(teresa).
person(teresas_daughter).
person(teresas_mother).
person(teresas_grandmother).
person(teresas_granddaughter).

[Hakan Kjellerstrand]

Hi Neng-Fa.

Thanks. Yes, the Teresa puzzle is much easier to solve by hand. May I add your solution to my collection (http://hakank.org/picat/#groza_puzzles) and - of course - attribute it to you?

By the way, I just got an idea how to model the Polyomino puzzles as a pure constraint model. The trickery is how to index the variants etc using matrix_element/4 (or perhaps element/3). Let's see how this works..

Best,

Hakan

[Hakan Kjellerstrand]

Neng-Fa's solution of the Teresa problem is here: http://hakank.org/picat/what_is_my_relation_to_teresa_nfz.pi . Thanks Neng-Fa.

I've continued to play with a "pure" constraint model for polyominos and had hoped that I should need to generate all the possible positions of the shape (+ rotations and flips),  but these approaches didn't work.

A work in progress of a pure CP/SAT model is available here: http://hakank.org/picat/polyominos_cp.pi

As a preprocessing step, it generates all possible positions that the shape (and its variants) can be placed in the grid.

The core model itself is quite simple (given the preprocessing), just two index lookups and an implication/equivalence to connect the value in the variant and X[I,J]:

   % ....

    foreach(I in 1..Rows)
      foreach(J in 1..Cols)
        % Select a variant
        Ix :: 1..FlattenLen,
        Ix #= (Variant[P]-1)*Rows*Cols + (I-1)*Cols + J,
        element(Ix,Flatten,Val),
        Val #= 1 #<=> X[I,J] #= P
      end

   % ...

For the hardest problem (go7/0) the jury is still out to prove unicity, but the time for printing the first (and unique) solution is about 20minutes. Much faster than the old program, but still too slow, but a progress.

Here are number of possible variants/symmetries (rotations + flips + any possible position in the grid) for each of the 12 pentominoes: [144,48,136,136,220,72,110,72,72,18,136,72] .

For the two problems with 6 pentominoes (go8/0 and go9/0) this SAT version is faster:

- go8/0:  31s (vs 115s for polyominos.pi)

- go9/0: 38s (vs 185s)

As for many CSP problems, the CP solver is faster than SAT for small(ish) problems, but for larger problems the SAT solver beats CP.

For example for go8/0:

- SAT solver 31s

- CP solver: 0.36s (!)

But then, for go9/0 the CP solver is much slower (over 10minutes).

I'm still playing with search strategies for the CP solver...

Best,

Hakan

[Neng-Fa Zhou]

Here is my program for Puzzle 172, which asks for packing of 12 pentominoes in a rectangle:

https://github.com/nfzhou/Picat/blob/master/pentominoes.pi

It uses a frame for each pentomino, and combines the frames to form the rectangle. It takes 0.2s to solve.

Cheers,

NF

[Mark Engelberg]

Couldn't no_overlap be replaced by a simple constraint that for each cell, the sum across all the PosMatrixes must be exactly 1?

[Hakan Kjellerstrand]

An update:

*  I have now completed the Polyomino Puzzles section. Still not fast enough, though.

   Here are the new puzzles solved:

   - Puzzle 130. Twelve pentominoes on a chessboard: http://hakank.org/picat/polyominos_cp.pi  (go11/0, first solution found in 4min30s)

   - Puzzle 132. A cut-up chessboard: http://hakank.org/picat/a_cut_up_chessboard.pi

* Chapter 6 Einstein puzzles is now completed. The new models:

  - Puzzle 57. Movies night: http://hakank.org/picat/movies_night.pi

  - Puzzle 58. Secret Santa: http://hakank.org/picat/secret_santa_groza.pi

  - Puzzle 60. Passengers in a railroad compartment:  http://hakank.org/picat/passengers_in_a_railroad_compartments.pi

* Chapter 8 Love and Marriage

  New model:

  - Puzzle 83. A family tree: http://hakank.org/picat/a_family_tree.pi

The TODOs:

* Chapter 8 Love and Marriage:

  - Puzzle 84. Uncles and aunts

* Chapter 10 Japanese Puzzles

  Puzzle 108. Sun and moon (Groza's description of this puzzle is not clear)

* Chapter 13 Self-reference and Other Puzzles

  Puzzle 141. Drinker paradox

And:

- speeding up the Polyomino solver

The full list of the puzzles:  http://hakank.org/picat/#groza_puzzles

Best,

Hakan

[Neng-Fa Zhou]

Thanks to Hakan, who pointed out a buggy behavior in my previous version. The overlap predicate is not implemented correctly. After the correction, the program becomes unsatisfiable. Later I realized that there are some shape variants that are impossible to obtain with only rotation. I have updated to program:

https://github.com/nfzhou/Picat/blob/master/pentominoes.pi

Now it takes the program 1m to solve the 12 pentominoes instance.

Coming to Mark Engelberg's question. Yes, it is possible to replace no_overlap with a simple equality constraint that ensures complete fill. I leave no_overlap as it is because the program can also do incomplete packing and it is not faster to replace no_overlap with a summation constraint. 

Cheers,

NF

[Hakan Kjellerstrand]

That's great, Neng-Fa!

On my machine, the following solution was found after 3min43s (which is quite faster than my model which takes about 20min to generate the first solution).

  7  7 10  5  5  5 12 11 11 11 11  9  6  1  4  4  4  8  8  8
  7 10 10 10  5  5 12 12 12 11  9  9  6  1  1  1  4  4  3  8
  7  7 10  2  2  2  2  2 12  9  9  6  6  6  1  3  3  3  3  8

A suggestion is to pretty print the solution by this instead:

print_matrix(M) =>
    foreach (I in 1..M.len)
      foreach(J in 1..M[1].len)
        printf("%3w",M[I,J])
      end,
      nl
    end,
    nl.

I have now linked to your solution at my Groza collection (http://hakank.org/picat/#groza_puzzles). Thanks!

Best,

Hakan

[Hakan Kjellerstrand]

Hi again, Neng-Fa.

I just updated your repo  and now the time to first solution is now 10.5s!  That's really great!

Best,

Hakan

[Hakan Kjellerstrand]

Finally, all 144 puzzles has now been modeled in Picat (either with an explicit reference to Groza's book or as a previous solution of the puzzle): http://hakank.org/picat/#groza_puzzles

Here are the last three puzzles that was solved:

- Puzzle 84. Uncles and aunts: http://hakank.org/picat/uncles_and_aunts.pi

- Puzzle 108. Sun and moon: http://hakank.org/picat/sun_and_moon.pi

-  Puzzle 141. Drinker paradox: http://hakank.org/picat/drinker_paradox.pi

The two puzzles "Uncles and Aunts" and "Sun and moon" was both last in each category (and thus the hardest) and they was indeed quite messy, especially the Sun and moon puzzle.

The solution of the "Drinker paradox" in the book is a Prover9 proof, though I just did a constraint model showing the contradiction (two solutions). If anyone have a better way to prove this paradox in Picat, feel free to show it.

Also, Groza has now added an errata on his book code site: https://users.utcluj.ro/~agroza/puzzles/maloga/codes.html  (including reports from your truly) as well as a link to my Picat solutions.

Thanks Neng-Fa for the help/inspiration with some of these puzzles.

Best,

Hakan

[Hakan Kjellerstrand]

Forgot to mention the GitHub commit for the solutions previously not committed:

https://github.com/hakank/hakank/commit/8c9099d8f35e0e06c480681bf7403a72447cc4ef

/Hakan

[Neng-Fa Zhou]

Congratulations, Hakan, for completing another great project. Your set of examples will be a valuable asset for the Picat community. I am amazed by your productivity. I am also impressed with the solidness of the Picat system as you didn't encounter even a single bug while writing and testing these  over 144 programs.  I am pretty sure that you have a long list of to-do lists for  perfecting the Picat system. You have made hug contributions to bringing Picat to the current state. Let's make Picat even greater.

Best,

Neng-Fa

[Peter Ludemann]

The sources seem to have an encoding problem (e.g., the comment starting at line 55 in http://hakank.org/picat/logic_equation.pi)

Is there an encoding setting that's missing? (I tried adding an Emacs "coding: utf-8" comment at the beginning, but that didn't work)

[Hakan Kjellerstrand]

Hi Peter.

Thanks for the report. It should be fixed now.

I though I've fixed these already. Some of the problem description are from Groza's electronic book/paper which contains characters that are might look  strange in a text file.

Best,

Hakan

[Hakan Kjellerstrand]

Hi Neng-Fa.

Thanks for your kind words.

Yes, Picat seems to be quite stable now which is great.

I might look into a regular/6 version for the polyomino puzzle, though converting the shapes and their symmetries to a huge DFA will take time and is tedious. And I'm not sure that it will be faster than your version either, which is - of course - a goal :-).

Best,

Hakan

[Claudio Cesar de Sá]

In the sequence of Neng-Fa:

Following the  Neng-Fa words to express  what Hakan represents for the Constraint Programming community.
I've been following Hakan for almost 15 years and his codes have become a reference everywhere.
Not just codes in Picat, but in several other solvers and CP languages.

Furthermore, Hakan is always ready to help us with any questions here on the list and other site, such as StackOverflow, for example.

Hakan, as well as others here on Picat's list (in addition to Neng-Fa, Peter, etc... yes there are others) have contributed a lot to the growth of this language with its roots back in Prolog, which has  more than 50 years old .

Thank you all to Hakan, Neng-Fa, Peter .... surely this list will be incomplete.

Thans for all

[jf]

Hello,

I think there is a small mistake in your solution of "Puzzle 103. Daily neighbours"

at http://hakank.org/picat/daily_neighbours.pi

Instead of

X-0-X-X".split("\n").

should be

X-0.X-X".split("\n").

Thank you very much for so many Picat examples.

Josef

Dne pátek 19. ledna 2024 v 10:05:17 UTC+1 uživatel Hakan Kjellerstrand napsal:

[Hakan Kjellerstrand]

Thanks for the report. Josef.

It's fixed now: http://hakank.org/picat/daily_neighbours.pi

Best,

Hakan

[jf]

Out of my laziness I stole your data for my experiment and the punishment came soon: I could not get my program working :-)

Best regards

Josef

Dne úterý 12. března 2024 v 17:58:07 UTC+1 uživatel Hakan Kjellerstrand napsal:

[jf]

Hello,

I tried to solve the polyomino 127 from Groza using exact cover problem (but not DEK algorithm).

Solution came in 13s, all 8 in 56s. No idea how to solve p's with holes.

Best regards

Josef

/*
  From Adrian Groza "Modelling Puzzles in First Order Logic"    
  - Puzzle 127. The 12 pentominoes

*/

import sat, util.

mainx => polyomino(127, _Vysl, 1).

main(Pol) =>
   Polyomino = Pol[1].to_int(),
   Results = findall(Results, polyomino(Polyomino, Results, 0)).sort().remove_dups(),
   nl,

   foreach ( Res in Results )
      vypis(Res),
      nl
   end,
   printf("Number of solutions: %d\n", Results.len()).

% gets the Tiles, Pr 0/1 if print or not
polyomino(Polident, Result, Pr) =>
   once genmatrix(Polident, Numberoftiles, Boardheight, Boardwidth, Tlnumbers, Matr),
   Mc = Matr.columns(),
   Numberofcolumns = Mc.len(),

   Indexes = [],
   foreach ( T in 1..Numberoftiles )
      element(Ind, Tlnumbers, T),
      Indexes := [Ind|Indexes]
   end,

   Totvals = [],
   foreach ( Col in 1..Numberofcolumns )
      Vals = [],
      foreach ( I in 1..Numberoftiles )
         element( Indexes[I], Mc[Col], Val ),
         Vals := [Val|Vals]
      end,
      Totvals := [Vals|Totvals],
      sum(Vals) #= 1
   end,

   if Pr == 1 then println("Solving...") end,
   % solve(Indexes),  % slower
   solve(Indexes ++ Totvals.vars()),
   if Pr == 1 then println("Solved"), nl end,

   once getresults(Matr, Indexes, Boardheight, Boardwidth, Numberoftiles, Result),

   if ( Pr == 1 ) then
      printf("Polyomino: %w   Number of tiles: %d   Size: %dx%d\n", Polident, Numberoftiles, Boardheight, Boardheight),
      printf("Matrix dimension: %d x %d\n\n", Matr.len(), Numberofcolumns),
      println("Lines selected from the matrix:"),nl,
      foreach ( I in Indexes )
         printf("%4d: %w\n", I, Matr[I])
      end,
      nl,
      println("Result:"), nl,
      vypis(Result),
      nl
   end.

% Matrix Result with different integers for each tile
getresults(Matr, Indexes, Rownum, Colnum, Numberoftiles, Result) =>
   Result = new_array(Rownum, Colnum),
   foreach ( Tileno in 1..Numberoftiles )
      Line = Matr[Indexes[Tileno]],
      foreach ( N in 1..Line.len() )
         if ( Line[N] > 0 ) then
            rowcol(N, Row, Col, Colnum),
            Result[Row,Col] = Tileno
         end
      end
   end.

rowcol(N, Row, Col, Boardwidth) =>   % ...
   Row = 1 + floor(N / (Boardwidth+0.1)),
   Col = N - floor(N / (Boardwidth+0.1) ) * Boardwidth.

% output
vypis(Result) =>
   Rows = Result.len(),
   Cols = Result[1].len(),
   foreach ( Row in 1..Rows )
      foreach ( Col in 1..Cols )
         printf(" %2d", Result[Row,Col])
      end,
      nl
   end,
   nl.

% generates (big) matrix, lines are "flattened" tiles
genmatrix(Polyident, Numberoftiles, Boardheight, Boardwidth, Tlnumbers, Matrix) =>
   polyomino(Polyident, Tilelist, Boardheight, Boardwidth, Numberoftiles, Rotations),
   findtiles(Tilelist, Numberoftiles, Polytiles),
   findmaxdim(Polytiles, Maxtiledim),
   Matrixtmp = [],
   Tlnumberstmp = [],
   foreach ( I in 1..Numberoftiles )
      Polytiles[I] = {Polynum, Polytile},
      transftile(Polytile, Rotations[I], Boardheight, Boardwidth, Polytiletrans),
      foreach ( Polytiletran in Polytiletrans )
         Polyheight = Polytiletran.len(),
         Polywidth = Polytiletran[1].len(),
         foreach ( Rowstart in 0..Boardheight-Polyheight )
            foreach ( Colstart in 0..Boardwidth-Polywidth )
               flattenpol(Polytiletran, Polynum, Maxtiledim, Boardheight, Boardwidth, Rowstart, Colstart, Row),
               Matrixtmp := [Row|Matrixtmp],
               Tlnumberstmp := [Polynum|Tlnumberstmp]
            end
         end
      end
   end,

   Tlnumbers = Tlnumberstmp.reverse(),
   Matrix = Matrixtmp.reverse().

findtiles(Tilelist, Numberoftiles, Tiles) =>
   Tiles = new_list(Numberoftiles),
   foreach ( I in 1..Numberoftiles )
      p(Tilelist[I], Tile),
      Tiles[I] = {I,Tile}
   end.

% generates instances of each tile: no rotate, rotate, rotate+flip
% removes duplicates and oversize tile variants
transftile(Polytile, norot, _, _, Poltiletrans) =>
   Poltiletrans = [Polytile].
transftile(Polytile, rot, Boardheight, Boardwidth, Poltiletrans) =>
   rotate90(Polytile, Polytile90),
   rotate180(Polytile, Polytile180),
   rotate270(Polytile, Polytile270),
   Dtmp = [ Polytile, Polytile90, Polytile180, Polytile270 ].remove_dups(),
   Poltiletrans = [ X : X in Dtmp, X.len() <= Boardheight, X[1].len() <= Boardwidth ].
transftile(Polytile, rotfl, Boardheight, Boardwidth, Poltiletrans) =>
   rotate90(Polytile, Polytile90),
   rotate180(Polytile, Polytile180),
   rotate270(Polytile, Polytile270),
   horizontal_flip(Polytile, Polytilefliph),
   rotate90(Polytilefliph, Polytilefliph90),
   rotate180(Polytilefliph, Polytilefliph180),
   rotate270(Polytilefliph, Polytilefliph270),
   Dtmp = [ Polytile, Polytile90, Polytile180, Polytile270, Polytilefliph, Polytilefliph90, Polytilefliph180, Polytilefliph270 ].remove_dups(),
   Poltiletrans = [ X : X in Dtmp, X.len() <= Boardheight, X[1].len() <= Boardwidth ].

findmaxdim(Tiles, Maxtiledim) =>
   findmaxdim(Tiles, 0, Maxtiledim).

findmaxdim([{_,Polytile}|Polytiles], Tmp, Maxtiledim) ?=>
   Tmp1 = max( [Polytile.len(), Polytile[1].len(), Tmp]),
   findmaxdim(Polytiles, Tmp1, Maxtiledim).
findmaxdim([], Tmp, Maxtiledim) =>
   Maxtiledim = Tmp.

% flattens the tile, background zero
flattenpol(Polytile, Polynum, Maxtiledim, Boardheight, Boardwidth, Rowstart, Colstart, Row) =>
   Polyheight = Polytile.len(),
   Polywidth = Polytile[1].len(),
   Row = new_list(Boardheight*Boardwidth),
   Row :: [0,1],
   foreach ( R in 1..Polyheight )
      foreach ( C in 1..Polywidth )
         if ( Polytile[R,C] > 0 ) then
            Row[(R-1)*Boardwidth + Rowstart*Boardwidth + C + Colstart] = 1
         end
      end
   end,
   foreach ( I in 1..Row.len() )
      ( Row[I] = 0 ; true )
   end.

% stolen from / inspired by: http://hakank.org/picat/rectangle_symmetries.pi
% Rotate 90 degrees
rotate90(Shape, Rotated) =>
    transpose(Shape, Transposed),
    reverse_each_row(Transposed, Rotated).

% Rotate 180 degrees
rotate180(Shape, Rotated) =>
   rotate90(Shape, Tmp),
   rotate90(Tmp, Rotated).

% Rotate 270 degrees
rotate270(Shape, Rotated) =>
   rotate90(Shape, Tmp1),
   rotate90(Tmp1, Tmp2),
   rotate90(Tmp2, Rotated).

% Horizontal Flip
horizontal_flip(Shape, Flipped) =>
    reverse(Shape, Flipped).

% Helper function to reverse each row
reverse_each_row([], []).
reverse_each_row([Row|Rows], [ReversedRow|ReversedRows]) :-
    reverse(Row, ReversedRow),
    reverse_each_row(Rows, ReversedRows).

transpose(Matrix,Transposed) =>
  Transposed = [[Matrix[J,I] : J in 1..Matrix.len] : I in 1..Matrix[1].len].

reverse(L, Rev) =>
  Rev = reverse(L).

% --------< DATA >--------------------------
polyomino(122, Tilelist, Rownum, Colnum, Tilesnum, Rotations) =>
   Tilelist = [ i3, l2, i2, dot ],
   Rownum = 3,
   Colnum = 3,
   Tilesnum = Tilelist.len(),
   Rotations = [norot,norot,norot,norot].
polyomino(123, Tilelist, Rownum, Colnum, Tilesnum, Rotations) =>
   Tilelist = [ i3, l2, i2, dot ],
   Rownum = 3,
   Colnum = 3,
   Tilesnum = Tilelist.len(),
   Rotations = [rot,rot,rot,rot].
polyomino(124, Tilelist, Rownum, Colnum, Tilesnum, Rotations) =>
   Tilelist = [ u, dot, zi, i3, li3, zf, ti, tis, dash2, li2 ],
   Rownum = 6,
   Colnum = 6,
   Tilesnum = Tilelist.len(),
   Rotations = [norot,norot,norot,rot,norot,norot,norot,norot,rot,rot].
polyomino(125, Tilelist, Rownum, Colnum, Tilesnum, Rotations) =>
   Tilelist = [ u, dot, zi, i3, li3, zf, ti, tis, dash2, li2 ],
   Rownum = 6,
   Colnum = 6,
   Tilesnum = Tilelist.len(),
   Rotations = [norot,norot,norot,norot,norot,norot,norot,norot,norot,norot].
polyomino(126, Tilelist, Rownum, Colnum, Tilesnum, Rotations) =>
   Tilelist = [ l, pi, yi, w ],
   Rownum = 4,
   Colnum = 5,
   Tilesnum = Tilelist.len(),
   Rotations = [rot,rot,rot,rot].
polyomino(127, Tilelist, Rownum, Colnum, Tilesnum, Rotations) =>
   Tilelist = [ t, u, w, v, x, yi, z, f, i5, l, pi, n ],
   Rownum = 3,
   Colnum = 20,
   Tilesnum = Tilelist.len(),
   Rotations = [rotfl,rotfl,rotfl,rotfl,rotfl,rotfl,rotfl,rotfl,rotfl,rotfl,rotfl,rotfl].
polyomino(128, Tilelist, Rownum, Colnum, Tilesnum, Rotations) =>
   Tilelist = [ t, w, yi, z, i5, l ],
   Rownum = 5,
   Colnum = 6,
   Tilesnum = Tilelist.len(),
   Rotations = [rotfl,rotfl,rotfl,rotfl,rotfl,rotfl].
polyomino(129, Tilelist, Rownum, Colnum, Tilesnum, Rotations) =>
   Tilelist = [ u, v, x, f, pi, n ],
   Rownum = 5,
   Colnum = 6,
   Tilesnum = Tilelist.len(),
   Rotations = [rotfl,rotfl,rotfl,rotfl,rotfl,rotfl].

p(i3, [[1],
       [1],
       [1]]).

p(l2, [[1,0],
       [1,1]]).
p(i2, [[1],
       [1]]).
p(dot, [[1]]).
p(u, [[1,0,1],
      [1,1,1]]).
p(zi, [[0,1,1],
      [0,1,0],
      [1,1,0]]).
p(li3, [[1,1],
        [1,0],
        [1,0]]).
p(zf, [[1,1,0],
       [0,1,1]]).
p(ti, [[0,1,0],
       [0,1,0],
       [1,1,1]]).
p(tis, [[0,1,0],
        [1,1,1]]).
p(dash2, [[1,1]]).
p(li2, [[10,10],
        [0,10]]).
p(l, [[1,0],
      [1,0],
      [1,0],
      [1,1]]).
p(pi, [[0,1],
       [1,1],
       [1,1]]).
p(yi, [[0,1],
       [1,1],
       [0,1],
       [0,1]]).
p(w, [[1,0,0],
      [1,1,0],
      [0,1,1]]).
p(t, [[1,1,1],
      [0,1,0],
      [0,1,0]]).
p(v, [[1,0,0],
      [1,0,0],
      [1,1,1]]).
p(x, [[0,1,0],
      [1,1,1],
      [0,1,0]]).
p(z, [[1,1,0],
      [0,1,0],
      [0,1,1]]).
p(f, [[0,1,1],
      [1,1,0],
      [0,1,0]]).
p(i5, [[1],
       [1],
       [1],
       [1],
       [1]]).
p(n, [[0,1],
      [0,1],
      [1,1],
      [1,0]]).
p(zero22, [[1,1],
       [1,1]]).

Dne úterý 12. března 2024 v 18:46:39 UTC+1 uživatel jf napsal:

[Neng-Fa Zhou]

Wow, you model is much faster than Hakan's and mine.  Could you write a short description of your model? What do you mean by "exact cover" and "p's with holes"?

Thanks,

NF

[jf]

Pentomino solving:

please look at:
https://boyetblog.s3.amazonaws.com/PCPlus/294.pentominoes.pdf

Flattening a tile:
10
11
becomes on 3 columns wide  board
100110000

and all possible various positions (no transformations in 122 puzzle):
100110000
010011000     -> right
000100110     -> down
000010011     -> down and right

Matrix where lines are formed by all possible transformations for all
tiles is created.
Article continues with description of D.E. Knuth's algorithm X to find,
which columns of this matrix contain exactly one '1', but I have not
used his algorithm (maybe it is faster..?).

Next part is selection of one of trasformations of each tile where
all columns sum to 1 from the matrix.

Tlnumbers is the list with number of each tile (Groza 122, 3x3):
[1,1,1,2,2,2,2,3,3 ..., corresponds to the Matrix lines.
Indexes [_0140a0::[1..3],_0141a0::[4..7] ... are used
to link Matrix lines and Tiles. Selected lines can be printed
and all columns must sum to 1.

The rest is final tile numbering and output.

Best regards
Josef

Dne čtvrtek 18. dubna 2024 v 4:17:54 UTC+2 uživatel Neng-Fa Zhou napsal:

[Neng-Fa Zhou]

Thanks for the explanation. It's interesting to set up the pentominoes problem as an exact cover problem. Your model for the exact cover problem uses element constraints. I would use a binary variable for each row,  which is 1 iff the the row is selected, and generate constraints to ensure that every square column is covered by the set of selected rows.

Cheers,

NF

[Peter Bernschneider]

Based on your programs and helpful hints I created the12pentominos.pi which is even a bit faster: 1.141 seconds for the 3x20 grid on my MacBook (compared to 18 seconds for Josef´s program).

[Neng-Fa Zhou]

Thank you, Peter, for the program. On my computer it returns all 8 solutions in 15s. Very impressive! This examples demonstrate the importance of modeling.

Cheers,

NF 

[Neng-Fa Zhou]

Hi Peter,

Your program is concise and elegant. I really like it. I have a couple of comments. First,  the article (https://boyetblog.s3.amazonaws.com/PCPlus/294.pentominoes.pdf) states that there are 1168 rows in the exact cover matrix, while you program creates a matrix with 1236 rows. Either the number 1168 is wrong, or the number 1236 is not optimal. Second, your program uses an array (Select) to indicate which rows are selected. While there is a constraint (sum(Select) #= 12), which constrains the total number of selected rows, there are not constraints that force exactly one variant of each pentomino to be selected. Will addition of such constraints improve the performance?

Cheers,

Neng-Fa 

On Sunday, April 21, 2024 at 12:05:20 PM UTC-4 peterbern...@googlemail.com wrote:

[Peter Bernschneider]

Good morning Neng-Fa,

I double checked the difference in number of rows between the PCplus article and my computation. I found that the only difference is for the N-pentomino: PCplus counts 68  lines and I get 136 = 17 columns * 2 rows * 4 reflections. Also 136 is the number we both count for Y and L, because the pentominos N, Y and L exactly fit into a 4 x 2 rectangle. Maybe PCplus is wrong?

The constraint sum(Select) #= 12 is redundant, because the first 12 columns signify the pentomino number and so the Exact Cover constraint (line 19) ensures, that for each pentomino exactly one instance is selected. BTW: When I remove the redundant constraint, the correct result is found in 1.299 seconds CPU time.

In fact an alternative approach would be to use subarrays of Select for each pentomino and constrain sum(Selcect[1..18])  #= 1 for X and so on for the other pentominos. With this approach we only need 3 * 20 = 60 columns for the Exact Cover matrix M. I tried this approach, but found no solution (CPU time 19.632 seconds). 

Cheers, Peter

[Neng-Fa Zhou]

Thanks, Peter, for the experimentation. I can confirm that the number of rows in the exact cover matrix for 3*20 is 1236. That means that the number given in the paper is wrong.

With an exactly one constraint for each pentomino, the program becomes almost twice as fast as the original one. Here is my modified version:

https://github.com/nfzhou/Picat/blob/master/pentominoes2.pi

Cheers,

NF