at a meetup someone mentioned a game for which they wanted to generate challenges with unique solutions and i proposed to use z3 for this

z3_sudoku_like.py

# modeled after https://ericpony.github.io/z3py-tutorial/guide-examples.htm
# at a meetup someone mentioned a game for which they wanted to generate challenges with unique solutions and i proposed to use z3 for this

# the rules are similar to sudoku
# there are two symbols represented as -1 and 1 because this made calculations easier

from z3 import *
from itertools import *
import numpy as np

# 8x8 matrix of integer variables
X = [[Int("x_%s_%s" % (i+1, j+1)) for j in range(8)]
     for i in range(8)]

# each cell contains a value of either -1 or 1
cells_c = [Or(1 == X[i][j], X[i][j] == -1)
           for i in range(8) for j in range(8)]


def transpose(m):
    return list(map(list, zip(*m)))


def tripples(iterable):
    a, b = tee(iterable)
    b2, c = tee(b)
    next(b2, None)
    next(c, None)
    next(c, None)
    return zip(a, b2, c)


# same number of -1 and 1 in each row and each column
eq = [Sum(list(X[i][j] for i in range(8))) == 0 for j in range(8)]
eq += [Sum(list(X[i][j] for j in range(8))) == 0 for i in range(8)]


# vert and horitzontal may be mixed up, sorry
# all rows and all columns must be unique, could use z3 Dinstinct here but did not figure it out
dist_vert = [X[i] != X[j]
             for i in range(8) for j in range(8) if j != i]

dist_hor = [transpose(X)[i] != transpose(X)[j]
            for i in range(8) for j in range(8) if j != i]

# no two after each other
two_vert = [Not(And((x1 == x2), (x2 == x3)))
            for i in range(8) for (x1, x2, x3) in tripples(X[i])]

two_horiz = [Not(And((x1 == x2), (x2 == x3)))
             for i in range(8) for (x1, x2, x3) in tripples(transpose(X)[i])]


sudoku_c = cells_c + eq + dist_vert + dist_hor + two_vert + two_horiz

# sudoku_like instance, we use '0' for empty cells
# example of a puzzle with unique solution
instance = ((1, 1, 0, 0, 1, 0, 0, 1),
            (0, 1, 0, 0, 1, 1, 0, 1),
            (0, 0, 1, 1, 0, 1, 0, 0),
            (0, 0, 0, 0, 0, 0, 1, 1),
            (0, 0, 0, 0, 0, 0, 0, 0),
            (0, 0, 0, 0, 0, 0, 0, 0),
            (0, 0, 1, 0, 1, 0, 1, 1),
            (0, 0, 0, 0, 0, 0, 1, 0))

# not unique example
# instance = ((1, 0, 0, 0, 0, 0, 0, 0),
#             (0, 0, 0, 0, 0, 0, 0, 0),
#             (0, 0, 0, 0, 0, 0, 0, 0),
#             (0, 0, 0, 0, 0, 0, 0, 0),
#             (0, 0, 0, 0, 0, 0, 0, 0),
#             (0, 0, 0, 0, 0, 0, 0, 0),
#             (0, 0, 0, 0, 0, 0, 0, 0),
#             (0, 0, 0, 0, 0, 0, 0, 0))


instance_c = [If(instance[i][j] == 0,
                 # this means, if instance[i][j] is 0, the formula is satisfied
                 True,
                 # if instance[i][j] != 0 it has to match the value in instance, in order to be satisfied
                 X[i][j] == instance[i][j])
              for i in range(8) for j in range(8)]

s = Solver()
s.add(sudoku_c + instance_c)
if s.check() == sat:
    m = s.model()
    r = [[m.evaluate(X[i][j]) for j in range(8)]
         for i in range(8)]
    print_matrix(r)

    # check unique
    # there must not exist another model that differs in more than one position
    s.add(Or([X[i][j] != r[i][j] for i in range(8) for j in range(8)]))

    if s.check() == sat:
        print("not a unique solution, other solution is:")
        m = s.model()
        r2 = [[m.evaluate(X[i][j]) for j in range(8)]
              for i in range(8)]
        print_matrix(r2)
        assert(r2 != r)
    else:
        print("no other model found")

else:
    print("failed to solve, not even one model exists")