New blog post: Z3 puzzle solving

This commit is contained in:
parent b1d58005c1
commit 7ab27b8c58
6 changed files with 480 additions and 0 deletions

4 index.html View File

 `@ -6,6 +6,10 @@` ``` ``` `

FliegendeWurst's corner of the WWW

` ``` ``` `Interesting tidbits:` ``` ``` `Solving a logic puzzle using an SMT solver` ``` ``` `Check out my projects:` ``` ``` `
`

214 logelei_off_by_one_sums.py Normal file View File

 `@ -0,0 +1,214 @@` `"""` `Python program to solve a logic puzzle.` `Full blog post: https://fliegendewurst.github.io/z3-logic-puzzle-solving.html` `Puzzle description: https://www.zeit.de/zeit-magazin/2022/32/logelei` `🄯 FliegendeWurst 2022` `This work is licensed under a Creative Commons Attribution 4.0 International License.` `http://creativecommons.org/licenses/by/4.0/` `"""` ``` ``` `from z3 import *` `import math` ``` ``` `s = Solver()` ``` ``` `# n*n grid` `n = 6` ``` ``` `grid = [[FreshInt() for x in range(n)] for y in range(n)]` ``` ``` `def print_solution(m, print_grid=True):` ` for k in range(num_sums):` ` print(" " * (3*num_sums + 2), end="")` ` for x in range(n):` ` val = m[sums_v[x][k]].as_long()` ` if val == -1:` ` print(" ", end=" ")` ` else:` ` print(f"{val: >2}", end=" ")` ` print()` ` print()` ` print(" " * (3*num_sums + 1), end="")` ` print("-" * (3*n))` ` y = 0` ` for row in grid:` ` for sum_h in sums_h[y]:` ` val = m[sum_h].as_long()` ` if val == -1:` ` print(" ", end=" ")` ` else:` ` print(f"{val: >2}", end=" ")` ` print("|", end=" ")` ` x = 0` ` for cell in row:` ` val = m[cell].as_long()` ` if val == 0 or not print_grid:` ` val = " "` ` print(f"{val: >2}", end=" ")` ` x += 1` ` print()` ` y += 1` ``` ``` `def distinct_if_nonzero(x):` ` for i in range(len(x)):` ` for j in range(i+1, len(x)):` ` cell_i = x[i]` ` cell_j = x[j]` ` s.add(If(And(cell_i != 0, cell_j != 0), cell_i != cell_j, True))` ``` ``` `# empty grid cell = 0` `# other numbers have to be in [1,2,3,4,5]` `# no duplicate digits in any row / column` `for row in grid:` ` for cell in row:` ` s.add(cell >= 0)` ` s.add(cell <= 5)` ` distinct_if_nonzero(row)` ``` ``` `for column in [[grid[y][x] for y in range(n)] for x in range(n)]:` ` distinct_if_nonzero(column)` ``` ``` `# each row and column has at most math.ceil(n/2) segments` `# if there are less, they are indicated by -1` `num_sums = math.ceil(n / 2)` `sums_h = [[FreshInt() for i in range(num_sums)] for y in range(n)]` `sums_v = [[FreshInt() for i in range(num_sums)] for x in range(n)]` `# for each pattern of used digits in a row, determine the sums` `# iterate over each row of the grid` `for y in range(n):` ` # iterate over each binary pattern` ` for p in range(2**n):` ` # match condition of this pattern` ` mc = True` ` # will contain a list of variables for each segment` ` segments = []` ` start_next_segment = True` ` # iterate over each grid cell` ` for x in range(n):` ` # check that binary digit in the pattern` ` if (p >> x) & 1 == 1:` ` mc = And(mc, grid[y][x] != 0)` ` if start_next_segment:` ` segments.append([grid[y][x]])` ` start_next_segment = False` ` else:` ` segments[-1].append(grid[y][x])` ` else:` ` mc = And(mc, grid[y][x] == 0)` ` start_next_segment = True` ` # specify sums value` ` for k in range(num_sums):` ` if k < len(segments):` ` off_by_one = Or(` ` sums_h[y][k] == sum(segments[k]) + 1,` ` sums_h[y][k] == sum(segments[k]) - 1` ` )` ` s.add(If(mc, off_by_one, True))` ` else:` ` s.add(If(mc, sums_h[y][k] == -1, True))` ``` ``` `# for each pattern of used digits in a columns, determine the sums` `for x in range(n):` ` for p in range(2**n):` ` # match condition` ` mc = True` ` segments = []` ` start_next_segment = True` ` for y in range(n):` ` if (p >> y) & 1 == 1:` ` mc = And(mc, grid[y][x] != 0)` ` if start_next_segment:` ` segments.append([grid[y][x]])` ` start_next_segment = False` ` else:` ` segments[-1].append(grid[y][x])` ` else:` ` mc = And(mc, grid[y][x] == 0)` ` start_next_segment = True` ` # specify sums value` ` #print(f"{p:b}"[::-1], segments)` ` for k in range(num_sums):` ` if k < len(segments):` ` off_by_one = Or(` ` sums_v[x][k] == sum(segments[k]) + 1,` ` sums_v[x][k] == sum(segments[k]) - 1` ` )` ` s.add(If(mc, off_by_one, True))` ` else:` ` s.add(If(mc, sums_v[x][k] == -1, True))` ``` ``` `res = s.check()` `print(res)` ``` ``` `def add_spec(spec_h, spec_v):` ` for a, b in zip(spec_h, sums_h):` ` for x, y in zip(a, b):` ` s.add(x == y)` ` for a, b in zip(spec_v, sums_v):` ` for x, y in zip(a, b):` ` s.add(x == y)` `spec_h = [` ` [2, 13, -1],` ` [5, 3, 6],` ` [8, 7, -1],` ` [4, 4, 1],` ` [5, 5, -1],` ` [9, 0, -1]` `]` ``` ``` `spec_v = [` ` [11, -1, -1],` ` [4, 5, -1],` ` [7, 7, -1],` ` [2, 7, 3],` ` [4, 4, 5],` ` [10, 2, -1]` `]` `s.push()` `add_spec(spec_h, spec_v)` ``` ``` `res = s.check()` `print(res)` ``` ``` `while res == sat:` ` m = s.model()` ` print_solution(m)` ` # find another solution, if possible` ` c = False` ` for row in grid:` ` for cell in row:` ` c = Or(c, cell != m[cell].as_long())` ` s.add(c)` ` res = s.check()` `print("no other solutions")` `s.pop()` ``` ``` `# try to find another puzzle with a unique solution` `while True:` ` s.push()` ` print("new push")` ` print(s.check())` ` m = s.model()` ` # condition c: keep found off-by-one sums configuration` ` # condition c2: to ban this sums configuration` ` c = True` ` c2 = False` ` for l in [*sums_h, *sums_v]:` ` for x in l:` ` c = And(c, x == m[x].as_long())` ` c2 = Or(c2, x != m[x].as_long())` ` s.add(c)` ` # try to find another solution` ` c = False` ` for row in grid:` ` for cell in row:` ` c = Or(c, cell != m[cell].as_long())` ` s.add(c)` ` res = s.check()` ` print(res)` ` if res == unsat:` ` print("found another puzzle with unique solution")` ` print_solution(m, print_grid=False)` ` input("continue? [press enter]")` ` s.pop()` ` s.add(c2)`

1 raspberry-pi-temperature-monitoring.html View File

 `@ -2,6 +2,7 @@` `` `Raspberry Pi temperature monitoring + calendar` `` `` `` `` ``

BIN sample-puzzle.png Normal file View File

Binary file not shown.
 After Width:  |  Height:  |  Size: 31 KiB

BIN sample-puzzle.xcf Normal file View File

Binary file not shown.

261 z3-logic-puzzle-solving.html Normal file View File

 `@ -0,0 +1,261 @@` `` `` `Solving a logic puzzle using an SMT solver` `` `` `` `` `` ``` ``` `` `

FliegendeWurst's corner of the WWW

` ``` ``` `

Solving a logic puzzle using an SMT solver

` ``` ``` `
` ``` ``` `In this blog post, I'll describe how to solve a logic puzzle using Z3, an automated SMT solver.` ``` ``` `

The puzzle

` ``` ``` `

` `You are given a rectangular grid where each cell may either contain a number (between 1 and 5) or be empty.` `Each number may only be used once in each row and column.` `In each row, the empty cells split the numbered cells into segments.` `The sums of these segments are indicated to the left of the grid.` `The same applies to the columns of the grid (sums are indicated above the grid).` `But there's a twist: due to a transmission error, all of the sums are off by one!` `The (already solved) 4-by-4 grid below illustrates these constraints.` `
` ``` ``` `` ``` ``` `

` ``` ``` `

` `I originally found this puzzle in an edition of the ZEIT, a weekly German newspaper.` `See the previous link for a more difficult puzzle. It is solvable without computer assistance, but quite tricky!` `

` ``` ``` `

Prerequisites

` ``` ``` `To follow along, you'll first need to install Python.` `Then, you need to install the Z3 Python bindings.` `The precise installation steps vary by operating system, check the official documentation for more details.` ``` ``` `

Defining the board

` ``` ``` `In the following, I will describe the code required to explain the puzzle to Z3.` `First, we need to import the z3 Python module. To avoid prefixing every constructor with z3., we import all symbols into the local namespace. We also import the math module (we will need it later).` `We also create a new Solver object for later use.` `
`
`from z3 import *`
`import math`
``` ```
`s = Solver()`
`
` `Problems are specified by creating a bunch of variables (booleans, integers, ...) and constraints on these variables.` `Z3 will then produce a model that assigns a value to each variable if the constraints are satisfiable.` `Since we are interested in the values of the grid cells, we create an integer variable for each cell.` `FreshInt returns a new integer variable that isn't identical to any other previously created variable.` `
`
`# n*n grid`
`n = 6`
``` ```
`grid = [[FreshInt() for x in range(n)] for y in range(n)]`
`
` ``` ``` `

Specifying the constraints

` ``` ``` `Empty grid cells will be indicated by a value of zero. All other cells need to be filled with a number between one and five.` `To implement this constraint, we iterate over each row and cell of the grid and add the constraint (integer value must be at least 0 and at most 5) to the solver.` `
`
`for row in grid:`
`    for cell in row:`
`        s.add(cell >= 0)`
`        s.add(cell <= 5)`
`
` ``` ``` `For each row/column, the numbers used must be unique.` `This is modeled by pairwise inequality of the variables making up that row or column.` `Of course, a value of zero (= empty grid cell) may appear more than once.` ``` ``` `We define a function distinct_if_nonzero that, given a list of variables, adds constraints to ensure that any two variables are not equal if both of them are nonzero.` `This is done by supplying three parameters to the If function: the condition, the constraint if the condition is true, the constraint if the condition is false.` `
`
`def distinct_if_nonzero(x):`
`    for i in range(len(x)):`
`        for j in range(i+1, len(x)):`
`            cell_i = x[i]`
`            cell_j = x[j]`
`            s.add(If(And(cell_i != 0, cell_j != 0), cell_i != cell_j, True))`
`
` `Then we simply apply this function to each row and column of the grid.` `
`
`for row in grid:`
`    distinct_if_nonzero(row)`
``` ```
`for column in [[grid[y][x] for y in range(n)] for x in range(n)]:`
`    distinct_if_nonzero(column)`
`
` ``` ``` `The sums indicated next to the grid are represented by integer variables.` `It is quite obvious that the maximum number of segments possible in each row is achieved if every second cell is filled with a number.` `As such, we only need to keep track of that many segment sums.` `
`
`num_sums = math.ceil(n / 2)`
`sums_h = [[FreshInt() for i in range(num_sums)] for y in range(n)]`
`sums_v = [[FreshInt() for i in range(num_sums)] for x in range(n)]`
`
` ``` ``` `Connecting these sums to the cell variables is done by considering each binary pattern p of numbered / not numbered cells.` `
`
`# iterate over each row of the grid`
`for y in range(n):`
`    # iterate over each binary pattern`
`    for p in range(2**n):`
`        # match condition of this pattern`
`        mc = True`
`        # will contain a list of variables for each segment`
`        segments = []`
`        start_next_segment = True`
`        # iterate over each grid cell`
`        for x in range(n):`
`            # check that binary digit in the pattern`
`            if (p >> x) & 1 == 1:`
`                mc = And(mc, grid[y][x] != 0)`
`                if start_next_segment:`
`                    segments.append([grid[y][x]])`
`                    start_next_segment = False`
`                else:`
`                    segments[-1].append(grid[y][x])`
`            else:`
`                mc = And(mc, grid[y][x] == 0)`
`                start_next_segment = True`
`        # specify sums value of each segment`
`        for k in range(num_sums):`
`            if k < len(segments):`
`                off_by_one = Or(`
`                    sums_h[y][k] == sum(segments[k]) + 1,`
`                    sums_h[y][k] == sum(segments[k]) - 1`
`                )`
`                s.add(If(mc, off_by_one, True))`
`            else:`
`                s.add(If(mc, sums_h[y][k] == -1, True))`
`
` `The same is done for the columns of the grid. For brevity, that code is omitted from this post. The full source code is linked at the end of the article.` ``` ``` `

Finding and displaying a solution

` ``` ``` `We still need to encode the off-by-one sums given in the puzzle as constraints.` `This is fairly simple:` `
`
`def add_spec(spec_h, spec_v):`
`    for a, b in zip(spec_h, sums_h):`
`        for x, y in zip(a, b):`
`            s.add(x == y)`
`    for a, b in zip(spec_v, sums_v):`
`        for x, y in zip(a, b):`
`            s.add(x == y)`
`spec_h = [`
`    [2, 13, -1],`
`    [5, 3, 6],`
`    [8, 7, -1],`
`    [4, 4, 1],`
`    [5, 5, -1],`
`    [9, 0, -1]`
`]`
``` ```
`spec_v = [`
`    [11, -1, -1],`
`    [4, 5, -1],`
`    [7, 7, -1],`
`    [2, 7, 3],`
`    [4, 4, 5],`
`    [10, 2, -1]`
`]`
`s.push()`
`add_spec(spec_h, spec_v)`
`
` `Note that we used s.push() to create a nested constraint context.` `Any constraints added after this call may be removed by calling s.pop().` `We will make use of this later to generate new puzzles (with new off-by-one sums).` ``` ``` `

` `Now that we have specified all of our contraints, we may ask Z3 to determine the validity of our model.` `s.check() may return sat, unsat or unknown.` `sat indicates that the problem is satisfiable (there is a variable assignment that fulfills all constraints), unsat indicates that no such assignment is possible.` `Z3 only returns unknown if it is not able to deduce whether the problem is satisfiable or not (e.g., due to incomplete theories).` `

` ``` ``` `

` `The loop below uses a simple trick to enumerate all solutions to the puzzle: after one solution is found, add a constraint that at least one grid cell must be different.` `

` ``` ``` `
`
`res = s.check()`
`print(res)`
``` ```
`while res == sat:`
`    m = s.model()`
`    print_solution(m)`
`    # find another solution, if possible`
`    c = False`
`    for row in grid:`
`        for cell in row:`
`            c = Or(c, cell != m[cell].as_long())`
`    s.add(c)`
`    res = s.check()`
`print("no other solutions")`
`s.pop()`
`
` ``` ``` `

Generating puzzles with a unique solution

` ``` ``` `

` `Generating new puzzles is surprisingly easy at this point.` `It boils down to not constraining the off-by-one sums.` `Z3 will still generate a model that fits all of the puzzle rules.` `To determine whether a newly-found puzzle has a unique solution, we first need to add the new off-by-one sums to Z3.` `Additionally, we mandate that at least one grid cell needs to differ.` `If no other solution is found, we know that the puzzle has a unique solution.` `Otherwise, we add a constraint that bans this particular off-by-one sums configuration (this ensures we always try new puzzles).` `

` ``` ``` `
`
`# try to find another puzzle with a unique solution`
`while True:`
`    s.push()`
`    print("new push")`
`    print(s.check())`
`    m = s.model()`
`    # condition c: keep found off-by-one sums configuration`
`    # condition c2: to ban this sums configuration`
`    c = True`
`    c2 = False`
`    for l in [*sums_h, *sums_v]:`
`        for x in l:`
`            c = And(c, x == m[x].as_long())`
`            c2 = Or(c2, x != m[x].as_long())`
`    s.add(c)`
`    # try to find another solution`
`    c = False`
`    for row in grid:`
`        for cell in row:`
`            c = Or(c, cell != m[cell].as_long())`
`    s.add(c)`
`    res = s.check()`
`    print(res)`
`    if res == unsat:`
`        print("found another puzzle with unique solution")`
`        print_solution(m, print_grid=False)`
`        input("continue? [press enter]")`
`    s.pop()`
`    s.add(c2)`
`
` ``` ``` `Full source code` ``` ``` `` ``` ``` `
`