How to find 3 triangles passing through every dot of a 5x5 grid in z3

Solution 1:

Here is my attempt:

    from z3 import *
    
    # https://stackoverflow.com/questions/70565942/how-to-find-3-triangles-passing-through-every-dot-of-a-5x5-grid-in-z3
    
    s = Solver()
    n = 7
    triangles = 4
    Cells = range(n * n)
    N = range(n)
    Triangles = range(triangles)
    corners = 3
    Corners = range(corners)
    
    
    #  triangles have three grid points each;
    #  row and column values are kept in two vectors
    Trow = [IntVector("tr" + str(t+1), corners) for t in Triangles]
    Tcol = [IntVector("tc" + str(t+1), corners) for t in Triangles]
    
    #  save some [] typing        
    def Row(t, c):
        return Trow[t][c]
    
    def Col(t, c):
        return Tcol[t][c]
    
    def ShowTriangle(model, t):
        print()
        print("Triangle " + str(t+1))
        for e in Corners:
            row = model.eval(simplify(Row(t, e)+1))
            col = model.eval(simplify(Col(t, e)+1))
            s = "col " + str(col).ljust(4) + "; row " + str(row).ljust(4)
            print(s)
        for row in N:
            s = ""
            for col in N:
                if model.eval(IsOnTriangle(n-1-row, col, t)):
                    s = s + str(t+1)
                else:
                    s = s + "."
            print(s)
    
    
    def InInterval(x, a, b):
        return And(x >= a, x <= b)
    
    #  a grid point is covered by a given triangle, if it is located
    #  on an edge of the triangle
    def IsOnTriangle(row, col, t):
        return Or(IsOnEdge(row, col, t, 0, 1),
                  IsOnEdge(row, col, t, 1, 2),
                  IsOnEdge(row, col, t, 0, 2))
    
    def IsOnEdge(row, col, t, c0, c1):
        row0 = Row(t, c0)
        row1 = Row(t, c1)
        col0 = Col(t, c0)
        col1 = Col(t, c1)
        #  for the time being, we disregard skewed edges
        return Or(IsOnHorizontalEdge(row, col, row0, col0, row1, col1), 
                  IsOnVerticalEdge(row, col, row0, col0, row1, col1),
                  IsOnMainDiagonalEdge(row, col, row0, col0, row1, col1),
                  IsOnSecondaryDiagonalEdge(row, col, row0, col0, row1, col1))
    
    def Equal3(x, a, b):
        return And(x == a, x == b)
    
    def IsOnHorizontalEdge(row, col, row0, col0, row1, col1):
        return And(Equal3(row, row0, row1), 
                   InInterval(col, col0, col1))
    
    def IsOnVerticalEdge(row, col, row0, col0, row1, col1):
        return And(Equal3(col, col0, col1), 
                   InInterval(row, row0, row1))
    
    def IsOnMainDiagonalEdge(row, col, row0, col0, row1, col1):
        return Or(And(row0 < row1, 
                      col0 < col1, 
                      (row - row0) == (col - col0), 
                      (row1 - row) == (col1 - col), 
                      InInterval(row, row0, row1), 
                      InInterval(col, col0, col1)), 
                  And(row0 > row1, 
                      col0 > col1, 
                      (row - row1) == (col - col1), 
                      (row0 - row) == (col0 - col), 
                      InInterval(row, row1, row0), 
                      InInterval(col, col1, col0)))
    
    def IsOnSecondaryDiagonalEdge(row, col, row0, col0, row1, col1):
        return Or(And(row0 < row1, 
                      col0 > col1, 
                      (row - row0) == (col0 - col), 
                      (row1 - row) == (col - col1),
                      InInterval(row, row0, row1),
                      InInterval(col, col1, col0)), 
                  And(row0 > row1, 
                      col0 < col1, 
                      (row - row1) == (col1 - col), 
                      (row0 - row) == (col - col0),
                      InInterval(row, row1, row0),
                      InInterval(col, col0, col1)))
    
    #  every grid position has to be visited by at least one triangle
    for row in N:
        for col in N:
            s.add(Or([IsOnTriangle(row, col, t) for t in Triangles]))
    
    # delimit triangles to grid
    for t in Triangles:
        for e in Corners:
            s.add(Row(t, e) >= 0, 
                  Row(t, e) < n, 
                  Col(t, e) >= 0, 
                  Col(t, e) < n)
    
    #  enforce order of corners
    #  to reduce symmetries
    for t in Triangles:
        for e in range(corners-1):
            s.add(Row(t, e) <= Row(t, e+1))
    
    #  enforce order of triangles
    #  to reduce symmetries
    for t in range(triangles-1):
        s.add(Row(t, 0) <= Row(t+1, 0))
    
    if sat == s.check():
        print("sat")
        for t in Triangles:
            ShowTriangle(s.model(), t)
    else:
        print("no solution found!")

Resulting output for 4 triangles in a 7x7 grid:

sat

Triangle 1
col 1   ; row 1   
col 7   ; row 1   
col 1   ; row 7   
1......
11.....
1.1....
1..1...
1...1..
1....1.
1111111

Triangle 2
col 2   ; row 2   
col 7   ; row 2   
col 2   ; row 7   
.2.....
.22....
.2.2...
.2..2..
.2...2.
.222222
.......

Triangle 3
col 7   ; row 3   
col 3   ; row 7   
col 7   ; row 7   
..33333
...3..3
....3.3
.....33
......3
.......
.......

Triangle 4
col 2   ; row 3   
col 6   ; row 3   
col 6   ; row 7   
.....4.
....44.
...4.4.
..4..4.
.44444.
.......
.......

As commented by @alias, this is probably not suitable for a first Z3 exercise. My model won't find solutions with triangles where the edges are skewed (neither horizontal, nor vertical, nor diagonal). Adding symmetry breaking constraints helped to speed-up the search for the 7x7 case.

A similar model written for MiniZinc:

int: n = 5;  %  grid dimension
set of int: N = 1..n;
int: triangles = 3;
int: corners = 3;
set of int: Triangles = 1..triangles;
set of int: Corners = 1..corners;

%  triangles have three row/column grid points each.
array[Triangles, Corners] of var 1..n: Row;
array[Triangles, Corners] of var 1..n: Col;
    
%  a grid point is covered by a given triangle, if it located
%  on an edge of the triangle
function var bool: IsOnTriangle(N: row, N: col, Triangles: t) =
    IsOnEdge(row, col, Row[t, 1], Col[t, 1], Row[t, 2], Col[t, 2]) \/
    IsOnEdge(row, col, Row[t, 1], Col[t, 1], Row[t, 3], Col[t, 3]) \/
    IsOnEdge(row, col, Row[t, 2], Col[t, 2], Row[t, 3], Col[t, 3]);
    
function var bool: Equal3(N: x, var N: a, var N: b) =
    (x == a) /\ (x == b);
    
function var bool: IsOnEdge(N: row, N: col, var N: aRow, var N: aCol, var N: bRow, var N: bCol) =
    IsOnHorizontalEdge(row, col, aRow, aCol, bRow, bCol) \/
    IsOnVerticalEdge(row, col, aRow, aCol, bRow, bCol) \/
    IsOnDiagonalEdge(row, col, aRow, aCol, bRow, bCol);
        
function var bool: InInterval(N: x, var N: a, var N: b) =
    if x >= a then x <= b else x >= b endif;
    
function var bool: IsOnHorizontalEdge(N: row, N: col, 
                                      var N: aRow, var N: aCol, 
                                      var N: bRow, var N: bCol) =
    Equal3(row, aRow, bRow) /\ 
    InInterval(col, aCol, bCol);

function var bool: IsOnVerticalEdge(N: row, N: col, 
                                    var N: aRow, var N: aCol, 
                                    var N: bRow, var N: bCol) =
    Equal3(col, aCol, bCol) /\ 
    InInterval(row, aRow, bRow);
   
function var bool: IsOnDiagonalEdge(N: row, N: col, 
                                    var N: aRow, var N: aCol, 
                                    var N: bRow, var N: bCol) =
    InInterval(row, aRow, aCol) /\
    InInterval(col, aCol, bCol) /\
    (IsOnMainDiagonalEdge(row, col, aRow, aCol, bRow, bCol) \/
     IsOnSecondaryDiagonalEdge(row, col, aRow, aCol, bRow, bCol));

function var bool: IsOnMainDiagonalEdge(N: row, N: col, 
                                        var N: aRow, var N: aCol, 
                                        var N: bRow, var N: bCol) =
    ((aRow < bRow) /\ (aCol < bCol) /\
    ((row - aRow) == (col - aCol)) /\
    ((bRow - row) == (bCol - col))) \/ 
    ((aRow > bRow) /\ (aCol > bCol) /\
    ((row - bRow) == (col - bCol)) /\
    ((aRow - row) == (aCol - col)));     
 
function var bool: IsOnSecondaryDiagonalEdge(N: row, N: col, 
                                             var N: aRow, var N: aCol, 
                                             var N: bRow, var N: bCol) =
    ((aRow < bRow) /\ (aCol > bCol) /\
    ((row - aRow) == (aCol - col)) /\
    ((bRow - row) == (col - bCol))) \/ 
    ((aRow > bRow) /\ (aCol < bCol) /\
    ((row - bRow) == (bCol - col)) /\
    ((aRow - row) == (col - aCol)));     
                
%  every grid position has to be visited by at least one triangle
constraint forall(row in N, col in N) (
    exists([IsOnTriangle(row, col, t) | t in Triangles])
    );

%  prune symmetries to speed-up the search

constraint forall(t in Triangles) (
    forall(e in 1..corners-1) (
        Row[t, e] <= Row[t, e+1]
    )
);

constraint forall(t in 1..triangles-1) (
    Row[t, 1] <= Row[t+1, 1]
);

output [ "\nTriangle \(t): \(Col[t, c]);\(Row[t, c])" | t in Triangles, c in Corners];