| This is an example of representing a Zebra Puzzle using a Z3-based Python code: | |
| There are 5 Producers in this puzzle. | |
| Categories and possible items: | |
| - Shirt: black, green, orange, pink, red | |
| - Name: Barbara, Isabella, Jane, Nicole, Rachel | |
| - Jam: apricot, cherry, fig, raspberry, watermelon | |
| - Size: 10 oz, 12 oz, 14 oz, 20 oz, 6 oz | |
| - Source: backyard, farmers' coop, local grocer, organic farm, wild pickings | |
| Clues: | |
| - The producer whose jam comes from Wild pickings is in the fourth position. | |
| - The producer selling Cherry jam is somewhere to the right of the one wearing a Green shirt. | |
| - Isabella is selling Cherry jam. | |
| - The producer wearing a Pink shirt is somewhere between the producer whose jam source is the Backyard and the one selling Watermelon jam, in that order. | |
| - The producer selling 14 oz jars is somewhere to the right of the one wearing a Green shirt. | |
| - The producer with 14 oz jars is next to the one selling Raspberry jam. | |
| - The Raspberry jam producer is positioned at one of the ends. | |
| - Barbara is next to the producer whose jam source is the Organic farm. | |
| - Jane is located somewhere between Nicole and Isabella, in that order. | |
| - The producer of Fig jam sources the fruit from an Organic farm. | |
| - The producer with 10 oz jars is at one of the ends. | |
| - The Raspberry jam producer is somewhere to the right of the one wearing a Green shirt. | |
| - The producer with 12 oz jars is next to the one who has 6 oz jars. | |
| - Isabella is next to the producer wearing a Black shirt. | |
| - The producer with 6 oz jars is next to the one whose source is the Local grocer. | |
| - The producer with 6 oz jars is in the second position. | |
| - Rachel's source of fruit is the Farmers' coop. | |
| - Barbara is next to Nicole. | |
| - The producer wearing an Orange shirt gets her fruit from the Backyard. | |
| - The producer with 12 oz jars is in the very first position. | |
| ```python | |
| from z3 import * | |
| import json | |
| import sys | |
| # Define all categories in a single list of tuples: | |
| # (House is implicit; each row's first column will be the house number.) | |
| categories = [ | |
| ("Shirt", ["black", "green", "orange", "pink", "red"]), | |
| ("Name", ["Barbara", "Isabella", "Jane", "Nicole", "Rachel"]), | |
| ("Jam", ["apricot", "cherry", "fig", "raspberry", "watermelon"]), | |
| ("Size", ["10 oz", "12 oz", "14 oz", "20 oz", "6 oz"]), | |
| ("Source", ["backyard", "farmers' coop", "local grocer", "organic farm", "wild pickings"]) | |
| ] | |
| # No need to change here, automatically processing | |
| NUM_POSITIONS = len(categories[0][1]) | |
| item_to_cat_and_index = {} | |
| for cat_idx, (cat_str, item_list) in enumerate(categories): | |
| for item_idx, item_str in enumerate(item_list): | |
| item_to_cat_and_index[(cat_str, item_str)] = (cat_idx, item_idx) | |
| Vars = [] | |
| for cat_idx, (cat_name, item_list) in enumerate(categories): | |
| var = IntVector(cat_name, len(item_list)) | |
| Vars.append(var) | |
| s = Solver() | |
| for cat_idx, (cat_name, item_list) in enumerate(categories): | |
| for item_idx, item_str in enumerate(item_list): | |
| s.add(Vars[cat_idx][item_idx] >= 1, Vars[cat_idx][item_idx] <= NUM_POSITIONS) | |
| s.add(Distinct(Vars[cat_idx])) | |
| def pos(cat_str, item_str): | |
| (cat_idx, item_idx) = item_to_cat_and_index[(cat_str, item_str)] | |
| return Vars[cat_idx][item_idx] | |
| # All clues here | |
| # The producer whose jam comes from Wild pickings is in the fourth position. | |
| s.add(pos("Source", "wild pickings") == 4) | |
| # The producer selling Cherry jam is somewhere to the right of the one wearing a Green shirt. | |
| s.add(pos("Jam", "cherry") > pos("Shirt", "green")) | |
| # Isabella is selling Cherry jam. | |
| s.add(pos("Name", "Isabella") == pos("Jam", "cherry")) | |
| # The producer wearing a Pink shirt is somewhere between the producer whose jam source is the Backyard and the one selling Watermelon jam, in that order. | |
| s.add(And(pos("Source", "backyard") < pos("Shirt", "pink"), pos("Shirt", "pink") < pos("Jam", "watermelon"))) | |
| # The producer selling 14 oz jars is somewhere to the right of the one wearing a Green shirt. | |
| s.add(pos("Size", "14 oz") > pos("Shirt", "green")) | |
| # The producer with 14 oz jars is next to the one selling Raspberry jam. | |
| s.add(Abs(pos("Size", "14 oz") - pos("Jam", "raspberry")) == 1) | |
| # The Raspberry jam producer is positioned at one of the ends. | |
| s.add(Or(pos("Jam", "raspberry") == 1, pos("Jam", "raspberry") == NUM_POSITIONS)) | |
| # Barbara is next to the producer whose jam source is the Organic farm. | |
| s.add(Abs(pos("Name", "Barbara") - pos("Source", "organic farm")) == 1) | |
| # Jane is located somewhere between Nicole and Isabella, in that order. | |
| s.add(And(pos("Name", "Nicole") < pos("Name", "Jane"), pos("Name", "Jane") < pos("Name", "Isabella"))) | |
| # The producer of Fig jam sources the fruit from an Organic farm. | |
| s.add(pos("Jam", "fig") == pos("Source", "organic farm")) | |
| # The producer with 10 oz jars is at one of the ends. | |
| s.add(Or(pos("Size", "10 oz") == 1, pos("Size", "10 oz") == NUM_POSITIONS)) | |
| # The Raspberry jam producer is somewhere to the right of the one wearing a Green shirt. | |
| s.add(pos("Jam", "raspberry") > pos("Shirt", "green")) | |
| # The producer with 12 oz jars is next to the one who has 6 oz jars. | |
| s.add(Abs(pos("Size", "12 oz") - pos("Size", "6 oz")) == 1) | |
| # Isabella is next to the producer wearing a Black shirt. | |
| s.add(Abs(pos("Name", "Isabella") - pos("Shirt", "black")) == 1) | |
| # The producer with 6 oz jars is next to the one whose source is the Local grocer. | |
| s.add(Abs(pos("Size", "6 oz") - pos("Source", "local grocer")) == 1) | |
| # The producer with 6 oz jars is in the second position. | |
| s.add(pos("Size", "6 oz") == 2) | |
| # Rachel's source of fruit is the Farmers' coop. | |
| s.add(pos("Name", "Rachel") == pos("Source", "farmers' coop")) | |
| # Barbara is next to Nicole. | |
| s.add(Abs(pos("Name", "Barbara") - pos("Name", "Nicole")) == 1) | |
| # The producer wearing an Orange shirt gets her fruit from the Backyard. | |
| s.add(pos("Shirt", "orange") == pos("Source", "backyard")) | |
| # The producer with 12 oz jars is in the very first position. | |
| s.add(pos("Size", "12 oz") == 1) | |
| # Solve the puzzle | |
| if s.check() == sat: | |
| m = s.model() | |
| rows = [] | |
| header = ["House"] + [cat_name for cat_name, _ in categories] | |
| for position in range(1, NUM_POSITIONS + 1): | |
| row = [str(position)] | |
| for cat_idx, (cat_name, item_list) in enumerate(categories): | |
| for item_idx, item_str in enumerate(item_list): | |
| if m.evaluate(Vars[cat_idx][item_idx]).as_long() == position: | |
| row.append(item_str) | |
| break | |
| rows.append(row) | |
| result_dict = {"header": header, "rows": rows} | |
| cnt = 1 | |
| block = [] | |
| for cat_idx, (cat_name, item_list) in enumerate(categories): | |
| for i in range(NUM_POSITIONS): | |
| block.append(Vars[cat_idx][i] != m[Vars[cat_idx][i]]) | |
| s.add(Or(block)) | |
| while s.check() == sat: | |
| m = s.model() | |
| cnt += 1 | |
| block = [] | |
| for cat_idx, (cat_name, item_list) in enumerate(categories): | |
| for i in range(NUM_POSITIONS): | |
| block.append(Vars[cat_idx][i] != m[Vars[cat_idx][i]]) | |
| s.add(Or(block)) | |
| if cnt == 1: | |
| # Output the solution as a JSON string. | |
| print(json.dumps(result_dict)) | |
| else: | |
| print(json.dumps({"error": "Multiple solutions found."})) | |
| else: | |
| print(json.dumps({"error": "No solution found."})) | |
| sys.stdout.flush() # Force immediate output | |
| ``` | |
| Based on this example, write a similar Z3-based Python code by changing only categories and constraints to represent the puzzle given below. |