Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
16 changes: 5 additions & 11 deletions examples/chess-recognition.py
Original file line number Diff line number Diff line change
Expand Up @@ -118,18 +118,12 @@ def softmax(vector):
(Count(board[0], P) == 0),
(Count(board[7], p) == 0),
(Count(board[7], P) == 0),
# The number of pieces of each piece type without promotion
((Count(board, p) == 8) | (Count(board, P) == 8)).implies(
(Count(board, b) <= 2) &
(Count(board, r) <= 2) &
(Count(board, n) <= 2) &
(Count(board, q) <= 1)
# The number of pieces can't exceed the starting number plus the number of promotions possible
(
(Count(board, b) + Count(board, r) + Count(board, n) + Count(board, q) <= 2+2+1+1 + 8-Count(board, p))
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

fine for me to include in this PR, but normally this could be split up in separate PRs (although it's a little more effort)

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

i'd update the comment to reflect the new/fixed constraint

),
((Count(board, P) == 8) | (Count(board, p) == 8)).implies(
(Count(board, B) <= 2) &
(Count(board, R) <= 2) &
(Count(board, N) <= 2) &
(Count(board, Q) <= 1)
(
(Count(board, B) + Count(board, R) + Count(board, N) + Count(board, Q) <= 2+2+1+1 + 8-Count(board, P))
),
# Bishops can't have moved if the pawns are still in starting position
((board[1, 1] == p) & (board[1, 3] == p) & (
Expand Down
159 changes: 159 additions & 0 deletions examples/sudoku_chaos_killer.py
Original file line number Diff line number Diff line change
@@ -0,0 +1,159 @@
import cpmpy as cp
import numpy as np


"""
Puzzle source: https://logic-masters.de/Raetselportal/Raetsel/zeigen.php?id=0009KE

Rules:

- Place the numbers from 1 to 9 exactly once in every row, column, and region.
- Each region is orthogonally connected and must be located by the solver.
- An area outlined by dashes is called a killer cage.
All numbers in a killer cage belong to the same region and sum to the number in the top left corner of the killer cage.
"""

SIZE = 9

# sudoku cells
cell_values = cp.intvar(1,SIZE, shape=(SIZE,SIZE))
# decision variables for the regions
cell_regions = cp.intvar(1,SIZE, shape=(SIZE,SIZE))
# regions cardinals
region_cardinals = cp.intvar(1,SIZE, shape=(SIZE,SIZE))


def killer_cage(idxs, values, regions, total):
"""
the sum of the cells in the cage must equal the total
all cells in the cage must be in the same region

Args:
idxs (np.array): array of indices representing the cells in the cage
values (cp.intvar): cpmpy variable representing the cell values
regions (cp.intvar): cpmpy variable representing the cell regions
total (int): the total sum for the cage

Returns:
list: list of cpmpy constraints enforcing the killer cage rules
"""
constraints = []
constraints.append(cp.sum([values[r, c] for r,c in idxs]) == total)
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

just for fun, I've been trying more numpy-type features lately. Could this become cp.sum(values[idxs]) == total?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

that doesn't work, I think something along the lines cp.sum(values[list(zip(*idxs))) == total should work, although the last time I did that the CI complained about the * operator, because it was introduced quite recently, so I'm not gonna attempt to make this magic work

constraints.append(cp.AllEqual([regions[r, c] for r,c in idxs]))
return constraints

def get_neighbours(r, c):
"""
from a cell get the indices of its orthogonally adjacent neighbours

Args:
r (int): row index
c (int): column index

Returns:
list: list of tuples representing the indices of orthogonally adjacent neighbours
"""
# a cell must be orthogonally adjacent to a cell in the same region

# check if on top row
if r == 0:
if c == 0:
return [(r, c+1), (r+1, c)]
elif c == SIZE-1:
return [(r, c-1), (r+1, c)]
else:
return [(r, c-1), (r, c+1), (r+1, c)]
# check if on bottom row
elif r == SIZE-1:
if c == 0:
return [(r, c+1), (r-1, c)]
elif c == SIZE-1:
return [(r, c-1), (r-1, c)]
else:
return [(r, c-1), (r, c+1), (r-1, c)]
# check if on left column
elif c == 0:
return [(r-1, c), (r+1, c), (r, c+1)]
# check if on right column
elif c == SIZE-1:
return [(r-1, c), (r+1, c), (r, c-1)]
# check if in the middle
else:
return [(r-1, c), (r+1, c), (r, c-1), (r, c+1)]



m = cp.Model(
killer_cage(np.array([[0,0],[0,1],[1,1]]), cell_values, cell_regions, 18),
killer_cage(np.array([[1,0],[2,0],[2,1]]), cell_values, cell_regions, 8),
killer_cage(np.array([[3,0],[3,1],[3,2],[2,2],[1,2]]), cell_values, cell_regions, 27),
killer_cage(np.array([[4,0],[4,1]]), cell_values, cell_regions, 17),
killer_cage(np.array([[5,0],[5,1]]), cell_values, cell_regions, 8),
killer_cage(np.array([[1,3],[1,4]]), cell_values, cell_regions, 6),
killer_cage(np.array([[0,7],[0,8]]), cell_values, cell_regions, 4),
killer_cage(np.array([[2,3],[3,3],[3,4],[4,3]]), cell_values, cell_regions, 12),
killer_cage(np.array([[1,5],[2,5],[3,5],[2,4]]), cell_values, cell_regions, 28),
killer_cage(np.array([[4,4],[4,5],[5,5],[4,6]]), cell_values, cell_regions, 16),
killer_cage(np.array([[2,8],[3,8]]), cell_values, cell_regions, 15),
killer_cage(np.array([[3,6],[3,7],[4,7],[4,8]]), cell_values, cell_regions, 17),
killer_cage(np.array([[6,2],[6,3],[7,3]]), cell_values, cell_regions, 21),
killer_cage(np.array([[7,2],[8,2]]), cell_values, cell_regions, 5),
killer_cage(np.array([[8,3],[8,4]]), cell_values, cell_regions, 15),
killer_cage(np.array([[6,4],[7,4]]), cell_values, cell_regions, 8),
killer_cage(np.array([[6,5],[7,5],[6,6]]), cell_values, cell_regions, 19),
killer_cage(np.array([[8,5],[8,6]]), cell_values, cell_regions, 11),
killer_cage(np.array([[7,6],[7,7],[8,7]]), cell_values, cell_regions, 10),
)

for i in range(cell_values.shape[0]):
m += cp.AllDifferent(cell_values[i,:])
m += cp.AllDifferent(cell_values[:,i])


total_cells = SIZE**2
for i in range(total_cells-1):
r1 = i // SIZE
c1 = i % SIZE

neighbours = get_neighbours(r1, c1)

# at least one neighbour must be in the same region with a smaller cardinal number or the cell itself must have cardinal number 1; this forces connectedness of regions
m += cp.any([cp.all([cell_regions[r1,c1] == cell_regions[r2,c2], region_cardinals[r1, c1] > region_cardinals[r2, c2]]) for r2,c2 in neighbours]) | (region_cardinals[r1,c1] == 1)



for r in range(1, SIZE+1):
# Enforce size for each region
m += cp.Count(cell_regions, r) == SIZE # each region must be of size SIZE


# Create unique IDs for each (value, region) pair to enforce all different
m += cp.AllDifferent([(cell_values[i,j]-1)*SIZE+cell_regions[i,j]-1 for i in range(SIZE) for j in range(SIZE)])
# Only 1 cell with cardinal number 1 per region
for r in range(1, SIZE+1):
m += cp.Count([(region_cardinals[i,j])*(cell_regions[i,j] == r) for i in range(SIZE) for j in range(SIZE)], 1) == 1


# Symmetry breaking for the regions
# fix top-left and bottom-right region to reduce symmetry
m += cell_regions[0,0] == 1
m += cell_regions[SIZE-1, SIZE-1] == SIZE

sol = m.solve()

print("The solution is:")
print(cell_values.value())
print("The regions are:")
print(cell_regions.value())

assert (cell_values.value() == [[9, 6, 7, 4, 8, 5, 2, 1, 3],
[2, 3, 8, 1, 5, 4, 6, 9, 7],
[1, 5, 2, 3, 9, 7, 4, 8, 6],
[4, 7, 6, 2, 1, 8, 3, 5, 9],
[8, 9, 3, 6, 4, 1, 5, 7, 2],
[7, 1, 9, 5, 3, 6, 8, 2, 4],
[6, 8, 5, 9, 2, 3, 7, 4, 1],
[5, 2, 4, 7, 6, 9, 1, 3, 8],
[3, 4, 1, 8, 7, 2, 9, 6, 5]]).all()

# can not assert regions as there are symmetric solutions.. I can add symmetry breaking constraint, but it is slow in this case
133 changes: 119 additions & 14 deletions examples/sudoku_chockablock.py
Original file line number Diff line number Diff line change
@@ -1,7 +1,22 @@
import cpmpy as cp
import numpy as np

# This cpmpy example solves a sudoku by marty_sears, which can be found on https://logic-masters.de/Raetselportal/Raetsel/zeigen.php?id=000I2P

"""
Puzzle source: https://logic-masters.de/Raetselportal/Raetsel/zeigen.php?id=000I2P

Rules:

- Normal sudoku rules apply.
- Unique N-Lines: ALL lines in the grid are N-Lines. Each N-line is composed of one or more non-overlapping sets of adjacent digits, each of which sum to N. Every line has a different N value.
- Coloured lines (not including the grey ones) each have an additional rule:
- Renban (pink): Digits on a pink line form a non-repeating consecutive set, which can be arranged in any order.
- Even Sum Lines (darker blue): All the digits on a darker blue line sum to an even number.
- Prime Lines (purple): Adjacent digits on a purple line sum to a prime number.
- Anti-Kropki Lines (red): No two digits anywhere on the same red line are consecutive, or in a 1:2 ratio (but they may repeat).
- Same Difference Lines (turquoise): Each pair of adjacent digits on a turquoise line have the same difference. This difference must be determined for each turquoise line.
- The grey perimeter can be used for making notes.
"""

# sudoku cells
cells = cp.intvar(1,9, shape=(9,9))
Expand All @@ -10,11 +25,20 @@


def n_lines(array, total):
# N-lines are composed of one or more non-overlapping sets of adjacent cells
# The number of such partitions is exponential, luckily all the lines are of length 3 so we can easily hardcode them
# partitions = [(3), (2,1), (1,2), (1,1,1)]
# For every partition we can check whether each subpartition sums to the same number
# the N variable should be equal to a partition where it holds that each subpartition sums to the same number
""""
N-lines are composed of one or more non-overlapping sets of adjacent cells
The number of such partitions is exponential, luckily all the lines are of length 3 so we can easily hardcode them
partitions = [(3), (2,1), (1,2), (1,1,1)]
For every partition we can check whether each subpartition sums to the same number
the N variable should be equal to a partition where it holds that each subpartition sums to the same number

Args:
array (cp.intvar): cpmpy variable representing the cells on the line
total (cp.intvar): cpmpy variable representing the total sum for the line

Returns:
cpmpy constraint enforcing the N-line rule
"""
all_partitions = [[array], [array[:2], array[2:]], [array[:1], array[1:]], [array[:1], array[1:2], array[2:]]]
sums = cp.intvar(0,27, shape=4)
partial_sums = []
Expand All @@ -34,44 +58,115 @@ def n_lines(array, total):
return cp.all(constraints)

def even_sum(array, total):
# line must sum to an even total
"""
line must sum to an even total

Args:
array (cp.intvar): cpmpy variable representing the cells on the line
total (cp.intvar): cpmpy variable representing the total sum for the line

Returns:
cpmpy constraint enforcing the even sum rule and the n-line rule
"""
return cp.all([n_lines(array, total), total % 2 == 0])

def prime_sum(array, total):
# all prime sums reachable for two sudoku digits
"""
line must sum to a prime total

Args:
array (cp.intvar): cpmpy variable representing the cells on the line
total (cp.intvar): cpmpy variable representing the total sum for the line

Returns:
cpmpy constraint enforcing the prime sum rule and the n-line rule
"""
primes = [2, 3, 5, 7, 11, 13, 17]
pairs = [(a,b) for a,b in zip(array, array[1:])]
return cp.all([n_lines(array, total), cp.all([cp.any([cp.sum(pair) == p for p in primes]) for pair in pairs])])

def renban(array, total):
# digits on a pink renban form a set of consecutive non repeating digits
"""
digits on a pink renban form a set of consecutive non repeating digits

Args:
array (cp.intvar): cpmpy variable representing the cells on the line
total (cp.intvar): cpmpy variable representing the total sum for the line

Returns:
cpmpy constraint enforcing the renban rule and the n-line rule
"""
return cp.all([n_lines(array, total), cp.AllDifferent(array), cp.max(array) - cp.min(array) == len(array) - 1])

# there are no kropki dots in this sudoku the two following functions are used for the anti-kropki line
def white_kropki(a, b):
# digits separated by a white dot differ by 1
"""
digits separated by a white dot differ by 1

Args:
a (cp.intvar): cpmpy variable representing cell a
b (cp.intvar): cpmpy variable representing cell b

Returns:
cpmpy constraint enforcing the white kropki rule
"""
return abs(a-b) == 1

def black_kropki(a, b):
# digits separated by a black dot are in a 1:2 ratio
"""
digits separated by a black dot are in a 1:2 ratio

Args:
a (cp.intvar): cpmpy variable representing cell a
b (cp.intvar): cpmpy variable representing cell b

Returns:
cpmpy constraint enforcing the black kropki rule
"""
return cp.any([a * 2 == b, a == 2 * b])

def anti_kropki(array, total):
# no pair anywhere on the line may be in a kropki relationship
"""
no pair anywhere on the line may be in a kropki relationship

Args:
array (cp.intvar): cpmpy variable representing the cells on the line
total (cp.intvar): cpmpy variable representing the total sum for the line

Returns:
cpmpy constraint enforcing the anti-kropki rule and the n-line rule
"""
all_pairs = [(a, b) for idx, a in enumerate(array) for b in array[idx+1:]]
constraints = []
for pair in all_pairs:
constraints.append(cp.all([~white_kropki(pair[0], pair[1]), ~black_kropki(pair[0], pair[1])]))
return cp.all([cp.all(constraints), n_lines(array, total)])

def same_difference(array, total):
# adjacent cells on the line must all have the same difference
"""
adjacent cells on the line must all have the same difference

Args:
array (cp.intvar): cpmpy variable representing the cells on the line
total (cp.intvar): cpmpy variable representing the total sum for the line

Returns:
cpmpy constraint enforcing the same difference rule and the n-line rule
"""
diff = cp.intvar(0,8, shape=1)
return cp.all([cp.all([abs(a-b) == diff for a,b in zip(array, array[1:])]), n_lines(array, total)])


def regroup_to_blocks(grid):
# Create an empty list to store the blocks
"""
Regroup the 9x9 grid into its 3x3 blocks.

Args:
grid (cp.intvar): cpmpy variable representing the 9x9 sudoku grid

Returns:
list: list of lists representing the 3x3 blocks of the sudoku grid
"""
blocks = [[] for _ in range(9)]

for row_index in range(9):
Expand Down Expand Up @@ -138,3 +233,13 @@ def regroup_to_blocks(grid):
sol = m.solve()
print("The solution is:")
print(cells.value())

assert (cells.value() == [[3, 1, 9, 5, 6, 8, 7, 2, 4],
[7, 2, 8, 9, 4, 1, 5, 3, 6],
[4, 5, 6, 7, 2, 3, 1, 8, 9],
[9, 7, 5, 2, 3, 4, 6, 1, 8],
[2, 8, 1, 6, 9, 5, 3, 4, 7],
[6, 4, 3, 1, 8, 7, 2, 9, 5],
[1, 6, 4, 8, 7, 2, 9, 5, 3],
[5, 3, 7, 4, 1, 9, 8, 6, 2],
[8, 9, 2, 3, 5, 6, 4, 7, 1]]).all()
Loading
Loading