Using Z3 to generate a slightly more optimal Minecraft sugarcane/water block layout compared to the farm presented by Mysticat in Top 3 Minecraft Sugarcane Farms at 7:32.
Original (190 sugarcanes):
Optimized (200 sugarcanes):
Using Z3 to generate a slightly more optimal Minecraft sugarcane/water block layout compared to the farm presented by Mysticat in Top 3 Minecraft Sugarcane Farms at 7:32.
Original (190 sugarcanes):
Optimized (200 sugarcanes):
import sys | |
from z3 import * | |
height = 19 | |
width = 9 | |
standard_solution = [ | |
[1, 0, 0, 0, 0, 1, 0, 0, 0], | |
[0, 0, 1, 0, 0, 0, 0, 1, 0], | |
[0, 0, 0, 0, 1, 0, 0, 0, 0], | |
[0, 1, 0, 0, 0, 0, 1, 0, 0], | |
[0, 0, 0, 1, 0, 0, 0, 0, 1], | |
[1, 0, 0, 0, 0, 1, 0, 0, 0], | |
[0, 0, 1, 0, 0, 0, 0, 1, 0], | |
[0, 0, 0, 0, 1, 0, 0, 0, 0], | |
[0, 1, 0, 0, 0, 0, 1, 0, 0], | |
[0, 0, 0, 1, 0, 0, 0, 0, 1], | |
[1, 0, 0, 0, 0, 1, 0, 0, 0], | |
[0, 0, 1, 0, 0, 0, 0, 1, 0], | |
[0, 0, 0, 0, 1, 0, 0, 0, 0], | |
[0, 1, 0, 0, 0, 0, 1, 0, 0], | |
[0, 0, 0, 1, 0, 0, 0, 0, 1], | |
[1, 0, 0, 0, 0, 1, 0, 0, 0], | |
[0, 0, 1, 0, 0, 0, 0, 1, 0], | |
[0, 0, 0, 0, 1, 0, 0, 0, 0], | |
[0, 1, 0, 0, 0, 0, 1, 0, 0], | |
] | |
def main(): | |
print_solution( | |
list(map(lambda row: list(map(lambda cell: cell != 0, row)), standard_solution)) | |
) | |
o = Optimize() | |
blocks = [[Bool(f"b_{y}_{x}") for x in range(width)] for y in range(height)] | |
# Each sugar cane requires an adjacent water block. | |
o.add( | |
*( | |
Implies( | |
blocks[y][x] == False, | |
adjacent_equals(blocks, y, x, [(-1, 0), (1, 0), (0, -1), (0, 1)], True), | |
) | |
for y in range(1, height - 1) | |
for x in range(1, width - 1) | |
) | |
) | |
o.add( | |
Or( | |
# Mirror symmetry about the x axis. | |
And( | |
*( | |
blocks[y][x] == blocks[height - 1 - y][x] | |
for y in range(height) | |
for x in range(width) | |
) | |
), | |
# Mirror symmetry about the y axis. | |
And( | |
*( | |
blocks[y][x] == blocks[y][width - 1 - x] | |
for y in range(height) | |
for x in range(width) | |
) | |
), | |
# Rotational symmetry. | |
And( | |
*( | |
blocks[y][x] == blocks[height - 1 - y][width - 1 - x] | |
for y in range(height) | |
for x in range(width) | |
) | |
), | |
) | |
) | |
# Minimize the adjacent water blocks. | |
for y in range(height): | |
for x in range(width): | |
directions = [ | |
(dy, dx) | |
for dy in [-1, 0, 1] | |
for dx in [-1, 0, 1] | |
if not (dy == 0 and dx == 0) | |
] | |
for direction in directions: | |
o.add_soft( | |
Implies( | |
blocks[y][x] == True, | |
Not(adjacent_equals(blocks, y, x, [direction], True)), | |
), | |
1_000, | |
) | |
# Minimize the water overall. | |
for y in range(height): | |
for x in range(width): | |
o.add_soft(blocks[y][x] == False, 1) | |
# Minimize the water within the growing area. | |
for y in range(1, height - 1): | |
for x in range(1, width - 1): | |
o.add_soft(blocks[y][x] == False, 1_000_000) | |
# print(o) | |
if o.check() == sat: | |
while o.check() == sat: | |
m = o.model() | |
# print(m) | |
evaluated = [ | |
[m.evaluate(blocks[y][x]) for x in range(width)] for y in range(height) | |
] | |
print_solution(evaluated) | |
o.add( | |
Or( | |
*( | |
blocks[y][x] != evaluated[y][x] | |
for y in range(height) | |
for x in range(width) | |
) | |
) | |
) | |
else: | |
raise RuntimeError("Failed to find a solution") | |
def adjacent_equals(blocks, y_mid, x_mid, directions, value): | |
return Or( | |
*( | |
blocks[y][x] == value | |
for (dy, dx) in directions | |
for y in [y_mid + dy] | |
if 0 <= y < height | |
for x in [x_mid + dx] | |
if 0 <= x < width | |
) | |
) | |
def print_solution(solution): | |
num_field = (height - 2) * (width - 2) | |
num_water_field = sum(1 for row in solution[1:-1] for cell in row[1:-1] if cell) | |
num_sugarcane_field = num_field - num_water_field | |
print(f"sugarcane: {num_sugarcane_field} water: {num_water_field}") | |
def character(y, x): | |
if 0 < y < height - 1 and 0 < x < width - 1: | |
# Dirt block | |
return "w" if solution[y][x] else "." | |
else: | |
# Structural block | |
return "w" if solution[y][x] else "#" | |
print( | |
"\n".join( | |
("".join((character(y, x) for x in range(width))) for y in range(height)) | |
) | |
) | |
sys.stdout.flush() | |
if __name__ == "__main__": | |
main() |