A z3 solver based solution for the unique sum sudoku puzzle by myxo and `I love sleeping`

z3-4x4-unique-sum-sudoku.py

#!/usr/bin/env python3

# https://sudokupad.app/nLjQ8DjNRJ
# "Unique Sum Sudoku"
# By I Love Sleeping & Myxo
# Normal sudoku rules do NOT apply. Fill the grid with digits 1-9, such that no digit repeats in any row, column or box. The set of digits in each row or column is unique, eg. if a row contains the digits 1234, no other row or column may contain exactly those digits. The digits in every row, column and box sum to x, where x has to be determined by the solver. Digits separated by an X sum to 10. Digits separated by a V sum to 5. Not all Xs and Vs are necessarily given.
# Featured in video: "How Hard Can A 4x4 Sudoku Be?" - Cracking The Cryptic
# https://www.youtube.com/watch?v=JvbnQMzOHhI

from itertools import permutations
import z3

solver = z3.Solver()

grid = [[z3.Int(f'g_{r}_{c}') for c in range(4)] for r in range(4)]


def transpose(grid):
    return [[grid[j][i] for j in range(len(grid))] for i in range(len(grid[1]))]


def boxes(grid):
    boxes = [[], [], [], []]
    for row in range(4):
        for col in range(4):
            boxes[(row // 2) * 2 + (col // 2)].append(grid[row][col])
    return boxes


########  SUDOKU RULES ###############

for row in grid:
    for var in row:
        solver.add(0 < var, var < 10)

for row in grid:
    solver.add(z3.Distinct(*row))

for col in transpose(grid):
    solver.add(z3.Distinct(*col))

for box in boxes(grid):
    solver.add(z3.Distinct(*box))

######## SAME SUM CONSTRAINTS ########

sum_X = z3.Sum(grid[0])

for row in grid:
    solver.add(z3.Sum(row) == sum_X)

for col in transpose(grid):
    solver.add(z3.Sum(col) == sum_X)

for box in boxes(grid):
    solver.add(z3.Sum(box) == sum_X)

######## SUM CONSTRAINTS #############

sums = {
    5: [
        ((0, 0), (0, 1)),
        ((1, 2), (2, 2)),
    ],
    10: [
        ((0, 3), (1, 3)),
        ((1, 1), (1, 2)),
        ((2, 1), (3, 1)),
    ],
}

for sum, pairs in sums.items():
    for (r1, c1), (r2, c2) in pairs:
        solver.add(grid[r1][c1] + grid[r2][c2] == sum)

######## SET DISTINCT ################


def set_distinct(row1, row2):
    return z3.Not(
        z3.Or(
            [
                z3.And([row1[i] == row2[p[i]] for i in range(4)])
                for p in permutations(range(4))
            ]
        )
    )


rows_and_cols = [*grid, *transpose(grid)]

for i, el1 in enumerate(rows_and_cols):
    for el2 in rows_and_cols[i + 1 :]:
        solver.add(set_distinct(el1, el2))

######################################

def print_solution(m):
    for row in grid:
        print(*["%2s" % m.eval(ele) for ele in row])

    print(f'\nTotal sum: {m.eval(sum_X)}')

print('---- solving ----')


if solver.check() == z3.sat:
    print('---- solved -----\n')

    m = solver.model()
    print_solution(m)

    expressions = []
    for row in grid:
        for ele in row:
            expressions.append(ele != m.eval(ele))

    solver.add(z3.Or(expressions))
    if solver.check() == z3.unsat:
        print('Solution is unique')
    else:
        print('Solution is not unique')
        m = solver.model()
        print_solution(m)
else:
    print('IMPOSSIBLE')

Another video solution

#!/usr/bin/env python3

# "Cheryl's Sudoku" 
#  by Elytron
# https://sudokupad.app/g337cy04rc
# https://youtu.be/JRIl0iPXOJg

from collections import defaultdict
import json
from typing import Literal

# types{{{
Digit = Literal[1, 2, 3, 4]
Size = Literal[0, 1, 2, 3]
Player = Literal["A", "B", "C", "D"]
SquareBoard = tuple[
    tuple[Digit, Digit, Digit, Digit],
    tuple[Digit, Digit, Digit, Digit],
    tuple[Digit, Digit, Digit, Digit],
    tuple[Digit, Digit, Digit, Digit],
]
FlatBoard = tuple[
    Digit,
    Digit,
    Digit,
    Digit,
    Digit,
    Digit,
    Digit,
    Digit,
    Digit,
    Digit,
    Digit,
    Digit,
    Digit,
    Digit,
    Digit,
    Digit,
]
# }}}

# utilities{{{
def check_valid(grid: SquareBoard):
    # assuming rows are permutations
    for j in range(4):
        col = {grid[i][j] for i in range(4)}
        if len(col) != 4:
            return False
        left_right_box, top_bottom_box = (j & 1) << 1, j & 0b10
        box = {
            grid[top_bottom_box][left_right_box],
            grid[top_bottom_box][left_right_box + 1],
            grid[top_bottom_box + 1][left_right_box],
            grid[top_bottom_box + 1][left_right_box + 1],
        }
        if len(box) != 4:
            return False
    return True


def flatten_board(board: SquareBoard) -> FlatBoard:
    flatten: list[Digit] = []
    for i in board:
        flatten.extend(i)
    flatten_tuple = tuple(flatten)
    assert len(flatten_tuple) == 16
    return flatten_tuple


def filter_by(boards: set[FlatBoard], player: Player, value: int):
    return group_by(boards, player)[value]


def group_by(boards: set[FlatBoard], player: Player):
    idx = "ABCD".index(player)
    result: defaultdict[int, set[FlatBoard]] = defaultdict(set)
    for board in boards:
        result[player_sums_for_boards[board][idx]].add(board)
    return result


def intersection(boards: set[FlatBoard]):
    if not boards:
        return tuple([None] * 16)
    somth = boards.pop()
    boards.add(somth)
    intx: list[int | None] = list(somth)
    for board in boards:
        for k, ele in enumerate(intx):
            if board[k] != ele:
                intx[k] = None
    return tuple(intx)


# }}}

# preprocessing{{{

with open(
    "./valid-sudokus.json"
) as f:  # a list of all valid sudokus generated by some other script
    boards = {flatten_board(board) for board in json.load(f)}

board_to_idx = {board: idx for idx, board in enumerate(boards)}

indicies: dict[Player, list[tuple[Size, Size]]] = {
    "A": [(1, 1), (2, 0), (2, 1)],
    "B": [(3, 2), (3, 3)],
    "C": [(1, 2), (2, 2), (2, 3)],
    "D": [(0, 3), (1, 3)],
}

flattened_indices = {
    i: tuple(4 * row + col for row, col in j) for i, j in indicies.items()
}

player_sums_for_boards: dict[FlatBoard, tuple[int, int, int, int]] = {}

for board in boards:
    sumss = tuple(sum(board[r] for r in flattened_indices[k]) for k in "ABCD")
    assert len(sumss) == 4
    player_sums_for_boards[board] = sumss
# }}}

# A's statement{{{

impossible_A = set()

for a in group_by(boards, "A").keys():
    all_possible_boards = filter_by(boards, "A", a)
    for board in all_possible_boards:
        _, b, c, d = player_sums_for_boards[board]
        for sym, val in zip("BCD", [b, c, d]):
            assert sym == "B" or sym == "C" or sym == "D"
            intrs = intersection(filter_by(boards, sym, val))
            if any(intrs):  # since None is Falsy, and non-zero numbers are truthy
                # print(f'{a:2} | {sym} can have {val} forcing {intrs}')
                impossible_A.add(a)
                break
        else:
            continue
        break

boards = {
    board for board in boards if player_sums_for_boards[board][0] not in impossible_A
}
# }}}

# B's statement{{{

possible_Bs = set()
for b in group_by(boards, "B").keys():
    all_possible_boards = filter_by(boards, "B", b)
    intrs = intersection(all_possible_boards)
    if not any(intrs):
        continue
    possible_Bs.add(b)

boards = {board for board in boards if player_sums_for_boards[board][1] in possible_Bs}
# }}}

# C's statement{{{
possible_Cs = set()
for c in group_by(boards, "C").keys():
    all_possiblities = {
        player_sums_for_boards[board] for board in filter_by(boards, "C", c)
    }
    if (not all_possiblities) or any(c in [a, b, d] for a, b, _, d in all_possiblities):
        continue
    possible_Cs.add(c)


boards = {board for board in boards if player_sums_for_boards[board][2] in possible_Cs}
# }}}

# D's statement{{{

possible_Ds = set()
for d in group_by(boards, "D").keys():
    all_possiblities = filter_by(boards, "D", d)
    if not all_possiblities:
        continue
    knownD = sum(x is not None for x in intersection(all_possiblities))
    for board in all_possiblities:
        a, b, c, _ = player_sums_for_boards[board]
        for sym, val in zip("BCA", [b, c, a]):
            assert sym == "B" or sym == "C" or sym == "A"
            intrs = intersection(filter_by(boards, sym, val))
            known_by_other = sum(i is not None for i in intrs)
            if known_by_other > knownD:
                break
        else:
            continue
        break
    else:
        continue
    possible_Ds.add(d)

boards = {board for board in boards if player_sums_for_boards[board][3] in possible_Ds}
# }}}

# Someone solved{{{
for player in "ABCD":
    hmm = group_by(boards, player)  # type: ignore
    for sm, games in hmm.items():
        if len(games) == 1:
            print(f"{player} would have solved if they had {sm} with the board {games}")
            win_game = games.pop()
            for i in range(0, 16, 4):
                print(*win_game[i : i + 4])
# }}}

"""
                                   :Solution:

                                    3 1 2 4
                                    2 4 3 1
                                    1 2 4 3
                                    4 3 1 2
"""
# vim: fdm=marker